Supporting inequalities and notation

Adapted from Martin Dvořák’s madvorak/utilities-zcu, commit 49f60eacb1401f82358b7d66ee447ea7f2fdebf1 (Apache-2.0).

noncomputable def NemytskiiLebesgue.integralLpNorm {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] (f : Ω → E) (p : ENNReal) (μ : MeasureTheory.Measure Ω) : ENNReal

The integral/essential-supremum seminorm, without a measurability test. This retains the pre-4.34 Mathlib meaning for estimates on arbitrary functions.

Equations

• NemytskiiLebesgue.integralLpNorm f p μ = if p = 0 then 0 else if p = ⊤ then MeasureTheory.eLpNormEssSup f μ else MeasureTheory.eLpNorm' f p.toReal μ

theorem NemytskiiLebesgue.integralLpNorm_eq_eLpNorm {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] {f : Ω → E} {p : ENNReal} {μ : MeasureTheory.Measure Ω} (hf : MeasureTheory.AEStronglyMeasurable f μ) : integralLpNorm f p μ = MeasureTheory.eLpNorm f p μ

theorem NemytskiiLebesgue.integralLpNorm_eq_lintegral_rpow_enorm_toReal {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] {f : Ω → E} {p : ENNReal} {μ : MeasureTheory.Measure Ω} (hp : p ≠ 0) (hp' : p ≠ ⊤) : integralLpNorm f p μ = (∫⁻ (ω : Ω), ‖f ω‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

theorem NemytskiiLebesgue.integralLpNorm_mono_ae {Ω : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace Ω] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : Ω → E} {g : Ω → F} {p : ENNReal} {μ : MeasureTheory.Measure Ω} (hfg : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ ‖g ω‖) : integralLpNorm f p μ ≤ integralLpNorm g p μ

theorem NemytskiiLebesgue.integralLpNorm_le_eLpNorm_of_ae_le {Ω : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace Ω] [NormedAddCommGroup E] [NormedAddCommGroup F] {f : Ω → E} {g : Ω → F} {p : ENNReal} {μ : MeasureTheory.Measure Ω} (hg : MeasureTheory.AEStronglyMeasurable g μ) (hfg : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ ‖g ω‖) : integralLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ

theorem NemytskiiLebesgue.one_le_four {α : Type u_1} [AddCommMonoidWithOne α] [Preorder α] [ZeroLEOneClass α] [AddLeftMono α] : 1 ≤ 4

theorem NemytskiiLebesgue.Nat.real_one_div_succ_pos (n : ℕ) : 1 / (↑n + 1) > 0

theorem NemytskiiLebesgue.ne_zero_of_ge_one {α : Type u_1} [Zero α] [One α] [PartialOrder α] [ZeroLEOneClass α] [NeZero 1] {x : α} (h1x : 1 ≤ x) : x ≠ 0

theorem NemytskiiLebesgue.posPart_sub_posPart_sq_le (x y : ℝ) : (x⁺ - y⁺) ^ 2 ≤ (x - y) ^ 2

def NemytskiiLebesgue.«term↱_» : Lean.ParserDescr

↱ embeds nonnegative real numbers into ℝ≥0∞ and sends negative numbers to zero.

Equations

• NemytskiiLebesgue.«term↱_» = Lean.ParserDescr.node `NemytskiiLebesgue.«term↱_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↱") (Lean.ParserDescr.cat `term 1024))

theorem NemytskiiLebesgue.natCast_div_natCast_eq_ofReal (p : ℕ) {q : ℕ} (hq : q ≠ 0) : ↑p / ↑q = ENNReal.ofReal (↑p / ↑q)

theorem NemytskiiLebesgue.ofReal_div_ofReal_toReal {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) : (ENNReal.ofReal p / ENNReal.ofReal q).toReal = p / q

theorem NemytskiiLebesgue.rpow_le_ofReal_rpow_of_le_ofReal {α R : ℝ} (hα : 0 ≤ α) (hR : 0 < R) {x : ENNReal} (hx : x ≤ ENNReal.ofReal R) : x ^ α ≤ ENNReal.ofReal (R ^ α)

theorem NemytskiiLebesgue.pow_transfer_ennreal_ofReal {a : ℝ} (ha : 0 ≤ a) {b : ℝ} (hb : 0 ≤ b) {c : ℝ} (hc : 0 < c) {d : ℝ} (hd : 0 < d) {r : ℝ} (hr : 0 ≤ r) (hcarb : c * a ^ r < b) : ENNReal.ofReal a ^ (d * r) ≤ ENNReal.ofReal (c ^ (-d)) * ENNReal.ofReal b ^ d

def NemytskiiLebesgue.«term↓_» : Lean.ParserDescr

Writing ↓t is slightly more general than writing Function.const _ t.

Equations

• NemytskiiLebesgue.«term↓_» = Lean.ParserDescr.node `NemytskiiLebesgue.«term↓_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↓") (Lean.ParserDescr.cat `term 1023))

def NemytskiiLebesgue.«term_.→» : Lean.TrailingParserDescr

The left-to-right direction of ↔.

Equations

• NemytskiiLebesgue.«term_.→» = Lean.ParserDescr.trailingNode `NemytskiiLebesgue.«term_.→» 1024 1024 (Lean.ParserDescr.symbol ".→")

def NemytskiiLebesgue.«term_.←» : Lean.TrailingParserDescr

The right-to-left direction of ↔.

Equations

• NemytskiiLebesgue.«term_.←» = Lean.ParserDescr.trailingNode `NemytskiiLebesgue.«term_.←» 1024 1024 (Lean.ParserDescr.symbol ".←")

def NemytskiiLebesgue.«termℝ^_» : Lean.ParserDescr

ℝ^n is the n-dimensional Euclidean space.

Equations

• NemytskiiLebesgue.«termℝ^_» = Lean.ParserDescr.node `NemytskiiLebesgue.«termℝ^_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℝ^") (Lean.ParserDescr.cat `term 1024))

theorem NemytskiiLebesgue.inner_eq_mul (a b : ℝ) : inner ℝ a b = a * b

theorem NemytskiiLebesgue.memLp_iff_measurable_and_finite {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [TopologicalSpace E] [ENorm E] {μ : MeasureTheory.Measure Ω} {p : ENNReal} {f : Ω → E} : MeasureTheory.MemLp f p μ ↔ MeasureTheory.AEStronglyMeasurable f μ ∧ MeasureTheory.eLpNorm f p μ < ⊤

theorem NemytskiiLebesgue.eLpNorm'_norm_rpow_div_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {D : Type u_2} [NormedAddCommGroup D] (u : Ω → D) {p α : ℝ} (hα : 0 < α) : MeasureTheory.eLpNorm' (fun (x : Ω) => ‖u x‖ ^ α) (p / α) μ = MeasureTheory.eLpNorm' u p μ ^ α

theorem NemytskiiLebesgue.eLpNorm_norm_rpow_div_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {D : Type u_2} [NormedAddCommGroup D] (u : Ω → D) (hu : MeasureTheory.AEStronglyMeasurable u μ) {p α : ℝ} (hα : 0 < α) (hp : 0 < p) : MeasureTheory.eLpNorm (fun (x : Ω) => ‖u x‖ ^ α) (ENNReal.ofReal (p / α)) μ = MeasureTheory.eLpNorm u (ENNReal.ofReal p) μ ^ α

theorem NemytskiiLebesgue.integrable_norm_rpow_of_memLp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] {p : ℝ} (hp : 1 < p) {u : Ω → E} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) : MeasureTheory.Integrable (fun (x : Ω) => ‖u x‖ ^ p) μ

theorem NemytskiiLebesgue.memLp_norm_rpow_div_of_memLp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] {α : ℝ} (hα : 0 < α) {u : Ω → E} {p : ℝ} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) : MeasureTheory.MemLp (fun (x : Ω) => ‖u x‖ ^ α) (ENNReal.ofReal (p / α)) μ

theorem NemytskiiLebesgue.memLp_rpow_div_of_memLp_of_ae_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {α : ℝ} (hα : 0 < α) {v : Ω → ℝ} (h0v : 0 ≤ᵐ[μ] v) {p : ℝ} (hvp : MeasureTheory.MemLp v (ENNReal.ofReal p) μ) : MeasureTheory.MemLp (fun (x : Ω) => v x ^ α) (ENNReal.ofReal (p / α)) μ

theorem NemytskiiLebesgue.Real.HolderConjugate.integrable_memLp_mul_memLp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {p q : ℝ} (hpq : p.HolderConjugate q) {g : Ω → ℝ} (hgq : MeasureTheory.MemLp g (ENNReal.ofReal q) μ) {l : Ω → ℝ} (hlp : MeasureTheory.MemLp l (ENNReal.ofReal p) μ) : MeasureTheory.Integrable (fun (ω : Ω) => g ω * l ω) μ

theorem NemytskiiLebesgue.Real.HolderConjugate.integrable_memLp_inner_memLp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {p q : ℝ} (hpq : p.HolderConjugate q) {g : Ω → E} (hgq : MeasureTheory.MemLp g (ENNReal.ofReal q) μ) {l : Ω → E} (hlp : MeasureTheory.MemLp l (ENNReal.ofReal p) μ) : MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (g ω) (l ω)) μ

noncomputable def NemytskiiLebesgue.normSMulSelf {T : Type u_1} {n : ℕ} : T → (ξ : EuclideanSpace ℝ (Fin n)) → EuclideanSpace ℝ (Fin n)

A parameter-independent map sending a vector to its norm times itself.

Equations

• NemytskiiLebesgue.normSMulSelf x✝ ξ = ‖ξ‖ • ξ