theorem Newton.lintegral_mul_mul_le_three_holder {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g h : α → ENNReal} {p q r : ENNReal} (hpqr : 1 / p + 1 / q + 1 / r = 1) (hp_top : p ≠ ⊤) (hq_top : q ≠ ⊤) (hr_top : r ≠ ⊤) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hh : AEMeasurable h μ) : ∫⁻ (x : α), f x * g x * h x ∂μ ≤ (∫⁻ (x : α), f x ^ p.toReal ∂μ) ^ (1 / p.toReal) * (∫⁻ (x : α), g x ^ q.toReal ∂μ) ^ (1 / q.toReal) * (∫⁻ (x : α), h x ^ r.toReal ∂μ) ^ (1 / r.toReal)

theorem Newton.young_exponent_p_le_r {p q r : ENNReal} (hq : 1 ≤ q) (hpqr : 1 / p + 1 / q = 1 + 1 / r) : p ≤ r

theorem Newton.young_exponent_q_le_r {p q r : ENNReal} (hp : 1 ≤ p) (hpqr : 1 / p + 1 / q = 1 + 1 / r) : q ≤ r

Auxiliary lemma to derive q ≤ r from Young exponent condition

theorem Newton.young_exponent_r_ge_one {p q r : ENNReal} (hp : 1 ≤ p) (hq : 1 ≤ q) (hpqr : 1 / p + 1 / q = 1 + 1 / r) : 1 ≤ r

Auxiliary lemma to derive r ≥ 1 from Young exponent condition

theorem Newton.ennreal_div_mul_right {p r : ENNReal} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hr_pos : r ≠ 0) (hr_ne_top : r ≠ ⊤) : r / (p * r) = 1 / p

Auxiliary lemma showing r / (p * r) = 1/p in ENNReal

theorem Newton.ennreal_div_mul_left {p r : ENNReal} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hr_pos : r ≠ 0) (hr_ne_top : r ≠ ⊤) : p / (p * r) = 1 / r

Auxiliary lemma showing p / (p * r) = 1/r in ENNReal

theorem Newton.ennreal_sub_div_mul {p r : ENNReal} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ⊤) (hr_pos : r ≠ 0) (hr_ne_top : r ≠ ⊤) : (r - p) / (p * r) = 1 / p - 1 / r

Auxiliary lemma showing (r - p) / (p * r) = 1/p - 1/r in ENNReal (when p ≤ r)

theorem Newton.young_exponent_to_three_holder {p q r : ENNReal} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hp_ne_top : p ≠ ⊤) (hq_ne_top : q ≠ ⊤) (hr_ne_top : r ≠ ⊤) (hpqr : 1 / p + 1 / q = 1 + 1 / r) : 1 / r + (r - p) / (p * r) + (r - q) / (q * r) = 1

Derive three-function Hölder exponent condition from Young exponent condition Note: p, q, r ≠ ⊤ is required (because ⊤/⊤ = 0 in ENNReal)

theorem Newton.decomposition_exponents_pos {p q r : ENNReal} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr_ne_top : r ≠ ⊤) : 0 < p / r ∧ 0 < q / r ∧ 0 ≤ 1 - p / r ∧ 0 ≤ 1 - q / r

Verify that exponents used in decomposition are non-negative (can be 0 at boundary)

theorem Newton.lintegral_const_top_of_volume_univ {n : ℕ} (c : ENNReal) (hc : c ≠ 0) (hn : 0 < n) : ∫⁻ (x : Fin n → ℝ), c = ⊤

For a nonzero constant c, the integral of c over the whole space is infinite when the dimension n is positive.

theorem Newton.lintegral_eq_zero_iff_ae_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} (hf : AEMeasurable f μ) : ∫⁻ (x : α), f x ∂μ = 0 ↔ f =ᵐ[μ] 0

Characterization of vanishing lintegral in terms of a.e. vanishing (ℝ≥0∞-valued).

theorem Newton.ae_eq_zero_of_lintegral_mul_eq_zero_left {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hg_pos : ∀ᵐ (x : α) ∂μ, 0 < g x) (hf_meas : AEMeasurable f μ) (hg_meas : AEMeasurable g μ) (h_int : ∫⁻ (x : α), f x * g x ∂μ = 0) : f =ᵐ[μ] 0

If the product f * g has zero integral and g is strictly positive a.e., then f vanishes a.e. (ℝ≥0∞-valued version).

theorem Newton.ae_eq_zero_of_lintegral_mul_eq_zero_right {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (hf_pos : ∀ᵐ (x : α) ∂μ, 0 < f x) (hf_meas : AEMeasurable f μ) (hg_meas : AEMeasurable g μ) (h_int : ∫⁻ (x : α), f x * g x ∂μ = 0) : g =ᵐ[μ] 0

Symmetric version of ae_eq_zero_of_lintegral_mul_eq_zero_left.

theorem Newton.eLpNorm_translate_right {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [TopologicalSpace G] [MeasurableAdd₂ G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure] (f : G → ℂ) (p : ENNReal) (a : G) (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm (fun (x : G) => f (x - a)) p μ = MeasureTheory.eLpNorm f p μ

theorem Newton.convolution_integrand_decomposition {n : ℕ} (f g : (Fin n → ℝ) → ℂ) (p q r : ENNReal) (hp : 1 ≤ p) (hq : 1 ≤ q) (hp_ne_top : p ≠ ⊤) (hq_ne_top : q ≠ ⊤) (hr_ne_top : r ≠ ⊤) (hpqr : 1 / p + 1 / q = 1 + 1 / r) (x y : Fin n → ℝ) : ‖f y‖ * ‖g (x - y)‖ = ‖f y‖ ^ (p / r).toReal * ‖g (x - y)‖ ^ (q / r).toReal * ‖f y‖ ^ (1 - p / r).toReal * ‖g (x - y)‖ ^ (1 - q / r).toReal