Nemytskii operators: Vitali #
Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).
theorem
NemytskiiLebesgue.integralLpNorm_nemytskii_rpow_le_of_growth
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[NormedAddCommGroup D]
{F : Type u_3}
[NormedAddCommGroup F]
{f : Ω → D → F}
{p : ENNReal}
(h1p : 1 ≤ p)
(hp : p ≠ ⊤)
{q : ENNReal}
(h1q : 1 ≤ q)
(hq : q ≠ ⊤)
{a : Ω → ℝ}
(haq : AEMeasurable a μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : D), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ (p / q).toReal)
(u : Ω → D)
:
theorem
NemytskiiLebesgue.integralLpNorm_nemytskii_rpow_le_of_growth_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin k)}
{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))
:
theorem
NemytskiiLebesgue.IsCaratheodory.seqContinuous_nemytskii_of_aestronglyMeas_of_growth
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{D : Type u_2}
{F : Type u_3}
[NormedAddCommGroup D]
[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ₙ : MeasureTheory.TendstoInMeasure μ uₙ Filter.atTop u)
(hpuₙ : MeasureTheory.UnifIntegrable uₙ p μ)
:
Function.NemytskiiConvergesTo (fun (n : ℕ) (ω : Ω) => f ω (uₙ n ω)) (fun (ω : Ω) => f ω (u ω)) q μ
theorem
NemytskiiLebesgue.IsCaratheodory.seqContinuous_nemytskii_of_aestronglyMeas_of_growth_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{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 : ℕ), AEMeasurable (uₙ n) μ)
{u : Ω → EuclideanSpace ℝ (Fin m)}
(hup : MeasureTheory.MemLp u p μ)
(huuₙ : MeasureTheory.TendstoInMeasure μ uₙ Filter.atTop u)
(hpuₙ : MeasureTheory.UnifIntegrable uₙ p μ)
:
Function.NemytskiiConvergesTo (fun (n : ℕ) (ω : Ω) => f ω (uₙ n ω)) (fun (ω : Ω) => f ω (u ω)) q μ
theorem
NemytskiiLebesgue.integral_inner_ge_of_ae_inner_ge_of_integrable
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{k : ℕ}
{g u : Ω → EuclideanSpace ℝ (Fin k)}
(hgu : MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (g ω) (u ω)) μ)
{b : Ω → ℝ}
(hb : MeasureTheory.Integrable b μ)
{p : ℝ}
(hup : MeasureTheory.Integrable (fun (x : Ω) => ‖u x‖ ^ p) μ)
{C : ℝ}
(hguCupb : ∀ᵐ (ω : Ω) ∂μ, inner ℝ (g ω) (u ω) ≥ C * ‖u ω‖ ^ p - b ω)
:
theorem
NemytskiiLebesgue.IsCaratheodory.integral_nemytskii_inner_ge_of_ae_all_inner_ge_of_growth
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin k) → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C₁ : ℝ}
(hC₁ : 0 ≤ C₁)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin k)), ‖f ω ξ‖ ≤ |a ω| + C₁ * ‖ξ‖ ^ (p / q))
{b : Ω → ℝ}
(hb1 : MeasureTheory.Integrable b μ)
{C₂ : ℝ}
(hfCpb : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin k)), inner ℝ (f ω ξ) ξ ≥ C₂ * ‖ξ‖ ^ p - b ω)
{u : Ω → EuclideanSpace ℝ (Fin k)}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
:
theorem
NemytskiiLebesgue.IsCaratheodory.memLp_nemytskii_ofReal_of_growth_of_holderConjugate_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin k) → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C₁ : ℝ}
(hC₁ : 0 ≤ C₁)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin k)), ‖f ω ξ‖ ≤ |a ω| + C₁ * ‖ξ‖ ^ (p / q))
{u : Ω → EuclideanSpace ℝ (Fin k)}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
:
MeasureTheory.MemLp (fun (ω : Ω) => f ω (u ω)) (ENNReal.ofReal q) μ
theorem
NemytskiiLebesgue.IsCaratheodory.integrable_inner_difference
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{f : Ω → E → E}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C₁ : ℝ}
(hC₁ : 0 ≤ C₁)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : E), ‖f ω ξ‖ ≤ |a ω| + C₁ * ‖ξ‖ ^ (p / q))
{u : Ω → E}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
{v : Ω → E}
(hvp : MeasureTheory.MemLp v (ENNReal.ofReal p) μ)
:
MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (f ω (u ω) - f ω (v ω)) (u ω - v ω)) μ
theorem
NemytskiiLebesgue.IsCaratheodory.integrable_inner_difference_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin k) → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C₁ : ℝ}
(hC₁ : 0 ≤ C₁)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin k)), ‖f ω ξ‖ ≤ |a ω| + C₁ * ‖ξ‖ ^ (p / q))
{u : Ω → EuclideanSpace ℝ (Fin k)}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
{v : Ω → EuclideanSpace ℝ (Fin k)}
(hvp : MeasureTheory.MemLp v (ENNReal.ofReal p) μ)
:
MeasureTheory.Integrable (fun (ω : Ω) => inner ℝ (f ω (u ω) - f ω (v ω)) (u ω - v ω)) μ
theorem
NemytskiiLebesgue.IsCaratheodory.coercive_integral_difference
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{f : Ω → E → E}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C₁ : ℝ}
(hC₁ : 0 ≤ C₁)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : E), ‖f ω ξ‖ ≤ |a ω| + C₁ * ‖ξ‖ ^ (p / q))
{C₂ : ℝ}
(hC₂ : 0 < C₂)
(hfCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : E), inner ℝ (f ω ξ - f ω η) (ξ - η) ≥ C₂ * ‖ξ - η‖ ^ p)
{u : Ω → E}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
{v : Ω → E}
(hvp : MeasureTheory.MemLp v (ENNReal.ofReal p) μ)
:
theorem
NemytskiiLebesgue.IsCaratheodory.coercive_integral_difference_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin k) → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C₁ : ℝ}
(hC₁ : 0 ≤ C₁)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : EuclideanSpace ℝ (Fin k)), ‖f ω ξ‖ ≤ |a ω| + C₁ * ‖ξ‖ ^ (p / q))
{C₂ : ℝ}
(hC₂ : 0 < C₂)
(hfCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : EuclideanSpace ℝ (Fin k)), inner ℝ (f ω ξ - f ω η) (ξ - η) ≥ C₂ * ‖ξ - η‖ ^ p)
{u : Ω → EuclideanSpace ℝ (Fin k)}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
{v : Ω → EuclideanSpace ℝ (Fin k)}
(hvp : MeasureTheory.MemLp v (ENNReal.ofReal p) μ)
:
theorem
NemytskiiLebesgue.ae_eq_of_ae_nemytskii_eq_nemytskii_of_ae_all_sub_inner_sub_ge
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{f : Ω → E → E}
{p C₂ : ℝ}
(hC₂ : 0 < C₂)
(hfCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : E), inner ℝ (f ω ξ - f ω η) (ξ - η) ≥ C₂ * ‖ξ - η‖ ^ p)
{u v : Ω → E}
(huv : (fun (ω : Ω) => f ω (u ω)) =ᵐ[μ] fun (ω : Ω) => f ω (v ω))
:
u =ᵐ[μ] v
theorem
NemytskiiLebesgue.ae_eq_of_ae_nemytskii_eq_nemytskii_of_ae_all_sub_inner_sub_ge_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{k : ℕ}
{f : Ω → EuclideanSpace ℝ (Fin k) → EuclideanSpace ℝ (Fin k)}
{p C₂ : ℝ}
(hC₂ : 0 < C₂)
(hfCp : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ η : EuclideanSpace ℝ (Fin k)), inner ℝ (f ω ξ - f ω η) (ξ - η) ≥ C₂ * ‖ξ - η‖ ^ p)
{u v : Ω → EuclideanSpace ℝ (Fin k)}
(huv : (fun (ω : Ω) => f ω (u ω)) =ᵐ[μ] fun (ω : Ω) => f ω (v ω))
:
u =ᵐ[μ] v