Nemytskii operators: Frechet

Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).

theorem NemytskiiLebesgue.frechet_remainder_le_of_all_in_set_icc_zero_one_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : E → F} {g' : E → E →L[ℝ] F} (hgg' : ∀ (ξ : E), HasFDerivAt g (g' ξ) ξ) {x e : E} {M : ℝ} (hxeM : ∀ t ∈ Set.Icc 0 1, ‖g' (x + t • e) - g' x‖ ≤ M) : ‖g (x + e) - g x - (g' x) e‖ ≤ M * ‖e‖

theorem NemytskiiLebesgue.ae_norm_frechet_ratio_tendsto_zero {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m k : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)} {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin k)} (hff' : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), HasFDerivAt (f ω) (f' ω ξ) ξ) {l : ℕ → Ω → EuclideanSpace ℝ (Fin m)} (hl : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (x : ℕ) => l x ω) Filter.atTop (nhds 0)) (u : Ω → EuclideanSpace ℝ (Fin m)) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => ‖f ω (u ω + l n ω) - f ω (u ω) - (f' ω (u ω)) (l n ω)‖ / ‖l n ω‖) Filter.atTop (nhds 0)

theorem NemytskiiLebesgue.integralLpNorm_le_eLpNorm_mul_eLpNorm_of_aestronglyMeas {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m k : ℕ} {p q r : ℝ} (hrpq : r.HolderTriple p q) {l : Ω → EuclideanSpace ℝ (Fin m)} (hl : MeasureTheory.AEStronglyMeasurable l μ) {ψ : Ω → ℝ} (hψ : MeasureTheory.AEStronglyMeasurable ψ μ) {R : Ω → EuclideanSpace ℝ (Fin k)} (hRψl : ∀ᵐ (ω : Ω) ∂μ, ‖R ω‖ ≤ ψ ω * ‖l ω‖) : integralLpNorm R (ENNReal.ofReal q) μ ≤ MeasureTheory.eLpNorm ψ (ENNReal.ofReal r) μ * MeasureTheory.eLpNorm l (ENNReal.ofReal p) μ

theorem NemytskiiLebesgue.eLpNorm_le_eLpNorm_mul_eLpNorm_of_aestronglyMeas {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m k : ℕ} {p q r : ℝ} (hrpq : r.HolderTriple p q) {l : Ω → EuclideanSpace ℝ (Fin m)} (hl : MeasureTheory.AEStronglyMeasurable l μ) {ψ : Ω → ℝ} (hψ : MeasureTheory.AEStronglyMeasurable ψ μ) {R : Ω → EuclideanSpace ℝ (Fin k)} (hR : MeasureTheory.AEStronglyMeasurable R μ) (hRψl : ∀ᵐ (ω : Ω) ∂μ, ‖R ω‖ ≤ ψ ω * ‖l ω‖) : MeasureTheory.eLpNorm R (ENNReal.ofReal q) μ ≤ MeasureTheory.eLpNorm ψ (ENNReal.ofReal r) μ * MeasureTheory.eLpNorm l (ENNReal.ofReal p) μ

theorem NemytskiiLebesgue.IsCaratheodory.aestronglyMeas_nemytskii {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m k : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)} (hf : IsCaratheodory f μ) {u : Ω → EuclideanSpace ℝ (Fin m)} {p : ℝ} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω (u ω)) μ

theorem NemytskiiLebesgue.IsCaratheodory.aestronglyMeas_frechet_remainder {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m k : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)} (hf : IsCaratheodory f μ) {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin k)} (hf' : IsCaratheodory f' μ) {p : ℝ} {u : Ω → EuclideanSpace ℝ (Fin m)} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) {u' : Ω → EuclideanSpace ℝ (Fin m)} (hu' : MeasureTheory.AEStronglyMeasurable u' μ) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω (u ω + u' ω) - f ω (u ω) - (f' ω (u ω)) (u' ω)) μ

theorem NemytskiiLebesgue.ae_frechet_ratio_le_of_ae_all_growth_deriv {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m k : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)} {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin k)} (hf' : ∀ᵐ (ω : Ω) ∂μ, Continuous (f' ω)) (hff' : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), HasFDerivAt (f ω) (f' ω ξ) ξ) {C : ℝ} (hC : 0 < C) {p : ℝ} (h1p : 1 ≤ p) {r : ℝ} (h1r : 1 ≤ r) {b : Ω → ℝ} (h0b : 0 ≤ᵐ[μ] b) (hf'bCpr : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f' ω ξ‖ ≤ b ω + C * ‖ξ‖ ^ (p / r)) {g : Ω → ℝ} (h0g : 0 ≤ᵐ[μ] g) {v : Ω → EuclideanSpace ℝ (Fin m)} (hvg : ∀ᵐ (ω : Ω) ∂μ, ‖v ω‖ ≤ g ω) (u : Ω → EuclideanSpace ℝ (Fin m)) : ∀ᵐ (ω : Ω) ∂μ, ‖f ω (u ω + v ω) - f ω (u ω) - (f' ω (u ω)) (v ω)‖ / ‖v ω‖ ≤ 2 * b ω + C * (‖u ω‖ + g ω) ^ (p / r) + C * ‖u ω‖ ^ (p / r)

theorem NemytskiiLebesgue.convergesTo_of_ae_tendsTo_of_ae_norm_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] {p : ENNReal} (hp1 : 1 ≤ p) (hp : p ≠ ⊤) {F : ℕ → Ω → E} (hF : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ) {g : Ω → E} (hg : MeasureTheory.AEStronglyMeasurable g μ) {b : Ω → ℝ} (hbp : MeasureTheory.MemLp b p μ) (hFb : ∀ (n : ℕ), ∀ᵐ (ω : Ω) ∂μ, ‖F n ω‖ ≤ b ω) (hgb : ∀ᵐ (ω : Ω) ∂μ, ‖g ω‖ ≤ b ω) (hFg : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (x : ℕ) => F x ω) Filter.atTop (nhds (g ω))) : Function.NemytskiiConvergesTo F g p μ

theorem NemytskiiLebesgue.IsCaratheodory.tendsTo_eLpNorm_frechet_ratio_of_ae_tendsTo {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m k : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)} (hf : IsCaratheodory f μ) {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin k)} (hf' : IsCaratheodory f' μ) (hff' : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), HasFDerivAt (f ω) (f' ω ξ) ξ) {p : ℝ} (h1p : 1 ≤ p) {r : ℝ} (h1r : 1 ≤ r) {C : ℝ} (hC : 0 < C) {b : Ω → ℝ} (h0b : 0 ≤ᵐ[μ] b) (hbr : MeasureTheory.MemLp b (ENNReal.ofReal r) μ) (hf'bCpr : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f' ω ξ‖ ≤ b ω + C * ‖ξ‖ ^ (p / r)) {u : Ω → EuclideanSpace ℝ (Fin m)} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) {l : ℕ → Ω → EuclideanSpace ℝ (Fin m)} (hl : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (l n) μ) {g : Ω → ℝ} (h0g : 0 ≤ᵐ[μ] g) (hgp : MeasureTheory.MemLp g (ENNReal.ofReal p) μ) (hlg : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖l n ω‖ ≤ g ω) (hl0 : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (x : ℕ) => l x ω) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (ω : Ω) => ‖f ω (u ω + l n ω) - f ω (u ω) - (f' ω (u ω)) (l n ω)‖ / ‖l n ω‖) (ENNReal.ofReal r) μ) Filter.atTop (nhds 0)

theorem NemytskiiLebesgue.Filter.Tendsto.extract_fast_subseq_eLpNorm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] {p : ENNReal} {l : ℕ → Ω → E} (hlp : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (l n) p μ) Filter.atTop (nhds 0)) : ∃ (s : ℕ → ℕ), StrictMono s ∧ ∀ (k : ℕ), MeasureTheory.eLpNorm (l (s k)) p μ ≤ ENNReal.ofReal (1 / 2 ^ k)

theorem NemytskiiLebesgue.IsCaratheodory.eLpNorm_frechet_remainder_le_ofReal_mul_eLpNorm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m k : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)} (hf : IsCaratheodory f μ) {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin k)} (hf' : IsCaratheodory f' μ) (hff' : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), HasFDerivAt (f ω) (f' ω ξ) ξ) {p q r : ℝ} (h1p : 1 ≤ p) (h1r : 1 ≤ r) (hrpq : r.HolderTriple p q) {b : Ω → ℝ} (h0b : 0 ≤ᵐ[μ] b) (hbr : MeasureTheory.MemLp b (ENNReal.ofReal r) μ) {C : ℝ} (hC : 0 < C) (hf'bCpr : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f' ω ξ‖ ≤ b ω + C * ‖ξ‖ ^ (p / r)) {u : Ω → EuclideanSpace ℝ (Fin m)} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) (ε : ℝ) : ε > 0 → ∃ δ > 0, ∀ (l : Ω → EuclideanSpace ℝ (Fin m)), MeasureTheory.MemLp l (ENNReal.ofReal p) μ → MeasureTheory.eLpNorm l (ENNReal.ofReal p) μ ≤ ENNReal.ofReal δ → MeasureTheory.eLpNorm (fun (ω : Ω) => f ω (u ω + l ω) - f ω (u ω) - (f' ω (u ω)) (l ω)) (ENNReal.ofReal q) μ ≤ ENNReal.ofReal ε * MeasureTheory.eLpNorm l (ENNReal.ofReal p) μ