Nemytskii operators: WeakConvergence #
Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).
def
Function.NemytskiiWeaklyConvergesTo
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(u : ℕ → E)
(v : E)
:
Sequential convergence against every continuous real linear functional.
Equations
- Function.NemytskiiWeaklyConvergesTo u v = ∀ (f : E →L[ℝ] ℝ), Filter.Tendsto (fun (n : ℕ) => f (u n)) Filter.atTop (nhds (f v))
Instances For
theorem
NemytskiiLebesgue.IsCaratheodory.strong_convergence_of_weak_convergence
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{X : Type}
[NormedAddCommGroup X]
[NormedSpace ℝ X]
{f : Ω → ℝ → ℝ}
(hf : IsCaratheodory f μ)
{p : ENNReal}
(h1p : 1 ≤ p)
(hp : p < ⊤)
{q : ENNReal}
(h1q : 1 ≤ q)
(hq : q < ⊤)
{ι : X →L[ℝ] Ω → ℝ}
(hιp : ∀ (x : X), MeasureTheory.MemLp (ι x) p μ)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a q μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : ℝ), |f ω ξ| ≤ |a ω| + C * |ξ| ^ (p / q).toReal)
{u : ℕ → X}
(hup : MeasureTheory.UnifIntegrable (⇑ι ∘ u) p μ)
{v : X}
(huv : Function.NemytskiiWeaklyConvergesTo u v)
:
Function.NemytskiiConvergesTo (fun (n : ℕ) (ω : Ω) => f ω (ι (u n) ω)) (fun (ω : Ω) => f ω (ι v ω)) q μ