Nemytskii operators: Continuity #
Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).
def
Function.NemytskiiConvergesTo
{Ω : Type u_1}
[MeasurableSpace Ω]
{D : Type u_2}
[NormedAddCommGroup D]
(f : ℕ → Ω → D)
(g : Ω → D)
(p : ENNReal)
(μ : MeasureTheory.Measure Ω)
:
A sequence of functions f converges to a function g in the Lp norm with respect to a
measure μ.
Equations
- Function.NemytskiiConvergesTo f g p μ = Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
Instances For
theorem
NemytskiiLebesgue.memLp_nemytskii_of_growth_of_aestronglyMeasurable
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[NormedAddCommGroup D]
{F : Type u_3}
[NormedAddCommGroup F]
{f : Ω → D → F}
{p : ENNReal}
(h0p : 0 < p)
(hp : p ≠ ⊤)
{q : ENNReal}
(h1q : 1 ≤ q)
(hq : q ≠ ⊤)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a q μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : D), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ (p / q).toReal)
{u : Ω → D}
(hup : MeasureTheory.MemLp u p μ)
(hfu : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω (u ω)) μ)
:
MeasureTheory.MemLp (fun (ω : Ω) => f ω (u ω)) q μ
theorem
NemytskiiLebesgue.IsCaratheodory.memLp_nemytskii_of_growth
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[NormedAddCommGroup D]
{F : Type u_3}
[NormedAddCommGroup F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{p : ENNReal}
(h1p : 1 ≤ p)
(hp : p ≠ ⊤)
{q : ENNReal}
(h1q : 1 ≤ q)
(hq : q ≠ ⊤)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a q μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : D), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ (p / q).toReal)
{u : Ω → D}
(hup : MeasureTheory.MemLp u p μ)
:
MeasureTheory.MemLp (fun (ω : Ω) => f ω (u ω)) q μ
theorem
NemytskiiLebesgue.IsCaratheodory.memLp_nemytskii_of_growth_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{p : ENNReal}
(h1p : 1 ≤ p)
(hp : p < ⊤)
{q : ENNReal}
(h1q : 1 ≤ q)
(hq : q < ⊤)
{f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a q μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ (p / q).toReal)
{u : Ω → EuclideanSpace ℝ (Fin m)}
(hup : MeasureTheory.MemLp u p μ)
:
MeasureTheory.MemLp (fun (ω : Ω) => f ω (u ω)) q μ
theorem
NemytskiiLebesgue.IsCaratheodory.memLp_nemytskii_of_growth_of_holderConjugate
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[NormedAddCommGroup D]
{f : Ω → D → D}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : D), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ (p / q))
{u : Ω → D}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
:
MeasureTheory.MemLp (fun (ω : Ω) => f ω (u ω)) (ENNReal.ofReal q) μ
theorem
NemytskiiLebesgue.convergesTo_of_tendsTo_of_growth_of_aestronglyMeas
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{F : Type u_2}
[NormedAddCommGroup F]
{p : ENNReal}
(h1p : 1 ≤ p)
(hp : p ≠ ⊤)
{f : ℕ → Ω → F}
(f_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ)
{g : Ω → F}
(hgp : MeasureTheory.MemLp g p μ)
{l : Ω → ℝ}
(hlp : MeasureTheory.MemLp l p μ)
(hfl : ∀ (n : ℕ), ∀ᵐ (ω : Ω) ∂μ, ‖f n ω‖ ≤ l ω)
(hfg : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n ω) Filter.atTop (nhds (g ω)))
:
Function.NemytskiiConvergesTo f g p μ
theorem
NemytskiiLebesgue.Filter.Tendsto.exists_fast_subseq
{f : ℕ → ENNReal}
(hf : Filter.Tendsto f Filter.atTop (nhds 0))
:
theorem
NemytskiiLebesgue.ae_summable_norm_of_tsum_eLpNorm_ne_top_of_aestronglyMeas
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[NormedAddCommGroup D]
{p : ENNReal}
(h1p : 1 ≤ p)
(hp : p ≠ ⊤)
{g : ℕ → Ω → D}
(hg : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (g n) μ)
(hgp : ∑' (n : ℕ), MeasureTheory.eLpNorm (g n) p μ ≠ ⊤)
:
theorem
NemytskiiLebesgue.IsCaratheodory.nemytskii_seqContinuous_of_aestronglyMeas_of_growth
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[NormedAddCommGroup D]
{F : Type u_3}
[NormedAddCommGroup F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{p : ENNReal}
(h1p : 1 ≤ p)
(hp : p ≠ ⊤)
{q : ENNReal}
(h1q : 1 ≤ q)
(hq : q ≠ ⊤)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a q μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : D), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ (p / q).toReal)
{uₙ : ℕ → Ω → D}
(huₙ : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (uₙ n) μ)
{u : Ω → D}
(hup : MeasureTheory.MemLp u p μ)
(huuₙ : Function.NemytskiiConvergesTo uₙ u p μ)
:
Function.NemytskiiConvergesTo (fun (n : ℕ) (ω : Ω) => f ω (uₙ n ω)) (fun (ω : Ω) => f ω (u ω)) q μ
theorem
NemytskiiLebesgue.IsCaratheodory.nemytskii_seqContinuous_of_memLp_of_growth_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{p : ENNReal}
(h1p : 1 ≤ p)
(hp : p < ⊤)
{q : ENNReal}
(h1q : 1 ≤ q)
(hq : q < ⊤)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a q μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ (p / q).toReal)
{uₙ : ℕ → Ω → EuclideanSpace ℝ (Fin m)}
(huₙ : ∀ (n : ℕ), MeasureTheory.MemLp (uₙ n) p μ)
{u : Ω → EuclideanSpace ℝ (Fin m)}
(hup : MeasureTheory.MemLp u p μ)
(huuₙ : Function.NemytskiiConvergesTo uₙ u p μ)
:
Function.NemytskiiConvergesTo (fun (n : ℕ) (ω : Ω) => f ω (uₙ n ω)) (fun (ω : Ω) => f ω (u ω)) q μ