Documentation

Carleson.RealInterpolation

This file contains a proof of the Marcinkiewisz real interpolation theorem. The proof roughly follows Folland, Real Analysis. Modern Techniques and Their Applications, section 6.4, theorem 6.28, but a different truncation is used, and some estimates instead follow the technique as e.g. described in [Duoandikoetxea, Fourier Analysis, 2000].

The file consists of the following sections:
- Convience results for working with (interpolated) exponents
- Results about the particular choice of exponent
- Interface for using cutoff functions
- Results about the particular choice of scale
- Some tools for measure theory computations
- Results about truncations of a function
- Measurability properties of truncations
- Truncations and Lp spaces
- Some results about the integrals of truncations
- Minkowski's integral inequality
- Apply Minkowski's integral inequality to truncations
- Weaktype estimates applied to truncations
- Definitions
- Proof of the real interpolation theorem

Convenience results for working with (interpolated) exponents #

theorem ComputationsInterpolatedExponents.ofReal_mem_Ioo_0_1 {t : ℝ} (h : t ∈ Set.Ioo 0 1) :

ENNReal.ofReal t ∈ Set.Ioo 0 1

theorem ComputationsInterpolatedExponents.ENNReal_preservation_positivity₀ {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hpq : p ≠ ⊤ ∨ q ≠ ⊤) :

0 < (1 - ENNReal.ofReal t) * p⁻¹ + ENNReal.ofReal t * q⁻¹

theorem ComputationsInterpolatedExponents.ENNReal_preservation_positivity {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hpq : p ≠ q) :

0 < (1 - ENNReal.ofReal t) * p⁻¹ + ENNReal.ofReal t * q⁻¹

theorem ComputationsInterpolatedExponents.ENNReal_preservation_positivity' {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p > 0

theorem ComputationsInterpolatedExponents.interp_exp_ne_top {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

theorem ComputationsInterpolatedExponents.interp_exp_ne_top' {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀p₁ : p₀ ≠ ⊤ ∨ p₁ ≠ ⊤) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

theorem ComputationsInterpolatedExponents.interp_exp_eq {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀p₁ : p₀ = p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p₀ = p

theorem ComputationsInterpolatedExponents.interp_exp_lt_top {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

theorem ComputationsInterpolatedExponents.interp_exp_lt_top' {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀p₁ : p₀ ≠ ⊤ ∨ p₁ ≠ ⊤) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

theorem ComputationsInterpolatedExponents.interp_exp_between {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ < p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p ∈ Set.Ioo p₀ p₁

theorem ComputationsInterpolatedExponents.one_le_interp_exp_aux {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀ : 1 ≤ p₀) (hp₁ : 1 ≤ p₁) (hp₀p₁ : p₀ < p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

1 ≤ p

theorem ComputationsInterpolatedExponents.switch_exponents {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p⁻¹ = (1 - ENNReal.ofReal (1 - t)) * p₁⁻¹ + ENNReal.ofReal (1 - t) * p₀⁻¹

theorem ComputationsInterpolatedExponents.one_le_toReal {a : ENNReal} (ha₁ : 1 ≤ a) (ha₂ : a < ⊤) :

1 ≤ a.toReal

theorem ComputationsInterpolatedExponents.one_le_interp {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀ : 1 ≤ p₀) (hp₁ : 1 ≤ p₁) (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

1 ≤ p

theorem ComputationsInterpolatedExponents.one_le_interp_toReal {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀ : 1 ≤ p₀) (hp₁ : 1 ≤ p₁) (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

1 ≤ p.toReal

theorem ComputationsInterpolatedExponents.coe_rpow_ne_top {a : ℝ} {q : ℝ} (hq : q ≥ 0) :

ENNReal.ofReal a ^ q ≠ ⊤

theorem ComputationsInterpolatedExponents.coe_rpow_ne_top' {a : ℝ} {q : ℝ} (hq : 0 < q) :

ENNReal.ofReal a ^ q ≠ ⊤

theorem ComputationsInterpolatedExponents.coe_pow_pos {a : ℝ} {q : ℝ} (ha : a > 0) :

ENNReal.ofReal a ^ q > 0

theorem ComputationsInterpolatedExponents.rpow_ne_top' {a : ENNReal} {q : ℝ} (ha : a ≠ 0) (ha' : a ≠ ⊤) :

theorem ComputationsInterpolatedExponents.exp_toReal_pos' {q : ENNReal} (hq : q ≥ 1) (hq' : q < ⊤) :

q.toReal > 0

theorem ComputationsInterpolatedExponents.ne_top_of_Ico {p : ENNReal} {q : ENNReal} {r : ENNReal} (hq : q ∈ Set.Ico p r) :

theorem ComputationsInterpolatedExponents.lt_top_of_Ico {p : ENNReal} {q : ENNReal} {r : ENNReal} (hq : q ∈ Set.Ico p r) :

theorem ComputationsInterpolatedExponents.ne_top_of_Ioo {p : ENNReal} {q : ENNReal} {r : ENNReal} (hq : q ∈ Set.Ioo p r) :

theorem ComputationsInterpolatedExponents.lt_top_of_Ioo {p : ENNReal} {q : ENNReal} {r : ENNReal} (hq : q ∈ Set.Ioo p r) :

theorem ComputationsInterpolatedExponents.ne_top_of_Ioc {p : ENNReal} {q : ENNReal} {r : ENNReal} (hq : q ∈ Set.Ioc p r) (hr : r < ⊤) :

theorem ComputationsInterpolatedExponents.pos_of_rb_Ioc {p : ENNReal} {q : ENNReal} {r : ENNReal} (hr : q ∈ Set.Ioc p r) :

0 < r

theorem ComputationsInterpolatedExponents.exp_toReal_ne_zero {q : ENNReal} (hq : q ≥ 1) (hq' : q < ⊤) :

q.toReal ≠ 0

theorem ComputationsInterpolatedExponents.exp_toReal_ne_zero' {q : ENNReal} (hq : q > 0) (hq' : q ≠ ⊤) :

q.toReal ≠ 0

theorem ComputationsInterpolatedExponents.exp_toReal_ne_zero_of_Ico {q : ENNReal} {p : ENNReal} (hq : q ∈ Set.Ico 1 p) :

q.toReal ≠ 0

theorem ComputationsInterpolatedExponents.pos_of_Ioo {p : ENNReal} {q : ENNReal} {r : ENNReal} (hq : q ∈ Set.Ioo p r) :

q > 0

theorem ComputationsInterpolatedExponents.ne_zero_of_Ioo {p : ENNReal} {q : ENNReal} {r : ENNReal} (hq : q ∈ Set.Ioo p r) :

q ≠ 0

theorem ComputationsInterpolatedExponents.pos_of_Icc_1 {p : ENNReal} {q : ENNReal} (hp : p ∈ Set.Icc 1 q) :

p > 0

theorem ComputationsInterpolatedExponents.pos_of_ge_1 {p : ENNReal} (hp : 1 ≤ p) :

p > 0

theorem ComputationsInterpolatedExponents.pos_rb_of_Icc_1_inh {p : ENNReal} {q : ENNReal} (hp : p ∈ Set.Icc 1 q) :

q > 0

theorem ComputationsInterpolatedExponents.toReal_pos_of_Ioo {q : ENNReal} {p : ENNReal} {r : ENNReal} (hp : p ∈ Set.Ioo q r) :

p.toReal > 0

theorem ComputationsInterpolatedExponents.toReal_ne_zero_of_Ioo {q : ENNReal} {p : ENNReal} {r : ENNReal} (hp : p ∈ Set.Ioo q r) :

p.toReal ≠ 0

theorem ComputationsInterpolatedExponents.eq_of_rpow_eq (a : ENNReal) (b : ENNReal) (c : ℝ) (hc : c ≠ 0) (h : a ^ c = b ^ c) :

a = b

theorem ComputationsInterpolatedExponents.le_of_rpow_le {a : ENNReal} {b : ENNReal} {c : ℝ} (hc : c > 0) (h : a ^ c ≤ b ^ c) :

a ≤ b

theorem ComputationsInterpolatedExponents.coe_inv_exponent {p₀ : ENNReal} (hp₀ : p₀ > 0) :

ENNReal.ofReal p₀⁻¹.toReal = p₀⁻¹

theorem ComputationsInterpolatedExponents.inv_of_interpolated_pos' {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀p₁ : p₀ ≠ p₁) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

theorem ComputationsInterpolatedExponents.interpolated_pos' {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

0 < p

theorem ComputationsInterpolatedExponents.exp_toReal_pos {p₀ : ENNReal} (hp₀ : p₀ > 0) (hp₀' : p₀ ≠ ⊤) :

0 < p₀.toReal

theorem ComputationsInterpolatedExponents.interp_exp_in_Ioo_zero_top {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ ⊤ ∨ p₁ ≠ ⊤) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p ∈ Set.Ioo 0 ⊤

theorem ComputationsInterpolatedExponents.inv_toReal_pos_of_ne_top {p₀ : ENNReal} (hp₀ : p₀ > 0) (hp' : p₀ ≠ ⊤) :

p₀⁻¹.toReal > 0

theorem ComputationsInterpolatedExponents.inv_toReal_ne_zero_of_ne_top {p₀ : ENNReal} (hp₀ : p₀ > 0) (hp' : p₀ ≠ ⊤) :

p₀⁻¹.toReal ≠ 0

theorem ComputationsInterpolatedExponents.interp_exp_toReal_pos {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

0 < p.toReal

theorem ComputationsInterpolatedExponents.interp_exp_toReal_pos' {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hp₀p₁ : p₀ ≠ ⊤ ∨ p₁ ≠ ⊤) :

0 < p.toReal

theorem ComputationsInterpolatedExponents.interp_exp_inv_pos {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

0 < p⁻¹.toReal

theorem ComputationsInterpolatedExponents.interp_exp_inv_ne_zero {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p⁻¹.toReal ≠ 0

theorem ComputationsInterpolatedExponents.preservation_interpolation {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p⁻¹.toReal = (1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal

theorem ComputationsInterpolatedExponents.preservation_positivity_inv_toReal {p₀ : ENNReal} {p₁ : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) :

0 < (1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal

theorem ComputationsInterpolatedExponents.ne_inv_toReal_exponents {p₀ : ENNReal} {p₁ : ENNReal} (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) :

p₀⁻¹.toReal ≠ p₁⁻¹.toReal

theorem ComputationsInterpolatedExponents.ne_inv_toReal_exp_interp_exp {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p₀⁻¹.toReal ≠ p⁻¹.toReal

theorem ComputationsInterpolatedExponents.ne_sub_toReal_exp {p₀ : ENNReal} {p₁ : ENNReal} (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) :

p₁⁻¹.toReal - p₀⁻¹.toReal ≠ 0

theorem ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p₀.toReal ≠ p.toReal

theorem ComputationsInterpolatedExponents.ne_toReal_exp_interp_exp₁ {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p.toReal ≠ p₁.toReal

theorem ComputationsInterpolatedExponents.ofReal_inv_interp_sub_exp_pos₁ {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) :

ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ > 0

theorem ComputationsInterpolatedExponents.ofReal_inv_interp_sub_exp_pos₀ {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) :

ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ > 0

theorem ComputationsInterpolatedExponents.exp_lt_iff {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p < p₀ ↔ p₁ < p₀

theorem ComputationsInterpolatedExponents.exp_gt_iff {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p₀ < p ↔ p₀ < p₁

theorem ComputationsInterpolatedExponents.exp_lt_exp_gt_iff {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p < p₀ ↔ p₁ < p

theorem ComputationsInterpolatedExponents.exp_gt_exp_lt_iff {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p₀ < p ↔ p < p₁

theorem ComputationsInterpolatedExponents.exp_lt_iff₁ {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p < p₁ ↔ p₀ < p₁

theorem ComputationsInterpolatedExponents.exp_gt_iff₁ {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) :

p₁ < p ↔ p₁ < p₀

Results about the particular choice of exponent #

The proof of the real interpolation theorem will estimate
`distribution (trunc f A(t)) t` and `distribution (trunc_compl f A(t)) t` for a
function `A`. The function `A` can be given a closed-form expression that works for
_all_ cases in the real interpolation theorem, because of the computation rules available
for elements in `ℝ≥0∞` that avoid the need for a limiting procedure, e.g. `⊤⁻¹ = 0`.

The function `A` will be of the form `A(t) = (t / d) ^ σ` for particular choices of `d` and
`σ`. This section contatins results about the exponents `σ`.

def ComputationsChoiceExponent.ζ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} :

Equations

ComputationsChoiceExponent.ζ = ((1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal) * (q₁⁻¹.toReal - q₀⁻¹.toReal) / (((1 - t) * q₀⁻¹.toReal + t * q₁⁻¹.toReal) * (p₁⁻¹.toReal - p₀⁻¹.toReal))

Instances For

theorem ComputationsChoiceExponent.ζ_equality₁ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) :

ComputationsChoiceExponent.ζ = ((1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal) * ((1 - t) * q₀⁻¹.toReal + t * q₁⁻¹.toReal - q₀⁻¹.toReal) / (((1 - t) * q₀⁻¹.toReal + t * q₁⁻¹.toReal) * ((1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal - p₀⁻¹.toReal))

theorem ComputationsChoiceExponent.ζ_equality₂ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) :

ComputationsChoiceExponent.ζ = ((1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal) * ((1 - t) * q₀⁻¹.toReal + t * q₁⁻¹.toReal - q₁⁻¹.toReal) / (((1 - t) * q₀⁻¹.toReal + t * q₁⁻¹.toReal) * ((1 - t) * p₀⁻¹.toReal + t * p₁⁻¹.toReal - p₁⁻¹.toReal))

theorem ComputationsChoiceExponent.ζ_symm {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} :

ComputationsChoiceExponent.ζ = ComputationsChoiceExponent.ζ

theorem ComputationsChoiceExponent.ζ_equality₃ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) :

ComputationsChoiceExponent.ζ = p₀.toReal * (q₀.toReal - q.toReal) / (q₀.toReal * (p₀.toReal - p.toReal))

theorem ComputationsChoiceExponent.one_sub_coe_one_sub {t : ℝ} (ht : t ∈ Set.Ioo 0 1) :

1 - ENNReal.ofReal (1 - t) = ENNReal.ofReal t

theorem ComputationsChoiceExponent.coe_one_sub {t : ℝ} (ht : t ∈ Set.Ioo 0 1) :

ENNReal.ofReal (1 - t) = 1 - ENNReal.ofReal t

theorem ComputationsChoiceExponent.ζ_equality₄ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ ≠ ⊤) :

ComputationsChoiceExponent.ζ = p₁.toReal * (q₁.toReal - q.toReal) / (q₁.toReal * (p₁.toReal - p.toReal))

theorem ComputationsChoiceExponent.ζ_equality₅ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) :

p₀.toReal + ComputationsChoiceExponent.ζ⁻¹ * (q.toReal - q₀.toReal) * (p₀.toReal / q₀.toReal) = p.toReal

theorem ComputationsChoiceExponent.ζ_equality₆ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ ≠ ⊤) :

p₁.toReal + ComputationsChoiceExponent.ζ⁻¹ * (q.toReal - q₁.toReal) * (p₁.toReal / q₁.toReal) = p.toReal

theorem ComputationsChoiceExponent.ζ_equality₇ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ = ⊤) :

ComputationsChoiceExponent.ζ = p₀.toReal / (p₀.toReal - p.toReal)

theorem ComputationsChoiceExponent.ζ_equality₈ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ = ⊤) :

ComputationsChoiceExponent.ζ = p₁.toReal / (p₁.toReal - p.toReal)

theorem ComputationsChoiceExponent.ζ_eq_top_top {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₁' : p₁ = ⊤) (hq₁' : q₁ = ⊤) :

ComputationsChoiceExponent.ζ = 1

theorem ComputationsChoiceExponent.ζ_pos_iff_aux {p₀ : ENNReal} {q₀ : ENNReal} {p : ENNReal} {q : ENNReal} (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) :

0 < p₀.toReal * (q₀.toReal - q.toReal) / (q₀.toReal * (p₀.toReal - p.toReal)) ↔ q.toReal < q₀.toReal ∧ p.toReal < p₀.toReal ∨ q₀.toReal < q.toReal ∧ p₀.toReal < p.toReal

theorem ComputationsChoiceExponent.preservation_inequality {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hp₀' : p₀ ≠ ⊤) :

p.toReal < p₀.toReal ↔ p < p₀

theorem ComputationsChoiceExponent.preservation_inequality' {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ ≠ p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hp₀' : p₀ ≠ ⊤) :

p₀.toReal < p.toReal ↔ p₀ < p

theorem ComputationsChoiceExponent.preservation_inequality_of_lt₀ {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₀q₁ : q₀ < q₁) :

q₀.toReal < q.toReal

theorem ComputationsChoiceExponent.preservation_inequality_of_lt₁ {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₀q₁ : q₀ < q₁) (hq₁' : q₁ ≠ ⊤) :

q.toReal < q₁.toReal

theorem ComputationsChoiceExponent.ζ_pos_toReal_iff₀ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) :

0 < ComputationsChoiceExponent.ζ ↔ q.toReal < q₀.toReal ∧ p.toReal < p₀.toReal ∨ q₀.toReal < q.toReal ∧ p₀.toReal < p.toReal

theorem ComputationsChoiceExponent.ζ_pos_toReal_iff₁ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ ≠ ⊤) :

0 < ComputationsChoiceExponent.ζ ↔ q.toReal < q₁.toReal ∧ p.toReal < p₁.toReal ∨ q₁.toReal < q.toReal ∧ p₁.toReal < p.toReal

theorem ComputationsChoiceExponent.ζ_pos_iff_aux₀ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) :

0 < ComputationsChoiceExponent.ζ ↔ q₀⁻¹.toReal < q₁⁻¹.toReal ∧ p₀⁻¹.toReal < p₁⁻¹.toReal ∨ q₁⁻¹.toReal < q₀⁻¹.toReal ∧ p₁⁻¹.toReal < p₀⁻¹.toReal

theorem ComputationsChoiceExponent.inv_toReal_iff {p₀ : ENNReal} {p₁ : ENNReal} (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) :

p₀⁻¹.toReal < p₁⁻¹.toReal ↔ p₁ < p₀

theorem ComputationsChoiceExponent.ζ_pos_iff {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) :

0 < ComputationsChoiceExponent.ζ ↔ q₁ < q₀ ∧ p₁ < p₀ ∨ q₀ < q₁ ∧ p₀ < p₁

theorem ComputationsChoiceExponent.ζ_pos_iff' {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) :

0 < ComputationsChoiceExponent.ζ ↔ q < q₀ ∧ p < p₀ ∨ q₀ < q ∧ p₀ < p

theorem ComputationsChoiceExponent.ζ_pos_iff_of_lt₀ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) :

0 < ComputationsChoiceExponent.ζ ↔ q₀ < q

theorem ComputationsChoiceExponent.ζ_pos_iff_of_lt₁ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) :

0 < ComputationsChoiceExponent.ζ ↔ q < q₁

theorem ComputationsChoiceExponent.ζ_neg_iff_aux₀ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) :

ComputationsChoiceExponent.ζ < 0 ↔ q₀⁻¹.toReal < q₁⁻¹.toReal ∧ p₁⁻¹.toReal < p₀⁻¹.toReal ∨ q₁⁻¹.toReal < q₀⁻¹.toReal ∧ p₀⁻¹.toReal < p₁⁻¹.toReal

theorem ComputationsChoiceExponent.ζ_neg_iff {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) :

ComputationsChoiceExponent.ζ < 0 ↔ q₁ < q₀ ∧ p₀ < p₁ ∨ q₀ < q₁ ∧ p₁ < p₀

theorem ComputationsChoiceExponent.ζ_neg_iff' {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) :

ComputationsChoiceExponent.ζ < 0 ↔ q < q₀ ∧ p₀ < p ∨ q₀ < q ∧ p < p₀

theorem ComputationsChoiceExponent.ζ_neg_iff_of_lt₀ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) :

ComputationsChoiceExponent.ζ < 0 ↔ q < q₀

theorem ComputationsChoiceExponent.ζ_neg_iff_of_lt₁ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) :

ComputationsChoiceExponent.ζ < 0 ↔ q₁ < q

theorem ComputationsChoiceExponent.ζ_neg_iff_aux {p₀ : ENNReal} {q₀ : ENNReal} {p : ENNReal} {q : ENNReal} (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) :

p₀.toReal * (q₀.toReal - q.toReal) / (q₀.toReal * (p₀.toReal - p.toReal)) < 0 ↔ q.toReal < q₀.toReal ∧ p₀.toReal < p.toReal ∨ q₀.toReal < q.toReal ∧ p.toReal < p₀.toReal

theorem ComputationsChoiceExponent.ζ_neg_toReal_iff₀ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) :

ComputationsChoiceExponent.ζ < 0 ↔ q.toReal < q₀.toReal ∧ p₀.toReal < p.toReal ∨ q₀.toReal < q.toReal ∧ p.toReal < p₀.toReal

theorem ComputationsChoiceExponent.ζ_neg_toReal_iff₁ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ ≠ ⊤) :

ComputationsChoiceExponent.ζ < 0 ↔ q.toReal < q₁.toReal ∧ p₁.toReal < p.toReal ∨ q₁.toReal < q.toReal ∧ p.toReal < p₁.toReal

theorem ComputationsChoiceExponent.ζ_neg_iff₀ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ ≠ ⊤) :

ComputationsChoiceExponent.ζ < 0 ↔ q < q₀ ∧ p₀ < p ∨ q₀ < q ∧ p < p₀

theorem ComputationsChoiceExponent.ζ_ne_zero {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) :

ComputationsChoiceExponent.ζ ≠ 0

theorem ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₀ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) :

ComputationsChoiceExponent.ζ ≤ 0 ↔ q < q₀

theorem ComputationsChoiceExponent.ζ_le_zero_iff_of_lt₁ {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hp₀p₁' : p₀ < p₁) :

ComputationsChoiceExponent.ζ ≤ 0 ↔ q₁ < q

theorem ComputationsChoiceExponent.eq_exponents₀ {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) :

q₀.toReal + q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₀.toReal) = (1 - t) * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₂ {p₀ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) :

q₀.toReal / p₀.toReal + p₀⁻¹.toReal * q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₀.toReal) = (1 - t) * p₀⁻¹.toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₁ {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) :

q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₀.toReal) = -t * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₃ {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₀' : q₀ ≠ ⊤) :

p₁⁻¹.toReal * q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₀.toReal) = -t * p₁⁻¹.toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₄ {q₀ : ENNReal} {q₁ : ENNReal} :

q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) = -(q₀⁻¹.toReal / (q₀⁻¹.toReal - q₁⁻¹.toReal))

theorem ComputationsChoiceExponent.eq_exponents₅ {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) :

q₁.toReal + -(q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₁.toReal)) = t * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₆ {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) :

q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₁.toReal) = (1 - t) * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₇ {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) :

q₁.toReal / p₁.toReal + -(p₁⁻¹.toReal * q₀⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₁.toReal)) = t * p₁⁻¹.toReal * q.toReal

theorem ComputationsChoiceExponent.eq_exponents₈ {p₀ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀ : q₀ > 0) (hq₁ : q₁ > 0) (hq₀q₁ : q₀ ≠ q₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hq₁' : q₁ ≠ ⊤) :

p₀⁻¹.toReal * q₁⁻¹.toReal / (q₁⁻¹.toReal - q₀⁻¹.toReal) * (q.toReal - q₁.toReal) = (1 - t) * p₀⁻¹.toReal * q.toReal

Interface for using cutoff functions #

structure ScaledPowerFunction :

A ScaledPowerFunction is meant to represent a function of the form t ↦ (t / d)^σ, where d is strictly positive and either σ > 0 or σ < 0.

σ : ℝ
d : ℝ
hd : self.d > 0
hσ : self.σ > 0 ∨ self.σ < 0

Instances For

theorem ScaledPowerFunction.hd (self : ScaledPowerFunction) :

self.d > 0

theorem ScaledPowerFunction.hσ (self : ScaledPowerFunction) :

self.σ > 0 ∨ self.σ < 0

structure ToneCouple :

A ToneCouple is an couple of two monotone functions that are practically inverses of each other. It is used in the proof of the real interpolation theorem.

Note: originally it seemed useful to make the possible choice of this function general in the proof of the real inteprolation theorem. However, in the end really only one function works for all the different cases. This infrastructure, however, could potentially still be useful, if one would like to try to improve the constant.

ton : ℝ → ℝ
inv : ℝ → ℝ
mon : Bool
ton_is_ton : if self.mon = true then StrictMonoOn self.ton (Set.Ioi 0) else StrictAntiOn self.ton (Set.Ioi 0)
ran_ton : ∀ t ∈ Set.Ioi 0, self.ton t ∈ Set.Ioi 0
ran_inv : ∀ t ∈ Set.Ioi 0, self.inv t ∈ Set.Ioi 0
inv_pf : if self.mon = true then ∀ s ∈ Set.Ioi 0, ∀ t ∈ Set.Ioi 0, (self.ton s < t ↔ s < self.inv t) ∧ (t < self.ton s ↔ self.inv t < s) else ∀ s ∈ Set.Ioi 0, ∀ t ∈ Set.Ioi 0, (self.ton s < t ↔ self.inv t < s) ∧ (t < self.ton s ↔ s < self.inv t)

Instances For

theorem ToneCouple.ton_is_ton (self : ToneCouple) :

if self.mon = true then StrictMonoOn self.ton (Set.Ioi 0) else StrictAntiOn self.ton (Set.Ioi 0)

theorem ToneCouple.ran_ton (self : ToneCouple) (t : ℝ) :

t ∈ Set.Ioi 0 → self.ton t ∈ Set.Ioi 0

theorem ToneCouple.ran_inv (self : ToneCouple) (t : ℝ) :

t ∈ Set.Ioi 0 → self.inv t ∈ Set.Ioi 0

theorem ToneCouple.inv_pf (self : ToneCouple) :

if self.mon = true then ∀ s ∈ Set.Ioi 0, ∀ t ∈ Set.Ioi 0, (self.ton s < t ↔ s < self.inv t) ∧ (t < self.ton s ↔ self.inv t < s) else ∀ s ∈ Set.Ioi 0, ∀ t ∈ Set.Ioi 0, (self.ton s < t ↔ self.inv t < s) ∧ (t < self.ton s ↔ s < self.inv t)

def spf_to_tc (spf : ScaledPowerFunction) :

A scaled power function gives rise to a ToneCouple.

Equations

One or more equations did not get rendered due to their size.

Instances For

Results about the particular choice of scale #

The proof of the real interpolation theorem will estimate
`distribution (trunc f A(t)) t` and `distribution (trunc_compl f A(t)) t` for a
function `A`. The function `A` can be given a closed-form expression that works for
_all_ cases in the real interpolation theorem, because of the computation rules available
for elements in `ℝ≥0∞` that avoid the need for a limiting procedure, e.g. `⊤⁻¹ = 0`.

The function `A` will be of the form `A(t) = (t / d) ^ σ` for particular choices of `d` and
`σ`. This section contatins results about the scale `d`.

def ChoiceScale.d {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} :

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem ChoiceScale.d_pos_aux₀ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

0 < MeasureTheory.eLpNorm f p μ ^ p.toReal

theorem ChoiceScale.d_ne_top_aux₀ {b : ℝ} {F : ENNReal} (hF : F ∈ Set.Ioo 0 ⊤) :

theorem ChoiceScale.d_ne_zero_aux₀ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} {b : ℝ} (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

(MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ b ≠ 0

theorem ChoiceScale.d_ne_zero_aux₁ {C : NNReal} {c : ℝ} (hC : C > 0) :

↑C ^ c ≠ 0

theorem ChoiceScale.d_ne_zero_aux₂ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} {C : NNReal} {b : ℝ} {c : ℝ} (hC : C > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

↑C ^ c * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ b ≠ 0

theorem ChoiceScale.d_ne_top_aux₁ {C : NNReal} {c : ℝ} (hC : C > 0) :

↑C ^ c ≠ ⊤

theorem ChoiceScale.d_ne_top_aux₂ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} {b : ℝ} (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

(MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ b ≠ ⊤

theorem ChoiceScale.d_ne_top_aux₃ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} {C : NNReal} {b : ℝ} {c : ℝ} (hC : C > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

↑C ^ c * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ b ≠ ⊤

theorem ChoiceScale.d_ne_zero_aux₃ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} {b₀ : ℝ} {c₀ : ℝ} {b₁ : ℝ} {c₁ : ℝ} (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

↑C₀ ^ c₀ * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ b₀ / (↑C₁ ^ c₁ * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ b₁) ≠ 0

theorem ChoiceScale.d_ne_top_aux₄ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} {b₀ : ℝ} {c₀ : ℝ} {b₁ : ℝ} {c₁ : ℝ} (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

↑C₀ ^ c₀ * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ b₀ / (↑C₁ ^ c₁ * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ b₁) ≠ ⊤

theorem ChoiceScale.d_pos {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

ChoiceScale.d > 0

theorem ChoiceScale.d_eq_top₀ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} (hp₀ : p₀ > 0) (hq₁ : q₁ > 0) (hp₀' : p₀ ≠ ⊤) (hq₀' : q₀ = ⊤) (hq₀q₁ : q₀ ≠ q₁) :

ChoiceScale.d = (↑C₀ ^ p₀.toReal * MeasureTheory.eLpNorm f p μ ^ p.toReal).toReal ^ p₀.toReal⁻¹

theorem ChoiceScale.d_eq_top₁ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hp₁' : p₁ ≠ ⊤) (hq₁' : q₁ = ⊤) (hq₀q₁ : q₀ ≠ q₁) (hC₁ : C₁ > 0) :

ChoiceScale.d = (↑C₁ ^ p₁.toReal * MeasureTheory.eLpNorm f p μ ^ p.toReal).toReal ^ p₁.toReal⁻¹

theorem ChoiceScale.d_eq_top_of_eq {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} (hC₁ : C₁ > 0) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hq₀' : q₀ ≠ ⊤) (hp₀' : p₀ ≠ ⊤) (hp₁ : p₁ > 0) (hp₀p₁ : p₀ = p₁) (hpp₀ : p = p₀) (hq₁' : q₁ = ⊤) :

ChoiceScale.d = (↑C₁ * MeasureTheory.eLpNorm f p μ).toReal

theorem ChoiceScale.d_eq_top_top {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} (hq₀ : q₀ > 0) (hq₀q₁ : q₀ ≠ q₁) (hp₁' : p₁ = ⊤) (hq₁' : q₁ = ⊤) :

ChoiceScale.d = ↑C₁

def ChoiceScale.spf_ch {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E₁] {f : α → E₁} {t : ℝ} (ht : t ∈ Set.Ioo 0 1) (hq₀q₁ : q₀ ≠ q₁) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁) (hp₀p₁ : p₀ ≠ p₁) (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

ScaledPowerFunction

The particular choice of scaled power function that works in the proof of the real interpolation theorem.

Equations

ChoiceScale.spf_ch ht hq₀q₁ hp₀ hq₀ hp₁ hq₁ hp₀p₁ hC₀ hC₁ hF = { σ := ComputationsChoiceExponent.ζ, d := ChoiceScale.d, hd := ⋯, hσ := ⋯ }

Instances For

Some tools for measure theory computations #

A collection of small lemmas to help with integral manipulations.

theorem MeasureTheory.lintegral_double_restrict_set {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {A : Set α} {B : Set α} {f : α → ENNReal} (hA : MeasurableSet A) (hB : MeasurableSet B) (hf : ∀ᵐ (x : α) ∂μ, x ∈ A \ B → f x ≤ 0) :

∫⁻ (x : α) in A, f x ∂μ = ∫⁻ (x : α) in A ∩ B, f x ∂μ

theorem MeasureTheory.measure_preserving_shift {a : ℝ} :

MeasureTheory.MeasurePreserving (fun (x : ℝ) => a + x) MeasureTheory.volume MeasureTheory.volume

theorem MeasureTheory.measureable_embedding_shift {a : ℝ} :

MeasurableEmbedding fun (x : ℝ) => a + x

theorem MeasureTheory.measure_preserving_scaling {a : ℝ} (ha : a ≠ 0) :

MeasureTheory.MeasurePreserving (fun (x : ℝ) => a * x) MeasureTheory.volume (ENNReal.ofReal |a⁻¹| • MeasureTheory.volume)

theorem MeasureTheory.lintegral_shift (f : ℝ → ENNReal) {a : ℝ} :

∫⁻ (x : ℝ), f (x + a) = ∫⁻ (x : ℝ), f x

theorem MeasureTheory.lintegral_shift' (f : ℝ → ENNReal) {a : ℝ} {s : Set ℝ} :

∫⁻ (x : ℝ) in (fun (z : ℝ) => z + a) ⁻¹' s, f (x + a) = ∫⁻ (x : ℝ) in s, f x

theorem MeasureTheory.lintegral_add_right_Ioi (f : ℝ → ENNReal) {a : ℝ} {b : ℝ} :

∫⁻ (x : ℝ) in Set.Ioi (b - a), f (x + a) = ∫⁻ (x : ℝ) in Set.Ioi b, f x

theorem MeasureTheory.lintegral_scale_constant (f : ℝ → ENNReal) {a : ℝ} (h : a ≠ 0) :

∫⁻ (x : ℝ), f (a * x) = ENNReal.ofReal |a⁻¹| * ∫⁻ (x : ℝ), f x

theorem MeasureTheory.lintegral_scale_constant_preimage (f : ℝ → ENNReal) {a : ℝ} (h : a ≠ 0) {s : Set ℝ} :

∫⁻ (x : ℝ) in (fun (z : ℝ) => a * z) ⁻¹' s, f (a * x) = ENNReal.ofReal |a⁻¹| * ∫⁻ (x : ℝ) in s, f x

theorem MeasureTheory.lintegral_scale_constant_halfspace (f : ℝ → ENNReal) {a : ℝ} (h : 0 < a) :

∫⁻ (x : ℝ) in Set.Ioi 0, f (a * x) = ENNReal.ofReal |a⁻¹| * ∫⁻ (x : ℝ) in Set.Ioi 0, f x

theorem MeasureTheory.lintegral_scale_constant_halfspace' {f : ℝ → ENNReal} {a : ℝ} (h : 0 < a) :

ENNReal.ofReal |a| * ∫⁻ (x : ℝ) in Set.Ioi 0, f (a * x) = ∫⁻ (x : ℝ) in Set.Ioi 0, f x

theorem MeasureTheory.lintegral_scale_constant' {f : ℝ → ENNReal} {a : ℝ} (h : a ≠ 0) :

ENNReal.ofReal |a| * ∫⁻ (x : ℝ), f (a * x) = ∫⁻ (x : ℝ), f x

theorem MeasureTheory.lintegral_rw_aux {g : ℝ → ENNReal} {f₁ : ℝ → ENNReal} {f₂ : ℝ → ENNReal} {A : Set ℝ} (heq : f₁ =ᵐ[MeasureTheory.volume.restrict A] f₂) :

∫⁻ (s : ℝ) in A, g s * f₁ s = ∫⁻ (s : ℝ) in A, g s * f₂ s

theorem MeasureTheory.power_aux {p : ℝ} {q : ℝ} :

(fun (s : ℝ) => ENNReal.ofReal s ^ (p + q)) =ᵐ[MeasureTheory.volume.restrict (Set.Ioi 0)] fun (s : ℝ) => ENNReal.ofReal s ^ p * ENNReal.ofReal s ^ q

theorem MeasureTheory.power_aux_2 {p : ℝ} {q : ℝ} :

(fun (s : ℝ) => ENNReal.ofReal (s ^ (p + q))) =ᵐ[MeasureTheory.volume.restrict (Set.Ioi 0)] fun (s : ℝ) => ENNReal.ofReal (s ^ p) * ENNReal.ofReal (s ^ q)

theorem MeasureTheory.ofReal_rpow_of_pos_aux {p : ℝ} :

(fun (s : ℝ) => ENNReal.ofReal s ^ p) =ᵐ[MeasureTheory.volume.restrict (Set.Ioi 0)] fun (s : ℝ) => ENNReal.ofReal (s ^ p)

theorem MeasureTheory.extract_constant_double_integral_rpow {f : ℝ → ℝ → ENNReal} {q : ℝ} (hq : q ≥ 0) {a : ENNReal} (ha : a ≠ ⊤) :

∫⁻ (s : ℝ) in Set.Ioi 0, (∫⁻ (t : ℝ) in Set.Ioi 0, a * f s t) ^ q = a ^ q * ∫⁻ (s : ℝ) in Set.Ioi 0, (∫⁻ (t : ℝ) in Set.Ioi 0, f s t) ^ q

theorem MeasureTheory.ofReal_rpow_rpow_aux {p : ℝ} :

(fun (s : ℝ) => ENNReal.ofReal s ^ p) =ᵐ[MeasureTheory.volume.restrict (Set.Ioi 0)] fun (s : ℝ) => ENNReal.ofReal (s ^ p)

theorem MeasureTheory.lintegral_rpow_of_gt {β : ℝ} {γ : ℝ} (hβ : β > 0) (hγ : γ > -1) :

∫⁻ (s : ℝ) in Set.Ioo 0 β, ENNReal.ofReal (s ^ γ) = ENNReal.ofReal (β ^ (γ + 1) / (γ + 1))

Results about truncations of a function #

def MeasureTheory.trunc {α : Type u_1} {E₁ : Type u_4} [NormedAddCommGroup E₁] (f : α → E₁) (t : ℝ) (x : α) :

E₁

The t-truncation of a function f.

Equations

MeasureTheory.trunc f t x = if ‖f x‖ ≤ t then f x else 0

Instances For

def MeasureTheory.trunc_compl {α : Type u_1} {E₁ : Type u_4} [NormedAddCommGroup E₁] (f : α → E₁) (t : ℝ) :

α → E₁

The complement of a t-truncatoin of a function f.

Equations

MeasureTheory.trunc_compl f t = f - MeasureTheory.trunc f t

Instances For

theorem MeasureTheory.trunc_compl_eq {α : Type u_1} {E₁ : Type u_4} [NormedAddCommGroup E₁] {a : ℝ} {f : α → E₁} :

f - MeasureTheory.trunc f a = fun (x : α) => if a < ‖f x‖ then f x else 0

def MeasureTheory.trnc {α : Type u_1} {E₁ : Type u_4} [NormedAddCommGroup E₁] (j : Bool) (f : α → E₁) (t : ℝ) :

α → E₁

A function to deal with truncations and complement of truncations in one go.

Equations

MeasureTheory.trnc false f t = f - MeasureTheory.trunc f t
MeasureTheory.trnc true f t = MeasureTheory.trunc f t

Instances For

theorem MeasureTheory.trunc_buildup {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {t : ℝ} [NormedAddCommGroup E₁] :

f = MeasureTheory.trunc f t + MeasureTheory.trunc_compl f t

A function is the complement if its truncation and the complement of the truncation.

theorem MeasureTheory.trunc_of_nonpos {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {a : ℝ} [NormedAddCommGroup E₁] (ha : a ≤ 0) :

MeasureTheory.trunc f a = 0

If the truncation parameter is non-positive, the truncation vanishes.

theorem MeasureTheory.trunc_compl_of_nonpos {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {a : ℝ} [NormedAddCommGroup E₁] (ha : a ≤ 0) :

MeasureTheory.trunc_compl f a = f

If the truncation parameter is non-positive, the complement of the truncation is the function itself.

Measurability properties of truncations #

theorem MeasureTheory.StronglyMeasurable.trunc {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {f : α → E₁} {t : ℝ} [NormedAddCommGroup E₁] (hf : MeasureTheory.StronglyMeasurable f) :

MeasureTheory.StronglyMeasurable (MeasureTheory.trunc f t)

theorem MeasureTheory.StronglyMeasurable.trunc_compl {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {f : α → E₁} {t : ℝ} [NormedAddCommGroup E₁] (hf : MeasureTheory.StronglyMeasurable f) :

MeasureTheory.StronglyMeasurable (f - MeasureTheory.trunc f t)

theorem MeasureTheory.aestronglyMeasurable_trunc {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} [NormedAddCommGroup E₁] (hf : MeasureTheory.AEStronglyMeasurable f μ) :

MeasureTheory.AEStronglyMeasurable (MeasureTheory.trunc f t) μ

theorem MeasureTheory.aestronglyMeasurable_trunc_compl {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} [NormedAddCommGroup E₁] (hf : MeasureTheory.AEStronglyMeasurable f μ) :

MeasureTheory.AEStronglyMeasurable (f - MeasureTheory.trunc f t) μ

theorem MeasureTheory.aestronglyMeasurable_trnc {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} {j : Bool} [NormedAddCommGroup E₁] (hf : MeasureTheory.AEStronglyMeasurable f μ) :

MeasureTheory.AEStronglyMeasurable (MeasureTheory.trnc j f t) μ

theorem MeasureTheory.trunc_le {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {a : ℝ} [NormedAddCommGroup E₁] (x : α) :

‖MeasureTheory.trunc f a x‖ ≤ max 0 a

theorem MeasureTheory.coe_coe_eq_ofReal (a : ℝ) :

↑a.toNNReal = ENNReal.ofReal a

A small lemma that is helpful for rewriting

theorem MeasureTheory.trunc_eLpNormEssSup_le {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {a : ℝ} [NormedAddCommGroup E₁] :

MeasureTheory.eLpNormEssSup (MeasureTheory.trunc f a) μ ≤ ENNReal.ofReal (max 0 a)

theorem MeasureTheory.trunc_mono {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {a : ℝ} {b : ℝ} [NormedAddCommGroup E₁] (hab : a ≤ b) {x : α} :

‖MeasureTheory.trunc f a x‖ ≤ ‖MeasureTheory.trunc f b x‖

theorem MeasureTheory.norm_trunc_mono {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} [NormedAddCommGroup E₁] :

Monotone fun (s : ℝ) => MeasureTheory.eLpNorm (MeasureTheory.trunc f s) p μ

The norm of the truncation is monotone in the truncation parameter

theorem MeasureTheory.trunc_buildup_norm {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {a : ℝ} {x : α} [NormedAddCommGroup E₁] :

‖MeasureTheory.trunc f a x‖ + ‖(f - MeasureTheory.trunc f a) x‖ = ‖f x‖

theorem MeasureTheory.trunc_le_func {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {a : ℝ} {x : α} [NormedAddCommGroup E₁] :

‖MeasureTheory.trunc f a x‖ ≤ ‖f x‖

theorem MeasureTheory.trunc_compl_le_func {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {a : ℝ} {x : α} [NormedAddCommGroup E₁] :

‖(f - MeasureTheory.trunc f a) x‖ ≤ ‖f x‖

theorem MeasureTheory.trunc_compl_anti {α : Type u_1} {E₁ : Type u_4} {f : α → E₁} {a : ℝ} {b : ℝ} {x : α} [NormedAddCommGroup E₁] (hab : a ≤ b) :

‖(f - MeasureTheory.trunc f b) x‖ ≤ ‖(f - MeasureTheory.trunc f a) x‖

theorem MeasureTheory.norm_trunc_compl_anti {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} [NormedAddCommGroup E₁] :

Antitone fun (s : ℝ) => MeasureTheory.eLpNorm (f - MeasureTheory.trunc f s) p μ

The norm of the complement of the truncation is antitone in the truncation parameter

theorem MeasureTheory.norm_trunc_measurable {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} [NormedAddCommGroup E₁] :

Measurable fun (s : ℝ) => MeasureTheory.eLpNorm (MeasureTheory.trunc f s) p μ

The norm of the truncation is meaurable in the truncation parameter

theorem MeasureTheory.norm_trunc_compl_measurable {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} [NormedAddCommGroup E₁] :

Measurable fun (s : ℝ) => MeasureTheory.eLpNorm (f - MeasureTheory.trunc f s) p μ

The norm of the complement of the truncation is measurable in the truncation parameter

theorem MeasureTheory.trnc_le_func {α : Type u_1} {E₁ : Type u_4} {j : Bool} {f : α → E₁} {a : ℝ} {x : α} [NormedAddCommGroup E₁] :

‖MeasureTheory.trnc j f a x‖ ≤ ‖f x‖

Truncations and L-p spaces #

theorem MeasureTheory.power_estimate {a : ℝ} {b : ℝ} {t : ℝ} {γ : ℝ} (hγ : γ > 0) (htγ : γ ≤ t) (hab : a ≤ b) :

(t / γ) ^ a ≤ (t / γ) ^ b

theorem MeasureTheory.power_estimate' {a : ℝ} {b : ℝ} {t : ℝ} {γ : ℝ} (ht : t > 0) (htγ : t ≤ γ) (hab : a ≤ b) :

(t / γ) ^ b ≤ (t / γ) ^ a

theorem MeasureTheory.rpow_le_rpow_of_exponent_le_base_le {a : ℝ} {b : ℝ} {t : ℝ} {γ : ℝ} (ht : t > 0) (htγ : t ≤ γ) (hab : a ≤ b) :

ENNReal.ofReal (t ^ b) ≤ ENNReal.ofReal (t ^ a) * ENNReal.ofReal (γ ^ (b - a))

theorem MeasureTheory.rpow_le_rpow_of_exponent_le_base_ge {a : ℝ} {b : ℝ} {t : ℝ} {γ : ℝ} (hγ : γ > 0) (htγ : γ ≤ t) (hab : a ≤ b) :

ENNReal.ofReal (t ^ a) ≤ ENNReal.ofReal (t ^ b) * ENNReal.ofReal (γ ^ (a - b))

theorem MeasureTheory.trunc_preserves_Lp {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {p : ENNReal} {a : ℝ} [NormedAddCommGroup E₁] (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.Memℒp (MeasureTheory.trunc f a) p μ

theorem MeasureTheory.trunc_compl_preserves_Lp {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {p : ENNReal} {a : ℝ} [NormedAddCommGroup E₁] (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.Memℒp (f - MeasureTheory.trunc f a) p μ

theorem MeasureTheory.estimate_eLpNorm_trunc_compl {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {a : ℝ} {μ : MeasureTheory.Measure α} {f : α → E₁} {p : ENNReal} {q : ENNReal} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] (hp : p ≠ ⊤) (hpq : q ∈ Set.Ioo 0 p) (hf : AEMeasurable f μ) (ha : a > 0) :

MeasureTheory.eLpNorm (f - MeasureTheory.trunc f a) q μ ^ q.toReal ≤ ENNReal.ofReal (a ^ (q.toReal - p.toReal)) * MeasureTheory.eLpNorm f p μ ^ p.toReal

theorem MeasureTheory.estimate_eLpNorm_trunc {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {a : ℝ} {μ : MeasureTheory.Measure α} {f : α → E₁} {p : ENNReal} {q : ENNReal} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] (hq : q ≠ ⊤) (hpq : p ∈ Set.Ioo 0 q) (hf : AEMeasurable f μ) :

MeasureTheory.eLpNorm (MeasureTheory.trunc f a) q μ ^ q.toReal ≤ ENNReal.ofReal (a ^ (q.toReal - p.toReal)) * MeasureTheory.eLpNorm f p μ ^ p.toReal

theorem MeasureTheory.trunc_Lp_Lq_higher {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {a : ℝ} {μ : MeasureTheory.Measure α} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] (hpq : p ∈ Set.Ioo 0 q) (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.Memℒp (MeasureTheory.trnc ⊤ f a) q μ

If f is in Lp, the truncation is element of Lq for q > p.

theorem MeasureTheory.trunc_compl_Lp_Lq_lower {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {a : ℝ} {μ : MeasureTheory.Measure α} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] (hp : p ≠ ⊤) (hpq : q ∈ Set.Ioo 0 p) (ha : a > 0) (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.Memℒp (MeasureTheory.trnc ⊥ f a) q μ

If f is in Lp, the complement of the truncation is in Lq for q < p.

Some results about the integrals of truncations #

def MeasureTheory.res (j : Bool) (β : ℝ) :

Equations

MeasureTheory.res j β = if j = true then Set.Ioo 0 β else Set.Ioi β

Instances For

theorem MeasureTheory.measurableSet_res {j : Bool} {β : ℝ} :

MeasurableSet (MeasureTheory.res j β)

theorem MeasureTheory.res_subset_Ioi {j : Bool} {β : ℝ} (hβ : β > 0) :

MeasureTheory.res j β ⊆ Set.Ioi 0

instance MeasureTheory.decidableMemRes {t : ℝ} {j : Bool} {β : ℝ} :

Decidable (t ∈ MeasureTheory.res j β)

Equations

MeasureTheory.decidableMemRes = Classical.propDecidable (t ∈ MeasureTheory.res j β)

def MeasureTheory.res' (j : Bool) (β : ℝ) :

Equations

MeasureTheory.res' j β = if j = true then Set.Ioc 0 β else Set.Ici β

Instances For

theorem MeasureTheory.res'comp (j : Bool) (β : ℝ) (hβ : β > 0) :

Set.Ioi 0 \ MeasureTheory.res' j β = MeasureTheory.res (decide ¬j = true) β

theorem MeasureTheory.measurableSet_res' {j : Bool} {β : ℝ} :

MeasurableSet (MeasureTheory.res' j β)

theorem MeasureTheory.res'subset_Ioi {j : Bool} {β : ℝ} (hβ : β > 0) :

MeasureTheory.res' j β ⊆ Set.Ioi 0

theorem MeasureTheory.lintegral_trunc_mul₀ {α : Type u_1} {E₁ : Type u_4} [NormedAddCommGroup E₁] {f : α → E₁} {g : ℝ → ENNReal} {j : Bool} {x : α} {tc : ToneCouple} {p : ℝ} (hp : p > 0) (hfx : ‖f x‖₊ > 0) :

∫⁻ (s : ℝ) in Set.Ioi 0, g s * ↑‖MeasureTheory.trnc j f (tc.ton s) x‖₊ ^ p = ∫⁻ (s : ℝ) in MeasureTheory.res' (xor j tc.mon) (tc.inv ‖f x‖), g s * ↑‖MeasureTheory.trnc j f (tc.ton s) x‖₊ ^ p

theorem MeasureTheory.lintegral_trunc_mul₁ {α : Type u_1} {E₁ : Type u_4} [NormedAddCommGroup E₁] {f : α → E₁} {g : ℝ → ENNReal} {j : Bool} {x : α} {p : ℝ} {tc : ToneCouple} :

∫⁻ (s : ℝ) in MeasureTheory.res' (xor j tc.mon) (tc.inv ‖f x‖), g s * ↑‖MeasureTheory.trnc j f (tc.ton s) x‖₊ ^ p = ∫⁻ (s : ℝ) in MeasureTheory.res (xor j tc.mon) (tc.inv ‖f x‖), g s * ↑‖MeasureTheory.trnc j f (tc.ton s) x‖₊ ^ p

theorem MeasureTheory.lintegral_trunc_mul₂ {α : Type u_1} {E₁ : Type u_4} [NormedAddCommGroup E₁] {f : α → E₁} {g : ℝ → ENNReal} {j : Bool} {x : α} {p : ℝ} {tc : ToneCouple} (hfx : ‖f x‖ > 0) :

∫⁻ (s : ℝ) in MeasureTheory.res (xor j tc.mon) (tc.inv ‖f x‖), g s * ↑‖MeasureTheory.trnc j f (tc.ton s) x‖₊ ^ p = ∫⁻ (s : ℝ) in MeasureTheory.res (xor j tc.mon) (tc.inv ‖f x‖), g s * ↑‖f x‖₊ ^ p

theorem MeasureTheory.lintegral_trunc_mul {α : Type u_1} {E₁ : Type u_4} [NormedAddCommGroup E₁] {f : α → E₁} {g : ℝ → ENNReal} {j : Bool} {x : α} {tc : ToneCouple} {p : ℝ} (hp : p > 0) (hfx : ‖f x‖₊ > 0) :

∫⁻ (s : ℝ) in Set.Ioi 0, g s * ↑‖MeasureTheory.trnc j f (tc.ton s) x‖₊ ^ p = (∫⁻ (s : ℝ) in MeasureTheory.res (xor j tc.mon) (tc.inv ‖f x‖), g s) * ↑‖f x‖₊ ^ p

Extract expressions for the lower Lebesgue integral of power functions

theorem MeasureTheory.lintegral_rpow_of_gt_abs {β : ℝ} {γ : ℝ} (hβ : β > 0) (hγ : γ > -1) :

∫⁻ (s : ℝ) in Set.Ioo 0 β, ENNReal.ofReal (s ^ γ) = ENNReal.ofReal (β ^ (γ + 1) / |γ + 1|)

theorem MeasureTheory.lintegral_Ioi_rpow_of_lt_abs {β : ℝ} {σ : ℝ} (hβ : β > 0) (hσ : σ < -1) :

∫⁻ (s : ℝ) in Set.Ioi β, ENNReal.ofReal (s ^ σ) = ENNReal.ofReal (β ^ (σ + 1) / |σ + 1|)

theorem MeasureTheory.lintegral_rpow_abs {j : Bool} {tc : ToneCouple} {γ : ℝ} {t : ℝ} (hγ : if xor j tc.mon = true then γ > -1 else γ < -1) (ht : t > 0) :

∫⁻ (s : ℝ) in MeasureTheory.res (xor j tc.mon) (tc.inv t), ENNReal.ofReal s ^ γ = ENNReal.ofReal (tc.inv t ^ (γ + 1) / |γ + 1|)

theorem MeasureTheory.value_lintegral_res₀ {j : Bool} {β : ℝ} {γ : ℝ} {tc : ToneCouple} (hβ : β > 0) (hγ : if xor j tc.mon = true then γ > -1 else γ < -1) :

∫⁻ (s : ℝ) in MeasureTheory.res (xor j tc.mon) β, ENNReal.ofReal (s ^ γ) = ENNReal.ofReal (β ^ (γ + 1) / |γ + 1|)

theorem MeasureTheory.value_lintegral_res₁ {t : ℝ} {γ : ℝ} {p' : ℝ} {spf : ScaledPowerFunction} (ht : t > 0) :

ENNReal.ofReal ((spf_to_tc spf).inv t ^ (γ + 1) / |γ + 1|) * ENNReal.ofReal (t ^ p') = ENNReal.ofReal (spf.d ^ (γ + 1) * t ^ (spf.σ⁻¹ * (γ + 1) + p') / |γ + 1|)

Minkowski's integral inequality #

theorem MeasureTheory.rpow_add_of_pos (a : ENNReal) (c : ℝ) (d : ℝ) (hc : c > 0) (hd : d > 0) :

a ^ (c + d) = a ^ c * a ^ d

theorem MeasureTheory.eq_of_le_of_le (a : ENNReal) (b : ENNReal) (hab : a ≤ b) (hab' : b ≤ a) :

a = b

def MeasureTheory.trunc_cut {α : Type u_1} {m : MeasurableSpace α} (f : α → ENNReal) (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] (n : ℕ) (x : α) :

Equations

MeasureTheory.trunc_cut f μ n = (MeasureTheory.spanningSets μ n).indicator fun (x : α) => min (f x) ↑n

Instances For

theorem MeasureTheory.trunc_cut_mono {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ENNReal} (x : α) :

Monotone fun (n : ℕ) => MeasureTheory.trunc_cut f μ n x

theorem MeasureTheory.trunc_cut_mono₀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ENNReal} :

Monotone (MeasureTheory.trunc_cut f μ)

theorem MeasureTheory.trunc_cut_sup {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ENNReal} (x : α) :

⨆ (n : ℕ), MeasureTheory.trunc_cut f μ n x = f x

theorem MeasureTheory.representationLp {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] {f : α → ENNReal} (hf : AEMeasurable f μ) {p : ℝ} {q : ℝ} (hp : p > 1) (hq : q ≥ 1) (hpq : p⁻¹ + q⁻¹ = 1) :

(∫⁻ (x : α), f x ^ p ∂μ) ^ (1 / p) = ⨆ g ∈ {g' : α → ENNReal | AEMeasurable g' μ ∧ ∫⁻ (x : α), g' x ^ q ∂μ ≤ 1}, ∫⁻ (x : α), f x * g x ∂μ

Characterization of ∫⁻ x : α, f x ^ p ∂μ by a duality argument.

theorem MeasureTheory.aemeasurability_prod₁ {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] ⦃f : α × β → ENNReal⦄ (hf : AEMeasurable f (μ.prod ν)) :

∀ᵐ (x : α) ∂μ, AEMeasurable (f ∘ Prod.mk x) ν

theorem MeasureTheory.aemeasurability_prod₂ {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] ⦃f : α × β → ENNReal⦄ (hf : AEMeasurable f (μ.prod ν)) :

∀ᵐ (y : β) ∂ν, AEMeasurable (f ∘ fun (x : α) => (x, y)) μ

theorem MeasureTheory.aemeasurability_integral_component {α : Type u_1} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] ⦃f : α × β → ENNReal⦄ (hf : AEMeasurable f (μ.prod ν)) :

AEMeasurable (fun (x : α) => ∫⁻ (y : β), f (x, y) ∂ν) μ

theorem MeasureTheory.lintegral_lintegral_pow_swap {α : Type u_1} {β : Type u_3} {p : ℝ} (hp : 1 ≤ p) [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SigmaFinite μ] ⦃f : α → β → ENNReal⦄ (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :

(∫⁻ (x : α), (∫⁻ (y : β), f x y ∂ν) ^ p ∂μ) ^ p⁻¹ ≤ ∫⁻ (y : β), (∫⁻ (x : α), f x y ^ p ∂μ) ^ p⁻¹ ∂ν

Minkowsi's integral inequality

theorem MeasureTheory.lintegral_lintegral_pow_swap_rpow {α : Type u_1} {β : Type u_3} {p : ℝ} (hp : p ≥ 1) [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SigmaFinite μ] ⦃f : α → β → ENNReal⦄ (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :

∫⁻ (x : α), (∫⁻ (y : β), f x y ∂ν) ^ p ∂μ ≤ (∫⁻ (y : β), (∫⁻ (x : α), f x y ^ p ∂μ) ^ p⁻¹ ∂ν) ^ p

Apply Minkowski's integral inequality to truncations #

theorem MeasureTheory.ton_aeMeasurable (tc : ToneCouple) :

AEMeasurable tc.ton (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem MeasureTheory.indicator_ton_measurable {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasureTheory.SigmaFinite μ] (hg : AEMeasurable g μ) (tc : ToneCouple) :

MeasureTheory.NullMeasurableSet {(s, x) : ℝ × α | ↑‖g x‖₊ ≤ tc.ton s} ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod μ)

theorem MeasureTheory.indicator_ton_measurable_lt {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasureTheory.SigmaFinite μ] (hg : AEMeasurable g μ) (tc : ToneCouple) :

MeasureTheory.NullMeasurableSet {(s, x) : ℝ × α | tc.ton s < ↑‖g x‖₊} ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod μ)

theorem MeasureTheory.truncation_ton_measurable {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasureTheory.SigmaFinite (μ.restrict (Function.support f))] (hf : AEMeasurable f μ) (tc : ToneCouple) :

AEMeasurable (fun (a : ℝ × α) => MeasureTheory.trunc f (tc.ton a.1) a.2) ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod (μ.restrict (Function.support f)))

theorem MeasureTheory.truncation_compl_ton_measurable {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasureTheory.SigmaFinite (μ.restrict (Function.support f))] (hf : AEMeasurable f μ) (tc : ToneCouple) :

AEMeasurable (fun (a : ℝ × α) => (f - MeasureTheory.trunc f (tc.ton a.1)) a.2) ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod (μ.restrict (Function.support f)))

theorem MeasureTheory.restrict_to_support {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {a : ℝ} {p : ℝ} (hp : p > 0) [NormedAddCommGroup E₁] (f : α → E₁) :

∫⁻ (x : α) in Function.support f, ↑‖MeasureTheory.trunc f a x‖₊ ^ p ∂μ = ∫⁻ (x : α), ↑‖MeasureTheory.trunc f a x‖₊ ^ p ∂μ

theorem MeasureTheory.restrict_to_support_trunc_compl {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {a : ℝ} {p : ℝ} [NormedAddCommGroup E₁] (hp : p > 0) (f : α → E₁) :

∫⁻ (x : α) in Function.support f, ↑‖(f - MeasureTheory.trunc f a) x‖₊ ^ p ∂μ = ∫⁻ (x : α), ↑‖(f - MeasureTheory.trunc f a) x‖₊ ^ p ∂μ

theorem MeasureTheory.restrict_to_support_trnc {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {a : ℝ} {p : ℝ} {j : Bool} [NormedAddCommGroup E₁] (hp : p > 0) (f : α → E₁) :

∫⁻ (x : α) in Function.support f, ↑‖MeasureTheory.trnc j f a x‖₊ ^ p ∂μ = ∫⁻ (x : α), ↑‖MeasureTheory.trnc j f a x‖₊ ^ p ∂μ

theorem MeasureTheory.aeMeasurable_trunc_restrict {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] {j : Bool} {hμ : MeasureTheory.SigmaFinite (μ.restrict (Function.support f))} (hf : AEMeasurable f μ) (tc : ToneCouple) :

AEMeasurable (fun (a : ℝ × α) => MeasureTheory.trnc j f (tc.ton a.1) a.2) ((MeasureTheory.volume.restrict (Set.Ioi 0)).prod (μ.restrict (Function.support f)))

theorem MeasureTheory.lintegral_lintegral_pow_swap_trunc_compl {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {q : ℝ} {q₀ : ℝ} {p₀ : ℝ} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] {j : Bool} {hμ : MeasureTheory.SigmaFinite (μ.restrict (Function.support f))} (hp₀ : p₀ > 0) (hp₀q₀ : p₀ ≤ q₀) (hf : AEMeasurable f μ) (tc : ToneCouple) :

∫⁻ (s : ℝ) in Set.Ioi 0, (∫⁻ (a : α) in Function.support f, ENNReal.ofReal (s ^ (q - q₀ - 1)) ^ (p₀⁻¹ * q₀)⁻¹ * ↑‖MeasureTheory.trnc j f (tc.ton s) a‖₊ ^ p₀ ∂μ) ^ (p₀⁻¹ * q₀) ≤ (∫⁻ (a : α) in Function.support f, (∫⁻ (s : ℝ) in Set.Ioi 0, (ENNReal.ofReal (s ^ (q - q₀ - 1)) ^ (p₀⁻¹ * q₀)⁻¹ * ↑‖MeasureTheory.trnc j f (tc.ton s) a‖₊ ^ p₀) ^ (p₀⁻¹ * q₀)) ^ (p₀⁻¹ * q₀)⁻¹ ∂μ) ^ (p₀⁻¹ * q₀)

theorem MeasureTheory.lintegral_congr_support {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {g : α → ENNReal} {h : α → ENNReal} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] (hf : AEMeasurable f μ) (hgh : ∀ x ∈ Function.support f, g x = h x) :

∫⁻ (x : α) in Function.support f, g x ∂μ = ∫⁻ (x : α) in Function.support f, h x ∂μ

theorem MeasureTheory.estimate_trnc {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {p₀ : ℝ} {q₀ : ℝ} {q : ℝ} {spf : ScaledPowerFunction} {j : Bool} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₀q₀ : p₀ ≤ q₀) (hf : AEMeasurable f μ) (hf₂ : MeasureTheory.SigmaFinite (μ.restrict (Function.support f))) (hpowers : if xor j (spf_to_tc spf).mon = true then q₀ < q else q < q₀) :

∫⁻ (s : ℝ) in Set.Ioi 0, MeasureTheory.eLpNorm (MeasureTheory.trnc j f ((spf_to_tc spf).ton s)) (ENNReal.ofReal p₀) μ ^ q₀ * ENNReal.ofReal (s ^ (q - q₀ - 1)) ≤ ENNReal.ofReal (spf.d ^ (q - q₀)) * ENNReal.ofReal |q - q₀|⁻¹ * (∫⁻ (a : α) in Function.support f, ENNReal.ofReal (‖f a‖ ^ (p₀ + spf.σ⁻¹ * (q - q₀) * (p₀ / q₀))) ∂μ) ^ (p₀⁻¹ * q₀)

One of the key estimates for the real interpolation theorem, not yet using the particular choice of exponent and scale in the ScaledPowerFunction.

def MeasureTheory.sel (j : Bool) (p₀ : ENNReal) (p₁ : ENNReal) :

Equations

MeasureTheory.sel true p₀ p₁ = p₁
MeasureTheory.sel false p₀ p₁ = p₀

Instances For

theorem MeasureTheory.estimate_trnc₁ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} {spf : ScaledPowerFunction} {j : Bool} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] (ht : t ∈ Set.Ioo 0 1) (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp₁ : p₁ > 0) (hq₁ : q₁ > 0) (hpq : MeasureTheory.sel j p₀ p₁ ≤ MeasureTheory.sel j q₀ q₁) (hp' : MeasureTheory.sel j p₀ p₁ ≠ ⊤) (hq' : MeasureTheory.sel j q₀ q₁ ≠ ⊤) (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hf : AEMeasurable f μ) (hf₂ : MeasureTheory.SigmaFinite (μ.restrict (Function.support f))) (hspf : spf.σ = ComputationsChoiceExponent.ζ) :

∫⁻ (s : ℝ) in Set.Ioi 0, MeasureTheory.eLpNorm (MeasureTheory.trnc j f ((spf_to_tc spf).ton s)) (MeasureTheory.sel j p₀ p₁) μ ^ (MeasureTheory.sel j q₀ q₁).toReal * ENNReal.ofReal (s ^ (q.toReal - (MeasureTheory.sel j q₀ q₁).toReal - 1)) ≤ ENNReal.ofReal (spf.d ^ (q.toReal - (MeasureTheory.sel j q₀ q₁).toReal)) * ENNReal.ofReal |q.toReal - (MeasureTheory.sel j q₀ q₁).toReal|⁻¹ * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ ((MeasureTheory.sel j p₀ p₁).toReal⁻¹ * (MeasureTheory.sel j q₀ q₁).toReal)

One of the key estimates for the real interpolation theorem, now using the particular choice of exponent, but not yet using the particular choice of scale in the ScaledPowerFunction.

theorem MeasureTheory.wnorm_eq_zero_iff {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E₁} {p : ENNReal} [NormedAddCommGroup E₁] (hp : p ≠ 0) :

MeasureTheory.wnorm f p μ = 0 ↔ f =ᵐ[μ] 0

Weaktype estimates applied to truncations #

theorem MeasureTheory.eLpNorm_trnc_est {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} {j : Bool} {a : ℝ} [NormedAddCommGroup E₁] :

MeasureTheory.eLpNorm (MeasureTheory.trnc j f a) p μ ≤ MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.weaktype_estimate {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {C₀ : NNReal} {p : ENNReal} {q : ENNReal} {f : α → E₁} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (hq : 0 < q) (hq' : q < ⊤) (hf : MeasureTheory.Memℒp f p μ) (h₀T : MeasureTheory.HasWeakType T p q μ ν C₀) {t : ℝ} (ht : t > 0) :

MeasureTheory.distribution (T f) (ENNReal.ofReal t) ν ≤ ↑C₀ ^ q.toReal * MeasureTheory.eLpNorm f p μ ^ q.toReal * ENNReal.ofReal (t ^ (-q.toReal))

theorem MeasureTheory.weaktype_estimate_top {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {C : NNReal} {p : ENNReal} {q : ENNReal} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (hq' : q = ⊤) {f : α → E₁} (hf : MeasureTheory.Memℒp f p μ) (hT : MeasureTheory.HasWeakType T p q μ ν C) {t : ℝ} (ht : ↑C * MeasureTheory.eLpNorm f p μ ≤ ENNReal.ofReal t) :

MeasureTheory.distribution (T f) (ENNReal.ofReal t) ν = 0

theorem MeasureTheory.weaktype_aux₀ {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {T : (α → E₁) → α' → E₂} {p₀ : ENNReal} {q₀ : ENNReal} {p : ENNReal} {q : ENNReal} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (hp₀ : p₀ > 0) (hq₀ : q₀ > 0) (hp : p > 0) (hq : q > 0) {C₀ : NNReal} (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hF : MeasureTheory.eLpNorm f p μ = 0) :

MeasureTheory.eLpNorm (T f) q ν = 0

If T has weaktype p₀-p₁, f is AEStronglyMeasurable and the p-norm of f vanishes, then the q-norm of T f vanishes.

theorem MeasureTheory.weaktype_estimate_trunc_compl {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {C₀ : NNReal} {p : ENNReal} {p₀ : ENNReal} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp₀ : 0 < p₀) {q₀ : ENNReal} (hp : p ≠ ⊤) (hq₀ : 0 < q₀) (hq₀' : q₀ < ⊤) (hp₀p : p₀ < p) (hf : MeasureTheory.Memℒp f p μ) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) {t : ℝ} (ht : t > 0) {a : ℝ} (ha : a > 0) :

MeasureTheory.distribution (T (f - MeasureTheory.trunc f a)) (ENNReal.ofReal t) ν ≤ ↑C₀ ^ q₀.toReal * MeasureTheory.eLpNorm (f - MeasureTheory.trunc f a) p₀ μ ^ q₀.toReal * ENNReal.ofReal (t ^ (-q₀.toReal))

theorem MeasureTheory.weaktype_estimate_trunc {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {C₁ : NNReal} {p : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp : 0 < p) (hq₁ : 0 < q₁) (hq₁' : q₁ < ⊤) (hp₁p : p < p₁) (hf : MeasureTheory.Memℒp f p μ) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) {t : ℝ} (ht : t > 0) {a : ℝ} :

MeasureTheory.distribution (T (MeasureTheory.trunc f a)) (ENNReal.ofReal t) ν ≤ ↑C₁ ^ q₁.toReal * MeasureTheory.eLpNorm (MeasureTheory.trunc f a) p₁ μ ^ q₁.toReal * ENNReal.ofReal (t ^ (-q₁.toReal))

theorem MeasureTheory.weaktype_estimate_trunc_top_top {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {a : ℝ} {C₁ : NNReal} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hC₁ : C₁ > 0) {p : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} (hp : 0 < p) (hp₁ : p₁ = ⊤) (hq₁ : q₁ = ⊤) (hp₁p : p < p₁) {f : α → E₁} (hf : MeasureTheory.Memℒp f p μ) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) {t : ℝ} (ht : t > 0) (ha : a = t / ↑C₁) :

MeasureTheory.distribution (T (MeasureTheory.trunc f a)) (ENNReal.ofReal t) ν = 0

theorem MeasureTheory.weaktype_estimate_trunc_compl_top {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {C₀ : NNReal} (hC₀ : C₀ > 0) {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp₀ : 0 < p₀) (hq₀ : q₀ = ⊤) (hp₀p : p₀ < p) (hp : p ≠ ⊤) {f : α → E₁} (hf : MeasureTheory.Memℒp f p μ) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) {t : ℝ} (ht : t > 0) {a : ℝ} {d : ℝ} (ha : a = (t / d) ^ (p₀.toReal / (p₀.toReal - p.toReal))) (hdeq : d = (↑C₀ ^ p₀.toReal * MeasureTheory.eLpNorm f p μ ^ p.toReal).toReal ^ p₀.toReal⁻¹) :

MeasureTheory.distribution (T (f - MeasureTheory.trunc f a)) (ENNReal.ofReal t) ν = 0

theorem MeasureTheory.weaktype_estimate_trunc_top {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {C₁ : NNReal} (hC₁ : C₁ > 0) {p : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp : 0 < p) (hp₁ : p₁ < ⊤) (hq₁ : q₁ = ⊤) (hp₁p : p < p₁) {f : α → E₁} (hf : MeasureTheory.Memℒp f p μ) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) {t : ℝ} (ht : t > 0) {a : ℝ} {d : ℝ} (ha : a = (t / d) ^ (p₁.toReal / (p₁.toReal - p.toReal))) (hdeq : d = (↑C₁ ^ p₁.toReal * MeasureTheory.eLpNorm f p μ ^ p.toReal).toReal ^ p₁.toReal⁻¹) :

MeasureTheory.distribution (T (MeasureTheory.trunc f a)) (ENNReal.ofReal t) ν = 0

def MeasureTheory.Subadditive {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (T : (α → E₁) → α' → E₂) :

Equations

MeasureTheory.Subadditive T = ∃ A > 0, ∀ (f g : α → E₁) (x : α'), ‖T (f + g) x‖ ≤ A * (‖T f x‖ + ‖T g x‖)

Instances For

def MeasureTheory.Subadditive_trunc {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m' : MeasurableSpace α'} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (T : (α → E₁) → α' → E₂) (A : ℝ) (f : α → E₁) (ν : MeasureTheory.Measure α') :

Equations

One or more equations did not get rendered due to their size.

Instances For

def MeasureTheory.SubadditiveOn {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (T : (α → E₁) → α' → E₂) (P : (α → E₁) → Prop) (A : ℝ) :

The operator is subadditive on functions satisfying P with constant A.

Equations

MeasureTheory.SubadditiveOn T P A = ∀ (f g : α → E₁) (x : α'), P f → P g → ‖T (f + g) x‖ ≤ A * (‖T f x‖ + ‖T g x‖)

Instances For

theorem MeasureTheory.SubadditiveOn.antitone {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {P' : (α → E₁) → Prop} (h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ} (sa : MeasureTheory.SubadditiveOn T P' A) :

MeasureTheory.SubadditiveOn T P A

theorem MeasureTheory.SubadditiveOn.neg {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] {T : (α → E₁) → α' → E₂} (P : (α → E₁) → Prop) {A : ℝ} (hA : A < 0) (h : MeasureTheory.SubadditiveOn T P A) (f : α → E₁) (hf : P f) :

T f = 0

theorem MeasureTheory.SubadditiveOn.zero {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} (hP : ∀ {f g : α → E₁}, P f → P g → P (f + g)) (A : ℝ) (h : ∀ (u : α → E₁), P u → T u = 0) :

MeasureTheory.SubadditiveOn T P A

theorem MeasureTheory.SubadditiveOn.biSup {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} [NormedAddCommGroup E₁] {ι : Type u_7} (𝓑 : Set ι) {T : ι → (α → E₁) → α' → ENNReal} {P : (α → E₁) → Prop} (hT : ∀ (u : α → E₁) (x : α'), P u → ⨆ i ∈ 𝓑, T i u x ≠ ⊤) (hP : ∀ {f g : α → E₁}, P f → P g → P (f + g)) (A : ℝ) (h : ∀ i ∈ 𝓑, MeasureTheory.SubadditiveOn (fun (u : α → E₁) (x : α') => (T i u x).toReal) P A) :

MeasureTheory.SubadditiveOn (fun (u : α → E₁) (x : α') => (⨆ i ∈ 𝓑, T i u x).toReal) P A

theorem MeasureTheory.SubadditiveOn.indicator {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ} (sa : MeasureTheory.SubadditiveOn T P A) (S : Set α') :

MeasureTheory.SubadditiveOn (fun (u : α → E₁) (x : α') => S.indicator (fun (y : α') => T u y) x) P A

theorem MeasureTheory.SubadditiveOn.const {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (t : (α → E₁) → E₂) (P : (α → E₁) → Prop) (h_add : ∀ {f g : α → E₁}, P f → P g → ‖t (f + g)‖ ≤ ‖t f‖ + ‖t g‖) :

MeasureTheory.SubadditiveOn (fun (u : α → E₁) (x : α') => t u) P 1

def MeasureTheory.SublinearOn {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace ℝ E₁] [NormedSpace ℝ E₂] (T : (α → E₁) → α' → E₂) (P : (α → E₁) → Prop) (A : ℝ) :

The operator is sublinear on functions satisfying P with constant A.

Equations

MeasureTheory.SublinearOn T P A = (MeasureTheory.SubadditiveOn T P A ∧ ∀ (f : α → E₁) (c : ℝ), P f → c ≥ 0 → T (c • f) = c • T f)

Instances For

theorem MeasureTheory.SublinearOn.antitone {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace ℝ E₁] [NormedSpace ℝ E₂] {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {P' : (α → E₁) → Prop} (h : ∀ {u : α → E₁}, P u → P' u) {A : ℝ} (sl : MeasureTheory.SublinearOn T P' A) :

MeasureTheory.SublinearOn T P A

theorem MeasureTheory.SublinearOn.biSup {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} [NormedAddCommGroup E₁] [NormedSpace ℝ E₁] {ι : Type u_7} (𝓑 : Set ι) (T : ι → (α → E₁) → α' → ENNReal) {P : (α → E₁) → Prop} (hT : ∀ (u : α → E₁) (x : α'), P u → ⨆ i ∈ 𝓑, T i u x ≠ ⊤) (h_add : ∀ {f g : α → E₁}, P f → P g → P (f + g)) (h_smul : ∀ {f : α → E₁} {c : ℝ}, P f → c ≥ 0 → P (c • f)) {A : ℝ} (h : ∀ i ∈ 𝓑, MeasureTheory.SublinearOn (fun (u : α → E₁) (x : α') => (T i u x).toReal) P A) :

MeasureTheory.SublinearOn (fun (u : α → E₁) (x : α') => (⨆ i ∈ 𝓑, T i u x).toReal) P A

theorem MeasureTheory.SublinearOn.indicator {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace ℝ E₁] [NormedSpace ℝ E₂] {T : (α → E₁) → α' → E₂} {P : (α → E₁) → Prop} {A : ℝ} (S : Set α') (sl : MeasureTheory.SublinearOn T P A) :

MeasureTheory.SublinearOn (fun (u : α → E₁) (x : α') => S.indicator (fun (y : α') => T u y) x) P A

theorem MeasureTheory.SublinearOn.const {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace ℝ E₁] [NormedSpace ℝ E₂] (t : (α → E₁) → E₂) (P : (α → E₁) → Prop) (h_add : ∀ {f g : α → E₁}, P f → P g → ‖t (f + g)‖ ≤ ‖t f‖ + ‖t g‖) (h_smul : ∀ (f : α → E₁) {c : ℝ}, P f → c ≥ 0 → t (c • f) = c • t f) :

MeasureTheory.SublinearOn (fun (u : α → E₁) (x : α') => t u) P 1

Proof of the real interpolation theorem #

In this section the estimates are combined to finally give a proof of the
real interpolation theorem.

def MeasureTheory.PreservesAEStrongMeasurability {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (T : (α → E₁) → α' → E₂) (p : ENNReal) :

Proposition that expresses that the map T map between function spaces preserves AE strong measurability on L^p.

Equations

MeasureTheory.PreservesAEStrongMeasurability T p = ∀ ⦃f : α → E₁⦄, MeasureTheory.Memℒp f p μ → MeasureTheory.AEStronglyMeasurable (T f) ν

Instances For

theorem MeasureTheory.estimate_distribution_Subadditive_trunc {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m' : MeasurableSpace α'} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {f : α → E₁} {t : ℝ} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (ht : t > 0) {a : ℝ} (ha : a > 0) {A : ℝ} (hA : A ≥ 0) (h : MeasureTheory.Subadditive_trunc T A f ν) :

MeasureTheory.distribution (T f) (ENNReal.ofReal (2 * A * t)) ν ≤ MeasureTheory.distribution (T (MeasureTheory.trunc f a)) (ENNReal.ofReal t) ν + MeasureTheory.distribution (T (f - MeasureTheory.trunc f a)) (ENNReal.ofReal t) ν

theorem MeasureTheory.rewrite_norm_func {α' : Type u_2} {E : Type u_3} {m' : MeasurableSpace α'} {ν : MeasureTheory.Measure α'} {q : ℝ} {g : α' → E} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] (hq : 0 < q) {A : ℝ} (hA : A > 0) (hg : AEMeasurable g ν) :

∫⁻ (x : α'), ↑‖g x‖₊ ^ q ∂ν = ENNReal.ofReal ((2 * A) ^ q * q) * ∫⁻ (s : ℝ) in Set.Ioi 0, MeasureTheory.distribution g (ENNReal.ofReal (2 * A * s)) ν * ENNReal.ofReal (s ^ (q - 1))

theorem MeasureTheory.estimate_norm_rpow_range_operator {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m' : MeasurableSpace α'} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {q : ℝ} {f : α → E₁} [NormedAddCommGroup E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hq : 0 < q) (tc : ToneCouple) {A : ℝ} (hA : A > 0) (ht : MeasureTheory.Subadditive_trunc T A f ν) (hTf : AEMeasurable (T f) ν) :

∫⁻ (x : α'), ↑‖T f x‖₊ ^ q ∂ν ≤ ENNReal.ofReal ((2 * A) ^ q * q) * ∫⁻ (s : ℝ) in Set.Ioi 0, MeasureTheory.distribution (T (MeasureTheory.trunc f (tc.ton s))) (ENNReal.ofReal s) ν * ENNReal.ofReal (s ^ (q - 1)) + MeasureTheory.distribution (T (f - MeasureTheory.trunc f (tc.ton s))) (ENNReal.ofReal s) ν * ENNReal.ofReal (s ^ (q - 1))

theorem MeasureTheory.ton_aeMeasurable_eLpNorm_trunc {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p₁ : ENNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] (tc : ToneCouple) :

AEMeasurable (fun (x : ℝ) => MeasureTheory.eLpNorm (MeasureTheory.trunc f (tc.ton x)) p₁ μ) (MeasureTheory.volume.restrict (Set.Ioi 0))

theorem MeasureTheory.estimate_norm_rpow_range_operator' {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {T : (α → E₁) → α' → E₂} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp₀ : p₀ > 0) (hq₀ : 0 < q₀) (hq₁ : q₁ > 0) (hp₁p : p < p₁) (hp₀p : p₀ < p) (tc : ToneCouple) (hq₀' : q₀ = ⊤ → ∀ s ∈ Set.Ioi 0, MeasureTheory.distribution (T (f - MeasureTheory.trunc f (tc.ton s))) (ENNReal.ofReal s) ν = 0) (hq₁' : q₁ = ⊤ → ∀ s ∈ Set.Ioi 0, MeasureTheory.distribution (T (MeasureTheory.trunc f (tc.ton s))) (ENNReal.ofReal s) ν = 0) (hf : MeasureTheory.Memℒp f p μ) (hT₁ : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) (hT₀ : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) :

∫⁻ (s : ℝ) in Set.Ioi 0, MeasureTheory.distribution (T (MeasureTheory.trunc f (tc.ton s))) (ENNReal.ofReal s) ν * ENNReal.ofReal (s ^ (q.toReal - 1)) + MeasureTheory.distribution (T (f - MeasureTheory.trunc f (tc.ton s))) (ENNReal.ofReal s) ν * ENNReal.ofReal (s ^ (q.toReal - 1)) ≤ (if q₁ < ⊤ then 1 else 0) * (↑C₁ ^ q₁.toReal * ∫⁻ (s : ℝ) in Set.Ioi 0, MeasureTheory.eLpNorm (MeasureTheory.trunc f (tc.ton s)) p₁ μ ^ q₁.toReal * ENNReal.ofReal (s ^ (q.toReal - q₁.toReal - 1))) + (if q₀ < ⊤ then 1 else 0) * (↑C₀ ^ q₀.toReal * ∫⁻ (s : ℝ) in Set.Ioi 0, MeasureTheory.eLpNorm (f - MeasureTheory.trunc f (tc.ton s)) p₀ μ ^ q₀.toReal * ENNReal.ofReal (s ^ (q.toReal - q₀.toReal - 1)))

theorem MeasureTheory.simplify_factor_rw_aux₀ (a : ENNReal) (b : ENNReal) (c : ENNReal) (d : ENNReal) (e : ENNReal) (f : ENNReal) :

a * b * c * d * e * f = a * c * e * (b * d * f)

theorem MeasureTheory.simplify_factor_rw_aux₁ (a : ENNReal) (b : ENNReal) (c : ENNReal) (d : ENNReal) (e : ENNReal) (f : ENNReal) :

a * b * c * d * e * f = c * (a * e) * (b * f * d)

theorem MeasureTheory.simplify_factor₀ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} {D : ℝ} [NormedAddCommGroup E₁] (hq₀' : q₀ ≠ ⊤) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (ht : t ∈ Set.Ioo 0 1) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) (hD : D = ChoiceScale.d) :

↑C₀ ^ q₀.toReal * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ (q₀.toReal / p₀.toReal) * ENNReal.ofReal (D ^ (q.toReal - q₀.toReal)) = ↑C₀ ^ ((1 - t) * q.toReal) * ↑C₁ ^ (t * q.toReal) * MeasureTheory.eLpNorm f p μ ^ q.toReal

theorem MeasureTheory.simplify_factor₁ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} {D : ℝ} [NormedAddCommGroup E₁] (hq₁' : q₁ ≠ ⊤) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (ht : t ∈ Set.Ioo 0 1) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) (hD : D = ChoiceScale.d) :

↑C₁ ^ q₁.toReal * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ (q₁.toReal / p₁.toReal) * ENNReal.ofReal (D ^ (q.toReal - q₁.toReal)) = ↑C₀ ^ ((1 - t) * q.toReal) * ↑C₁ ^ (t * q.toReal) * MeasureTheory.eLpNorm f p μ ^ q.toReal

def MeasureTheory.finite_spanning_sets_from_lintegrable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → ENNReal} (hg : AEMeasurable g μ) (hg_int : ∫⁻ (x : α), g x ∂μ < ⊤) :

(μ.restrict (Function.support g)).FiniteSpanningSetsIn Set.univ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem MeasureTheory.support_sigma_finite_of_lintegrable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → ENNReal} (hg : AEMeasurable g μ) (hg_int : ∫⁻ (x : α), g x ∂μ < ⊤) :

MeasureTheory.SigmaFinite (μ.restrict (Function.support g))

theorem MeasureTheory.support_sigma_finite_from_Memℒp {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] (hf : MeasureTheory.Memℒp f p μ) (hp : p ≠ ⊤) (hp' : p ≠ 0) :

MeasureTheory.SigmaFinite (μ.restrict (Function.support f))

theorem MeasureTheory.combine_estimates₀ {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {t : ℝ} {T : (α → E₁) → α' → E₂} {A : ℝ} (hA : A > 0) [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] {spf : ScaledPowerFunction} (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hf : MeasureTheory.Memℒp f p μ) (hT : MeasureTheory.Subadditive_trunc T A f ν) (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) (hspf : spf = ChoiceScale.spf_ch ht hq₀q₁ ⋯ ⋯ ⋯ ⋯ ⋯ hC₀ hC₁ hF) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (h₂T : MeasureTheory.PreservesAEStrongMeasurability T p) :

∫⁻ (x : α'), ↑‖T f x‖₊ ^ q.toReal ∂ν ≤ ENNReal.ofReal ((2 * A) ^ q.toReal * q.toReal) * ((if q₁ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ + (if q₀ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹) * ↑C₀ ^ ((1 - t) * q.toReal) * ↑C₁ ^ (t * q.toReal) * MeasureTheory.eLpNorm f p μ ^ q.toReal

theorem MeasureTheory.combine_estimates₁ {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {t : ℝ} {T : (α → E₁) → α' → E₂} {A : ℝ} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hA : A > 0) {spf : ScaledPowerFunction} (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hf : MeasureTheory.Memℒp f p μ) (hT : MeasureTheory.Subadditive_trunc T A f ν) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (h₂T : MeasureTheory.PreservesAEStrongMeasurability T p) (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) (hspf : spf = ChoiceScale.spf_ch ht hq₀q₁ ⋯ ⋯ ⋯ ⋯ ⋯ hC₀ hC₁ hF) :

MeasureTheory.eLpNorm (T f) q ν ≤ ENNReal.ofReal (2 * A) * q ^ q⁻¹.toReal * ((if q₁ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ + (if q₀ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹) ^ q⁻¹.toReal * ↑C₀ ^ (1 - t) * ↑C₁ ^ t * MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.simplify_factor₃ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {C₀ : NNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} [NormedAddCommGroup E₁] (hp₀ : p₀ > 0) (hp₀' : p₀ ≠ ⊤) (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hp₀p₁ : p₀ = p₁) :

↑C₀ ^ q₀.toReal * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ (q₀.toReal / p₀.toReal) = (↑C₀ * MeasureTheory.eLpNorm f p μ) ^ q₀.toReal

theorem MeasureTheory.simplify_factor_aux₄ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} [NormedAddCommGroup E₁] (hq₀' : q₀ ≠ ⊤) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ = p₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

↑C₀ ^ ((1 - t) * q.toReal) * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ ((1 - t) * p₀⁻¹.toReal * q.toReal) * ↑C₁ ^ (t * q.toReal) * (MeasureTheory.eLpNorm f p μ ^ p.toReal) ^ (t * p₁⁻¹.toReal * q.toReal) = ↑C₀ ^ ((1 - t) * q.toReal) * ↑C₁ ^ (t * q.toReal) * MeasureTheory.eLpNorm f p μ ^ q.toReal

theorem MeasureTheory.simplify_factor₄ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} {D : ℝ} [NormedAddCommGroup E₁] (hq₀' : q₀ ≠ ⊤) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) (hD : D = ChoiceScale.d) :

(↑C₀ * MeasureTheory.eLpNorm f p μ) ^ q₀.toReal * ENNReal.ofReal (D ^ (q.toReal - q₀.toReal)) = ↑C₀ ^ ((1 - t) * q.toReal) * ↑C₁ ^ (t * q.toReal) * MeasureTheory.eLpNorm f p μ ^ q.toReal

theorem MeasureTheory.simplify_factor₅ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {C₀ : NNReal} {C₁ : NNReal} {μ : MeasureTheory.Measure α} {f : α → E₁} {t : ℝ} {D : ℝ} [NormedAddCommGroup E₁] (hq₁' : q₁ ≠ ⊤) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (ht : t ∈ Set.Ioo 0 1) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ ≠ q₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) * p₀⁻¹ + ENNReal.ofReal t * p₁⁻¹) (hq : q⁻¹ = (1 - ENNReal.ofReal t) * q₀⁻¹ + ENNReal.ofReal t * q₁⁻¹) (hC₀ : C₀ > 0) (hC₁ : C₁ > 0) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) (hD : D = ChoiceScale.d) :

(↑C₁ * MeasureTheory.eLpNorm f p μ) ^ q₁.toReal * ENNReal.ofReal (D ^ (q.toReal - q₁.toReal)) = ↑C₀ ^ ((1 - t) * q.toReal) * ↑C₁ ^ (t * q.toReal) * MeasureTheory.eLpNorm f p μ ^ q.toReal

theorem MeasureTheory.exists_hasStrongType_real_interpolation_aux₀ {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {t : ℝ} {T : (α → E₁) → α' → E₂} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) {C₀ : NNReal} (hp : p⁻¹ = (1 - ENNReal.ofReal t) / p₀ + ENNReal.ofReal t / p₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (h₂T : MeasureTheory.PreservesAEStrongMeasurability T p) (hf : MeasureTheory.Memℒp f p μ) (hF : MeasureTheory.eLpNorm f p μ = 0) :

MeasureTheory.eLpNorm (T f) q ν = 0

The trivial case for the estimate in the real interpolation theorem when the function Lp norm of f vanishes.

theorem MeasureTheory.exists_hasStrongType_real_interpolation_aux {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {t : ℝ} {T : (α → E₁) → α' → E₂} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {A : ℝ} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hA : A > 0) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hp₀p₁ : p₀ < p₁) (hq₀q₁ : q₀ ≠ q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) / p₀ + ENNReal.ofReal t / p₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) (hT : MeasureTheory.Subadditive_trunc T A f ν) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) (h₂T : MeasureTheory.PreservesAEStrongMeasurability T p) (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.eLpNorm (T f) q ν ≤ ENNReal.ofReal (2 * A) * q ^ q⁻¹.toReal * ((if q₁ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ + (if q₀ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹) ^ q⁻¹.toReal * ↑C₀ ^ (1 - t) * ↑C₁ ^ t * MeasureTheory.eLpNorm f p μ

The estimate for the real interpolation theorem in case p₀ < p₁.

theorem MeasureTheory.exists_hasStrongType_real_interpolation_aux₁ {α : Type u_1} {E₁ : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {μ : MeasureTheory.Measure α} {t : ℝ} {f : α → E₁} [NormedAddCommGroup E₁] (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ < q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) / p₀ + ENNReal.ofReal t / p₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) (hF : MeasureTheory.eLpNorm f p μ ∈ Set.Ioo 0 ⊤) :

(ENNReal.ofReal q.toReal * ((((↑C₀ * MeasureTheory.eLpNorm f p μ) ^ q₀.toReal * ∫⁻ (t : ℝ) in Set.Ioo 0 ChoiceScale.d, ENNReal.ofReal (t ^ (q.toReal - q₀.toReal - 1))) * if q₀ = ⊤ then 0 else 1) + ((↑C₁ * MeasureTheory.eLpNorm f p μ) ^ q₁.toReal * ∫⁻ (t : ℝ) in Set.Ici ChoiceScale.d, ENNReal.ofReal (t ^ (q.toReal - q₁.toReal - 1))) * if q₁ = ⊤ then 0 else 1)) ^ q.toReal⁻¹ ≤ q ^ q.toReal⁻¹ * ((ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ * if q₀ = ⊤ then 0 else 1) + ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ * if q₁ = ⊤ then 0 else 1) ^ q.toReal⁻¹ * ↑C₀ ^ (1 - t) * ↑C₁ ^ t * MeasureTheory.eLpNorm f p μ

theorem MeasureTheory.exists_hasStrongType_real_interpolation_aux₂ {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {p : ENNReal} {q : ENNReal} {p₀ : ENNReal} {q₀ : ENNReal} {p₁ : ENNReal} {q₁ : ENNReal} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {t : ℝ} {T : (α → E₁) → α' → E₂} {f : α → E₁} [NormedAddCommGroup E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ < q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) / p₀ + ENNReal.ofReal t / p₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) (h₂T : MeasureTheory.PreservesAEStrongMeasurability T p) (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.eLpNorm (T f) q ν ≤ q ^ q.toReal⁻¹ * ((ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ * if q₀ = ⊤ then 0 else 1) + ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ * if q₁ = ⊤ then 0 else 1) ^ q.toReal⁻¹ * ↑C₀ ^ (1 - t) * ↑C₁ ^ t * MeasureTheory.eLpNorm f p μ

The main estimate in the real interpolation theorem for p₀ = p₁, before taking roots, for the case q₀ < q₁.

theorem MeasureTheory.exists_hasStrongType_real_interpolation_aux₃ {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {t : ℝ} {T : (α → E₁) → α' → E₂} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} [NormedAddCommGroup E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hp₀p₁ : p₀ = p₁) (hq₀q₁ : q₀ ≠ q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) / p₀ + ENNReal.ofReal t / p₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) (h₂T : MeasureTheory.PreservesAEStrongMeasurability T p) (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.eLpNorm (T f) q ν ≤ q ^ q.toReal⁻¹ * ((ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹ * if q₀ = ⊤ then 0 else 1) + ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ * if q₁ = ⊤ then 0 else 1) ^ q.toReal⁻¹ * ↑C₀ ^ (1 - t) * ↑C₁ ^ t * MeasureTheory.eLpNorm f p μ

The main estimate for the real interpolation theorem for p₀ = p₁, requiring q₀ ≠ q₁, before taking roots.

theorem MeasureTheory.exists_hasStrongType_real_interpolation_aux₄ {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {t : ℝ} {T : (α → E₁) → α' → E₂} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} {A : ℝ} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hA : A > 0) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hp : p⁻¹ = (1 - ENNReal.ofReal t) / p₀ + ENNReal.ofReal t / p₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) (hT : MeasureTheory.Subadditive_trunc T A f ν) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) (h₂T : MeasureTheory.PreservesAEStrongMeasurability T p) (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.eLpNorm (T f) q ν ≤ (if p₀ = p₁ then 1 else ENNReal.ofReal (2 * A)) * q ^ q⁻¹.toReal * ((if q₁ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₁.toReal|⁻¹ + (if q₀ < ⊤ then 1 else 0) * ENNReal.ofReal |q.toReal - q₀.toReal|⁻¹) ^ q⁻¹.toReal * ↑C₀ ^ (1 - t) * ↑C₁ ^ t * MeasureTheory.eLpNorm f p μ

The main estimate for the real interpolation theorem, before taking roots, combining the cases p₀ ≠ p₁ and p₀ = p₁.

def MeasureTheory.C_realInterpolation_ENNReal (p₀ : ENNReal) (p₁ : ENNReal) (q₀ : ENNReal) (q₁ : ENNReal) (q : ENNReal) (C₀ : NNReal) (C₁ : NNReal) (A : NNReal) (t : ℝ) :

The definition of the constant in the real interpolation theorem, when viewed as an element of ℝ≥0∞.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem MeasureTheory.C_realInterpolation_ENNReal_ne_top {t : ℝ} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {A : NNReal} (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) :

MeasureTheory.C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t ≠ ⊤

theorem MeasureTheory.C_realInterpolation_ENNReal_pos {t : ℝ} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {A : NNReal} (hA : A > 0) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) :

MeasureTheory.C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t > 0

def MeasureTheory.C_realInterpolation (p₀ : ENNReal) (p₁ : ENNReal) (q₀ : ENNReal) (q₁ : ENNReal) (q : ENNReal) (C₀ : NNReal) (C₁ : NNReal) (A : NNReal) (t : ℝ) :

The constant occurring in the real interpolation theorem.

Equations

MeasureTheory.C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t = (MeasureTheory.C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t).toNNReal

Instances For

theorem MeasureTheory.C_realInterpolation_pos {t : ℝ} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {A : NNReal} (hA : A > 0) (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) :

0 < MeasureTheory.C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t

theorem MeasureTheory.coe_C_realInterpolation {t : ℝ} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {q : ENNReal} {A : NNReal} (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁) {C₀ : NNReal} {C₁ : NNReal} (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hq : q⁻¹ = (1 - ENNReal.ofReal t) / q₀ + ENNReal.ofReal t / q₁) :

↑(MeasureTheory.C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A t) = MeasureTheory.C_realInterpolation_ENNReal p₀ p₁ q₀ q₁ q C₀ C₁ A t

theorem MeasureTheory.Subadditive_trunc_from_SubadditiveOn_Lp₀p₁ {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {f : α → E₁} {t : ℝ} {T : (α → E₁) → α' → E₂} {p₀ : ENNReal} {p₁ : ENNReal} {p : ENNReal} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [NormedAddCommGroup E₂] (hp₀ : p₀ > 0) (hp₁ : p₁ > 0) {A : NNReal} (ht : t ∈ Set.Ioo 0 1) (hp : p⁻¹ = (1 - ENNReal.ofReal t) / p₀ + ENNReal.ofReal t / p₁) (hT : MeasureTheory.SubadditiveOn T (fun (f : α → E₁) => MeasureTheory.Memℒp f p₀ μ ∨ MeasureTheory.Memℒp f p₁ μ) ↑A) (hf : MeasureTheory.Memℒp f p μ) :

MeasureTheory.Subadditive_trunc T (↑A) f ν

theorem MeasureTheory.exists_hasStrongType_real_interpolation {α : Type u_1} {α' : Type u_2} {E₁ : Type u_4} {E₂ : Type u_5} {m : MeasurableSpace α} {m' : MeasurableSpace α'} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α'} {T : (α → E₁) → α' → E₂} {p₀ : ENNReal} {p₁ : ENNReal} {q₀ : ENNReal} {q₁ : ENNReal} {p : ENNReal} {q : ENNReal} [MeasurableSpace E₁] [NormedAddCommGroup E₁] [BorelSpace E₁] [MeasurableSpace E₂] [NormedAddCommGroup E₂] [BorelSpace E₂] (hp₀ : p₀ ∈ Set.Ioc 0 q₀) (hp₁ : p₁ ∈ Set.Ioc 0 q₁) (hq₀q₁ : q₀ ≠ q₁) {C₀ : NNReal} {C₁ : NNReal} {t : NNReal} {A : NNReal} (hA : A > 0) (ht : t ∈ Set.Ioo 0 1) (hC₀ : 0 < C₀) (hC₁ : 0 < C₁) (hp : p⁻¹ = (1 - ↑t) / p₀ + ↑t / p₁) (hq : q⁻¹ = (1 - ↑t) / q₀ + ↑t / q₁) (hmT : ∀ (f : α → E₁), MeasureTheory.Memℒp f p μ → MeasureTheory.AEStronglyMeasurable (T f) ν) (hT : MeasureTheory.SubadditiveOn T (fun (f : α → E₁) => MeasureTheory.Memℒp f p₀ μ ∨ MeasureTheory.Memℒp f p₁ μ) ↑A) (h₀T : MeasureTheory.HasWeakType T p₀ q₀ μ ν C₀) (h₁T : MeasureTheory.HasWeakType T p₁ q₁ μ ν C₁) :

MeasureTheory.HasStrongType T p q μ ν (MeasureTheory.C_realInterpolation p₀ p₁ q₀ q₁ q C₀ C₁ A ↑t)

Marcinkiewicz real interpolation theorem.