Real-analysis glue for CIV.IsAdmissibleDrift's and CIV.IsLocallyBoundedOn's own measurability
clauses: a pointwise (respectively a.e.-pointwise) limit of measurable, respectively
almost-everywhere strongly measurable, functions is again measurable, respectively almost-everywhere
strongly measurable.
theorem
CIV.continuous_measurable
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
[TopologicalSpace β]
[MeasurableSpace β]
[BorelSpace β]
{f : α → β}
(hf : Continuous f)
:
theorem
CIV.measurable_of_forall_tendsto
{m : ℕ}
{β : Type u_1}
[TopologicalSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
[MeasurableSpace β]
[BorelSpace β]
{Bn : ℕ → CKN.Vec m × ℝ → β}
{B : CKN.Vec m × ℝ → β}
(hBn : ∀ (n : ℕ), Measurable (Bn n))
(hconv : ∀ (z : CKN.Vec m × ℝ), Filter.Tendsto (fun (n : ℕ) => Bn n z) Filter.atTop (nhds (B z)))
:
theorem
CIV.measurable_pair_of_isAdmissibleDrift_of_forall_tendsto
{m : ℕ}
{Bn : ℕ → CKN.Vec m × ℝ → CKN.Vec m}
{B : CKN.Vec m × ℝ → CKN.Vec m}
{divBn : ℕ → CKN.Vec m × ℝ → ℝ}
{divB : CKN.Vec m × ℝ → ℝ}
(hBn : ∀ (n : ℕ), Measurable (Bn n))
(hdivBn : ∀ (n : ℕ), Measurable (divBn n))
(hconvB : ∀ (z : CKN.Vec m × ℝ), Filter.Tendsto (fun (n : ℕ) => Bn n z) Filter.atTop (nhds (B z)))
(hconvDiv : ∀ (z : CKN.Vec m × ℝ), Filter.Tendsto (fun (n : ℕ) => divBn n z) Filter.atTop (nhds (divB z)))
:
theorem
CIV.aestronglyMeasurable_of_forall_ae_tendsto
{m : ℕ}
{μ : MeasureTheory.Measure (CKN.Vec m × ℝ)}
{qn : ℕ → CKN.Vec m × ℝ → ℝ}
{q : CKN.Vec m × ℝ → ℝ}
(hqn : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (qn n) μ)
(hconv : ∀ᵐ (z : CKN.Vec m × ℝ) ∂μ, Filter.Tendsto (fun (n : ℕ) => qn n z) Filter.atTop (nhds (q z)))
:
theorem
CIV.aestronglyMeasurable_isLocallyBoundedOn_of_forall_ae_tendsto
{m : ℕ}
{I : Set ℝ}
{qn : ℕ → CKN.Vec m × ℝ → ℝ}
{q : CKN.Vec m × ℝ → ℝ}
(hqn : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (qn n) (MeasureTheory.volume.restrict (Set.univ ×ˢ I)))
(hconv :
∀ᵐ (z : CKN.Vec m × ℝ) ∂MeasureTheory.volume.restrict (Set.univ ×ˢ I), Filter.Tendsto (fun (n : ℕ) => qn n z) Filter.atTop (nhds (q z)))
: