Nemytskii operators: Lipschitz #
Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).
theorem
NemytskiiLebesgue.memLp_nemytskii_of_globally_lipschitz_of_aestronglyMeas
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[NormedAddCommGroup D]
{F : Type u_3}
[NormedAddCommGroup F]
{p : ENNReal}
{f : Ω → D → F}
(hf0p : MeasureTheory.MemLp (fun (x : Ω) => f x 0) p μ)
{u : Ω → D}
(hup : MeasureTheory.MemLp u p μ)
(hfu : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω (u ω)) μ)
{L : Ω → ℝ}
(hL' : MeasureTheory.eLpNorm L ⊤ μ < ⊤)
(hfL : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : D), ‖f ω ξ - f ω η‖ ≤ L ω * ‖ξ - η‖)
:
MeasureTheory.MemLp (fun (ω : Ω) => f ω (u ω)) p μ
theorem
NemytskiiLebesgue.IsCaratheodory.memLp_nemytskii_of_globally_lipschitz
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{p : ENNReal}
(hf0p : MeasureTheory.MemLp (fun (x : Ω) => f x 0) p μ)
{u : Ω → EuclideanSpace ℝ (Fin m)}
(hup : MeasureTheory.MemLp u p μ)
{L : Ω → ℝ}
(hL : MeasureTheory.MemLp L ⊤ μ)
(hfL : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : EuclideanSpace ℝ (Fin m)), ‖f ω ξ - f ω η‖ ≤ L ω * ‖ξ - η‖)
:
MeasureTheory.MemLp (fun (ω : Ω) => f ω (u ω)) p μ
theorem
NemytskiiLebesgue.integralLpNorm_difference_le_of_lipschitz
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[NormedAddCommGroup D]
{F : Type u_3}
[NormedAddCommGroup F]
{f : Ω → D → F}
{L : Ω → ℝ}
(hL : MeasureTheory.AEStronglyMeasurable L μ)
(hfL : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : D), ‖f ω ξ - f ω η‖ ≤ L ω * ‖ξ - η‖)
{u v : Ω → D}
(huv : MeasureTheory.AEStronglyMeasurable (u - v) μ)
(p : ENNReal)
:
integralLpNorm (fun (ω : Ω) => f ω (u ω) - f ω (v ω)) p μ ≤ MeasureTheory.eLpNorm L ⊤ μ * MeasureTheory.eLpNorm (u - v) p μ
theorem
NemytskiiLebesgue.integralLpNorm_difference_le_of_lipschitz_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)}
{L : Ω → ℝ}
(hL : AEMeasurable L μ)
(hfL : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : EuclideanSpace ℝ (Fin m)), ‖f ω ξ - f ω η‖ ≤ L ω * ‖ξ - η‖)
{p : ENNReal}
{u : Ω → EuclideanSpace ℝ (Fin m)}
(hup : MeasureTheory.MemLp u p μ)
{v : Ω → EuclideanSpace ℝ (Fin m)}
(hvp : MeasureTheory.MemLp v p μ)
:
integralLpNorm (fun (ω : Ω) => f ω (u ω) - f ω (v ω)) p μ ≤ MeasureTheory.eLpNorm L ⊤ μ * MeasureTheory.eLpNorm (u - v) p μ
theorem
NemytskiiLebesgue.ennreal_holderTriple_of_lt_of_lt
{p α : ℝ}
(hp : 0 < p)
(hα : 0 < α)
:
(ENNReal.ofReal (p / α)).HolderTriple (ENNReal.ofReal p) (ENNReal.ofReal (p / (α + 1)))
theorem
NemytskiiLebesgue.eLpNorm_one_ofReal_eq_measure_univ_rpow_inv
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
{p α : ℝ}
(hp : 0 < p)
(hα : 0 < α)
:
theorem
NemytskiiLebesgue.locally_integralLpNorm_difference_le
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{D : Type u_2}
[NormedAddCommGroup D]
{F : Type u_3}
[NormedAddCommGroup F]
{f : Ω → D → F}
{p : ℝ}
(h1p : 1 ≤ p)
{q : ℝ}
(h1q : 1 ≤ q)
{α : ℝ}
(hα : 0 ≤ α)
(hqpα : q = p / (α + 1))
{C : ℝ}
(hC : 0 < C)
(hfC : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : D), ‖f ω ξ - f ω η‖ ≤ C * (1 + ‖ξ‖ ^ α + ‖η‖ ^ α) * ‖ξ - η‖)
{R : ℝ}
(hR : 0 < R)
:
∃ (L : ℝ),
0 < L ∧ ∀ (u v : Ω → D),
MeasureTheory.MemLp u (ENNReal.ofReal p) μ →
MeasureTheory.MemLp v (ENNReal.ofReal p) μ →
MeasureTheory.eLpNorm u (ENNReal.ofReal p) μ ≤ ENNReal.ofReal R →
MeasureTheory.eLpNorm v (ENNReal.ofReal p) μ ≤ ENNReal.ofReal R →
integralLpNorm (fun (ω : Ω) => f ω (u ω) - f ω (v ω)) (ENNReal.ofReal q) μ ≤ ENNReal.ofReal L * MeasureTheory.eLpNorm (u - v) (ENNReal.ofReal p) μ
theorem
NemytskiiLebesgue.locally_integralLpNorm_difference_le_real
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{m k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)}
{p : ℝ}
(h1p : 1 ≤ p)
{q : ℝ}
(h1q : 1 ≤ q)
{α : ℝ}
(hα : 0 ≤ α)
(hqpα : q = p / (α + 1))
{C : ℝ}
(hC : 0 < C)
(hfC : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : EuclideanSpace ℝ (Fin m)), ‖f ω ξ - f ω η‖ ≤ C * (1 + ‖ξ‖ ^ α + ‖η‖ ^ α) * ‖ξ - η‖)
{R : ℝ}
(hR : 0 < R)
:
∃ (L : ℝ),
0 < L ∧ ∀ (u v : Ω → EuclideanSpace ℝ (Fin m)),
MeasureTheory.MemLp u (ENNReal.ofReal p) μ →
MeasureTheory.MemLp v (ENNReal.ofReal p) μ →
MeasureTheory.eLpNorm u (ENNReal.ofReal p) μ ≤ ENNReal.ofReal R →
MeasureTheory.eLpNorm v (ENNReal.ofReal p) μ ≤ ENNReal.ofReal R →
integralLpNorm (fun (ω : Ω) => f ω (u ω) - f ω (v ω)) (ENNReal.ofReal q) μ ≤ ENNReal.ofReal L * MeasureTheory.eLpNorm (u - v) (ENNReal.ofReal p) μ