Nemytskii operators: IntegralFunctional

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

theorem NemytskiiLebesgue.IsCaratheodory.integralFunctional_wellDefined {Ω : 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 ≠ ⊤) {a : Ω → ℝ} (ha : MeasureTheory.Integrable a μ) {C : ℝ} (hC : 0 ≤ C) (hfaCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : D), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ p.toReal) {u : Ω → D} (hup : MeasureTheory.MemLp u p μ) : MeasureTheory.Integrable (fun (ω : Ω) => f ω (u ω)) μ

theorem NemytskiiLebesgue.IsCaratheodory.integralFunctional_wellDefined_real {Ω : Type} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → ℝ} (hf : IsCaratheodory f μ) {p : ENNReal} (h1p : 1 ≤ p) (hp : p < ⊤) {a : Ω → ℝ} (ha : MeasureTheory.Integrable a μ) {C : ℝ} (hC : 0 ≤ C) (hfaCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ p.toReal) {u : Ω → EuclideanSpace ℝ (Fin m)} (hup : MeasureTheory.MemLp u p μ) : MeasureTheory.Integrable (fun (ω : Ω) => f ω (u ω)) μ

noncomputable def NemytskiiLebesgue.outR1 {Ω : Type u_1} {m : ℕ} (f : Ω → EuclideanSpace ℝ (Fin m) → ℝ) : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin 1)

Regard a real-valued integrand as taking values in one-dimensional Euclidean space.

Equations

• NemytskiiLebesgue.outR1 f x1✝ x2✝ = NemytskiiLebesgue.realLIE (f x1✝ x2✝)

noncomputable def NemytskiiLebesgue.outR1nested {Ω : Type u_1} {m : ℕ} (f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] ℝ) : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin 1)

Transport the output of an integrand derivative to one-dimensional Euclidean space.

Equations

• NemytskiiLebesgue.outR1nested f' x1✝ x2✝ = LinearMap.toContinuousLinearMap ↑NemytskiiLebesgue.realLIE.toLinearEquiv ∘SL f' x1✝ x2✝

theorem NemytskiiLebesgue.IsCaratheodory.outR1 {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → ℝ} (hf : IsCaratheodory f μ) : IsCaratheodory (NemytskiiLebesgue.outR1 f) μ

theorem NemytskiiLebesgue.IsCaratheodory.outR1nested {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : ℕ} {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] ℝ} (hf' : IsCaratheodory f' μ) : IsCaratheodory (NemytskiiLebesgue.outR1nested f') μ

theorem NemytskiiLebesgue.hasFDerivAt_outR1_outR1nested {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → ℝ} {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] ℝ} (hff' : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), HasFDerivAt (f ω) (f' ω ξ) ξ) : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), HasFDerivAt (outR1 f ω) (outR1nested f' ω ξ) ξ

theorem NemytskiiLebesgue.outR1nested_norm_eq {Ω : Type u_1} {m : ℕ} (f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] ℝ) (ω : Ω) (ξ : EuclideanSpace ℝ (Fin m)) : ‖outR1nested f' ω ξ‖ = ‖f' ω ξ‖

theorem NemytskiiLebesgue.outR1nested_growth {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : ℕ} (f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] ℝ) {b : Ω → ℝ} {C α : ℝ} (hf'bCα : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f' ω ξ‖ ≤ b ω + C * ‖ξ‖ ^ α) : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖outR1nested f' ω ξ‖ ≤ b ω + C * ‖ξ‖ ^ α

theorem NemytskiiLebesgue.IsCaratheodory.memLp_nemytskii_deriv {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : ℕ} {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] ℝ} (hf' : IsCaratheodory f' μ) {p q : ℝ} (hpq : p.HolderConjugate q) {b : Ω → ℝ} (hbq : MeasureTheory.MemLp b (ENNReal.ofReal q) μ) {C : ℝ} (hC : 0 ≤ C) (hfbCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f' ω ξ‖ ≤ b ω + C * ‖ξ‖ ^ (p - 1)) {u : Ω → EuclideanSpace ℝ (Fin m)} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) : MeasureTheory.MemLp (fun (ω : Ω) => f' ω (u ω)) (ENNReal.ofReal q) μ

theorem NemytskiiLebesgue.IsCaratheodory.integrable_nemytskii_deriv_apply {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : ℕ} {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] ℝ} (hf' : IsCaratheodory f' μ) {p q : ℝ} (hpq : p.HolderConjugate q) {b : Ω → ℝ} (hbq : MeasureTheory.MemLp b (ENNReal.ofReal q) μ) {C : ℝ} (hC : 0 ≤ C) (hf'bCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f' ω ξ‖ ≤ b ω + C * ‖ξ‖ ^ (p - 1)) {u : Ω → EuclideanSpace ℝ (Fin m)} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) {v : Ω → EuclideanSpace ℝ (Fin m)} (hvp : MeasureTheory.MemLp v (ENNReal.ofReal p) μ) : MeasureTheory.Integrable (fun (ω : Ω) => (f' ω (u ω)) (v ω)) μ

theorem NemytskiiLebesgue.norm_integral_le_eLpNorm_one_toReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (g : Ω → ℝ) : ‖∫ (ω : Ω), g ω ∂μ‖ ≤ (MeasureTheory.eLpNorm g 1 μ).toReal

theorem NemytskiiLebesgue.IsCaratheodory.integralFunctional_frechet_deriv {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {m : ℕ} {f : Ω → EuclideanSpace ℝ (Fin m) → ℝ} (hf : IsCaratheodory f μ) {f' : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin m) →L[ℝ] ℝ} (hf' : IsCaratheodory f' μ) (hff' : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), HasFDerivAt (f ω) (f' ω ξ) ξ) {p q : ℝ} (hpq : p.HolderConjugate q) {b : Ω → ℝ} (h0b : 0 ≤ᵐ[μ] b) (hbq : MeasureTheory.MemLp b (ENNReal.ofReal q) μ) {C : ℝ} (hC : 0 < C) (hf'bCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin m)), ‖f' ω ξ‖ ≤ b ω + C * ‖ξ‖ ^ (p - 1)) {u : Ω → EuclideanSpace ℝ (Fin m)} (hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ) : (∀ (v : Ω → EuclideanSpace ℝ (Fin m)), MeasureTheory.MemLp v (ENNReal.ofReal p) μ → MeasureTheory.Integrable (fun (ω : Ω) => (f' ω (u ω)) (v ω)) μ) ∧ ∀ ε > 0, ∃ δ > 0, ∀ (l : Ω → EuclideanSpace ℝ (Fin m)), MeasureTheory.MemLp l (ENNReal.ofReal p) μ → MeasureTheory.eLpNorm l (ENNReal.ofReal p) μ ≤ ENNReal.ofReal δ → ‖∫ (ω : Ω), f ω (u ω + l ω) - f ω (u ω) - (f' ω (u ω)) (l ω) ∂μ‖ ≤ ε * (MeasureTheory.eLpNorm l (ENNReal.ofReal p) μ).toReal