Nemytskii operators: Closure #
Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).
theorem
NemytskiiLebesgue.IsCaratheodory.const
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
(c : F)
:
IsCaratheodory (fun (x : Ω) (x_1 : D) => c) μ
theorem
NemytskiiLebesgue.IsCaratheodory.of_stronglyMeasurable
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
{f : Ω → F}
(hf : MeasureTheory.StronglyMeasurable f)
:
IsCaratheodory (fun (ω : Ω) (x : D) => f ω) μ
theorem
NemytskiiLebesgue.IsCaratheodory.of_continuous
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
{f : D → F}
(hf : Continuous f)
:
IsCaratheodory (fun (x : Ω) (x_1 : D) => f x_1) μ
theorem
NemytskiiLebesgue.IsCaratheodory.add
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Add F]
[ContinuousAdd F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω → D → F}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f + g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.real_add
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{g : Ω → ↑D → EuclideanSpace ℝ (Fin k)}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f + g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.neg
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Neg F]
[ContinuousNeg F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
:
IsCaratheodory (-f) μ
theorem
NemytskiiLebesgue.IsCaratheodory.sub
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Sub F]
[ContinuousSub F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω → D → F}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f - g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.real_sub
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m k : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → EuclideanSpace ℝ (Fin k)}
(hf : IsCaratheodory f μ)
{g : Ω → ↑D → EuclideanSpace ℝ (Fin k)}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f - g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.mul
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Mul F]
[ContinuousMul F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω → D → F}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f * g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.real_mul
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → ℝ}
(hf : IsCaratheodory f μ)
{g : Ω → ↑D → ℝ}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f * g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.smul
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{M : Type u_3}
[TopologicalSpace M]
{F : Type u_4}
[TopologicalSpace F]
[SMul M F]
[ContinuousSMul M F]
{f : Ω → D → M}
(hf : IsCaratheodory f μ)
{g : Ω → D → F}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f • g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.const_smul
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{M : Type u_3}
{F : Type u_4}
[TopologicalSpace F]
[SMul M F]
[ContinuousConstSMul M F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
(c : M)
:
IsCaratheodory (c • f) μ
theorem
NemytskiiLebesgue.IsCaratheodory.inv
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Inv F]
[ContinuousInv F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
:
IsCaratheodory f⁻¹ μ
theorem
NemytskiiLebesgue.IsCaratheodory.div
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Div F]
[ContinuousDiv F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω → D → F}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f / g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.real_div
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → ℝ}
(hf : IsCaratheodory f μ)
{g : Ω → ↑D → ℝ}
(hg : IsCaratheodory g μ)
(hg0 : ∀ᵐ (ω : Ω) ∂μ, ∀ (x : ↑D), g ω x ≠ 0)
:
IsCaratheodory (f / g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.pow_nat
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Monoid F]
[ContinuousMul F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
(n : ℕ)
:
IsCaratheodory (f ^ n) μ
theorem
NemytskiiLebesgue.IsCaratheodory.real_pow_nat
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → ℝ}
(hf : IsCaratheodory f μ)
(n : ℕ)
:
IsCaratheodory (f ^ n) μ
theorem
NemytskiiLebesgue.IsCaratheodory.sup
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Max F]
[ContinuousSup F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω → D → F}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f ⊔ g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.real_sup
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → ℝ}
(hf : IsCaratheodory f μ)
{g : Ω → ↑D → ℝ}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f ⊔ g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.inf
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
[Min F]
[ContinuousInf F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω → D → F}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f ⊓ g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.real_inf
{Ω : Type}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{m : ℕ}
{D : Set (EuclideanSpace ℝ (Fin m))}
{f : Ω → ↑D → ℝ}
(hf : IsCaratheodory f μ)
{g : Ω → ↑D → ℝ}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (f ⊓ g) μ
theorem
NemytskiiLebesgue.IsCaratheodory.comp_continuous
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
{G : Type u_4}
[TopologicalSpace G]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : F → G}
(hg : Continuous g)
:
IsCaratheodory (fun (x1 : Ω) (x2 : D) => g (f x1 x2)) μ
theorem
NemytskiiLebesgue.IsCaratheodory.comp_measurePreserving
{Ω : Type u_1}
{Ω' : Type u_2}
[MeasurableSpace Ω]
[MeasurableSpace Ω']
{μ : MeasureTheory.Measure Ω}
{μ' : MeasureTheory.Measure Ω'}
{D : Type u_3}
[TopologicalSpace D]
{F : Type u_4}
[TopologicalSpace F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω' → Ω}
(hg : MeasureTheory.MeasurePreserving g μ' μ)
:
IsCaratheodory (f ∘ g) μ'
theorem
NemytskiiLebesgue.IsCaratheodory.norm
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[NormedAddCommGroup F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
:
IsCaratheodory (fun (x1 : Ω) (x2 : D) => ‖f x1 x2‖) μ
theorem
NemytskiiLebesgue.IsCaratheodory.nnnorm
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[NormedAddCommGroup F]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
:
IsCaratheodory (fun (x1 : Ω) (x2 : D) => ‖f x1 x2‖₊) μ
theorem
NemytskiiLebesgue.IsCaratheodory.prod
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
{G : Type u_4}
[TopologicalSpace G]
{f : Ω → D → F}
(hf : IsCaratheodory f μ)
{g : Ω → D → G}
(hg : IsCaratheodory g μ)
:
IsCaratheodory (fun (ω : Ω) (x : D) => (f ω x, g ω x)) μ
theorem
NemytskiiLebesgue.IsCaratheodory.fst
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
{G : Type u_4}
[TopologicalSpace G]
{f : Ω → D → F × G}
(hf : IsCaratheodory f μ)
:
IsCaratheodory (fun (ω : Ω) (x : D) => (f ω x).1) μ
theorem
NemytskiiLebesgue.IsCaratheodory.snd
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{D : Type u_2}
[TopologicalSpace D]
{F : Type u_3}
[TopologicalSpace F]
{G : Type u_4}
[TopologicalSpace G]
{f : Ω → D → F × G}
(hf : IsCaratheodory f μ)
:
IsCaratheodory (fun (ω : Ω) (x : D) => (f ω x).2) μ