Nemytskii operators: Caratheodory #
Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).
structure
NemytskiiLebesgue.IsCaratheodory
{Ω : Type u_1}
{D : Type u_2}
{F : Type u_3}
[MeasurableSpace Ω]
[TopologicalSpace D]
[TopologicalSpace F]
(f : Ω → D → F)
(μ : MeasureTheory.Measure Ω)
:
A function f : Ω → D → F is Carathéodory with respect to a measure μ if:
(1) For every x ∈ D, the mapping (f · x) is strongly measurable.
(2) For almost every ω ∈ Ω with respect to μ, the mapping (f ω ·) is continuous.
- isStronglyMeasurable (x : D) : MeasureTheory.StronglyMeasurable fun (x_1 : Ω) => f x_1 x
- ae_continuous : ∀ᵐ (ω : Ω) ∂μ, Continuous (f ω)
Instances For
theorem
NemytskiiLebesgue.normSMulSelf_isCaratheodory
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{n : ℕ}
:
theorem
NemytskiiLebesgue.aestronglyMeasurable_composition_of_stronglyMeasurable
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[TopologicalSpace.PseudoMetrizableSpace F]
{f : Ω → D → F}
(hf : ∀ (x : D), MeasureTheory.AEStronglyMeasurable (fun (x_1 : Ω) => f x_1 x) μ)
(hf' : ∀ᵐ (ω : Ω) ∂μ, Continuous (f ω))
{g : Ω → D}
(hg : MeasureTheory.StronglyMeasurable g)
:
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω (g ω)) μ
theorem
NemytskiiLebesgue.aestronglyMeasurable_composition
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[TopologicalSpace.PseudoMetrizableSpace F]
{f : Ω → D → F}
(hf : ∀ (x : D), MeasureTheory.AEStronglyMeasurable (fun (x_1 : Ω) => f x_1 x) μ)
(hf' : ∀ᵐ (ω : Ω) ∂μ, Continuous (f ω))
{g : Ω → D}
(hg : MeasureTheory.AEStronglyMeasurable g μ)
:
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω (g ω)) μ
theorem
NemytskiiLebesgue.IsCaratheodory.aestronglyMeas_nemytskii_of_aestronglyMeas
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[TopologicalSpace.PseudoMetrizableSpace F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω → D}
(hg : MeasureTheory.AEStronglyMeasurable g μ)
:
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω (g ω)) μ
theorem
NemytskiiLebesgue.IsCaratheodory.aestronglyMeas_nemytskii_of_aeMeas_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{g : Ω → ↑D}
(hg : AEMeasurable g μ)
:
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => f ω (g ω)) μ
theorem
NemytskiiLebesgue.IsCaratheodory.aeMeas_nemytskii_of_aeMeas_real
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{g : Ω → ↑D}
(hg : AEMeasurable g μ)
:
AEMeasurable (fun (ω : Ω) => f ω (g ω)) μ