def Newton.IsConjugateExponent (p q : ENNReal) : Prop

Conjugate exponent relation.

For 1 ≤ p ≤ ∞, the conjugate exponent q satisfies 1/p + 1/q = 1.

Equations

• Newton.IsConjugateExponent p q = (p = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1 ∨ 1 < p ∧ p < ⊤ ∧ 1 < q ∧ q < ⊤ ∧ 1 / p + 1 / q = 1)

theorem Newton.holder_inequality_one_infty {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] (f : α → E) (g : α → F) (hf : MeasureTheory.Integrable f μ) (hg_ae : MeasureTheory.AEStronglyMeasurable g μ) (hg_bound : ∃ (C : ℝ), ∀ᵐ (x : α) ∂μ, ‖g x‖ ≤ C) : ∫ (x : α), ‖f x‖ * ‖g x‖ ∂μ ≤ (∫ (x : α), ‖f x‖ ∂μ) * sInf {C : ℝ | ∀ᵐ (x : α) ∂μ, ‖g x‖ ≤ C}

Hölder's inequality (basic form for p = 1, q = ∞).

For any measurable functions f and g: ∫ |f · g| dμ ≤ ‖f‖{L^1} · ‖g‖{L^∞}

theorem Newton.holder_inequality {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] (p q : ENNReal) (hpq : IsConjugateExponent p q) (f : α → E) (g : α → F) (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g q μ) : MeasureTheory.Integrable (fun (x : α) => ‖f x‖ * ‖g x‖) μ ∧ ∫ (x : α), ‖f x‖ * ‖g x‖ ∂μ ≤ (MeasureTheory.eLpNorm f p μ).toReal * (MeasureTheory.eLpNorm g q μ).toReal

Hölder's inequality (general form with eLpNorm).

For conjugate exponents 1 ≤ p, q ≤ ∞ with 1/p + 1/q = 1: ∫ |f · g| dμ ≤ ‖f‖{L^p(μ)} · ‖g‖{L^q(μ)}

theorem Newton.memLp_mul_of_memLp_conjugate {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (p q : ENNReal) (hpq : IsConjugateExponent p q) (f g : α → ℝ) (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g q μ) : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ

theorem Newton.eLpNorm_toReal_pos_of_ae_pos {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (p : ENNReal) (hp : 1 < p) (f : α → ℝ) (hf : MeasureTheory.MemLp f p μ) (hf_pos : ∀ᵐ (x : α) ∂μ, 0 < f x) (hμ_pos : μ Set.univ ≠ 0) : 0 < (MeasureTheory.eLpNorm f p μ).toReal

theorem Newton.conjugate_exponent_formula (p : ENNReal) (hp : 1 < p) (hp_top : p < ⊤) : ∃ (q : ENNReal), IsConjugateExponent p q ∧ q = ENNReal.ofReal (p.toReal / (p.toReal - 1))

Conjugate exponent computation.

Compute the conjugate exponent explicitly from p.

theorem Newton.holder_kernel_pairing_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2} [NormedAddCommGroup E] {β : Type u_4} [MeasurableSpace β] {ν : MeasureTheory.Measure β} [NormedSpace ℝ E] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (p q : ENNReal) (hpq : IsConjugateExponent p q) {F : α → β → E} {φ : α → ℝ} (hF_meas : MeasureTheory.AEStronglyMeasurable (Function.uncurry F) (μ.prod ν)) (hF_prod : MeasureTheory.Integrable (Function.uncurry F) (μ.prod ν)) (hF_memLp : ∀ᵐ (y : β) ∂ν, MeasureTheory.MemLp (fun (x : α) => F x y) p μ) (hF_norm : MeasureTheory.Integrable (fun (y : β) => (MeasureTheory.eLpNorm (fun (x : α) => F x y) p μ).toReal) ν) (hφ_mem : MeasureTheory.MemLp φ q μ) : |∫ (x : α), ‖∫ (y : β), F x y ∂ν‖ * φ x ∂μ| ≤ (MeasureTheory.eLpNorm φ q μ).toReal * ∫ (y : β), (MeasureTheory.eLpNorm (fun (x : α) => F x y) p μ).toReal ∂ν

Auxiliary estimate used in the proof of Minkowski's integral inequality. It bounds the pairing between the norm of a fibrewise integral and a dual element of L^q.