Coarse-graining support: Support.Probability.SeparableHilbertMeasurability #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Separable Hilbert measurability helpers #
This file isolates the abstract measurable-space facts needed by the fixed-competitor measurability cleanup. The first lemma is metric rather than Hilbert-specific: a map into a second-countable metric Borel space is measurable once its distances to a fixed countable dense sequence are measurable.
theorem
HCPolySupport.measurable_of_measurable_dist_denseRange
{Ω : Type u_1}
{β : Type u_2}
[MeasurableSpace Ω]
[PseudoMetricSpace β]
[MeasurableSpace β]
[BorelSpace β]
(c : ℕ → β)
(hc : DenseRange c)
{F : Ω → β}
(hFdist : ∀ (n : ℕ), Measurable fun (ω : Ω) => dist (F ω) (c n))
:
theorem
HCPolySupport.measurable_of_measurable_dist_denseSeq
{Ω : Type u_1}
{β : Type u_2}
[MeasurableSpace Ω]
[PseudoMetricSpace β]
[MeasurableSpace β]
[BorelSpace β]
[SecondCountableTopology β]
[Nonempty β]
{F : Ω → β}
(hFdist : ∀ (n : ℕ), Measurable fun (ω : Ω) => dist (F ω) (TopologicalSpace.denseSeq β n))
:
theorem
HCPolySupport.measurable_of_measurable_norm_inner_denseRange
{Ω : Type u_1}
{H : Type u_2}
[MeasurableSpace Ω]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[MeasurableSpace H]
[BorelSpace H]
(u : ℕ → H)
(hu : DenseRange u)
{F : Ω → H}
(hNorm : Measurable fun (ω : Ω) => ‖F ω‖)
(hInner : ∀ (n : ℕ), Measurable fun (ω : Ω) => inner ℝ (u n) (F ω))
:
theorem
HCPolySupport.measurable_norm_of_norm_eq_iSup_abs_inner
{Ω : Type u_1}
{H : Type u_2}
[MeasurableSpace Ω]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
(u : ℕ → H)
{F : Ω → H}
(hNormEq : ∀ (x : H), ‖x‖ = ⨆ (n : ℕ), |inner ℝ (u n) x|)
(hInner : ∀ (n : ℕ), Measurable fun (ω : Ω) => inner ℝ (u n) (F ω))
:
Measurable fun (ω : Ω) => ‖F ω‖
theorem
HCPolySupport.measurable_of_measurable_inner_denseRange_of_norm_eq_iSup_abs_inner
{Ω : Type u_1}
{H : Type u_2}
[MeasurableSpace Ω]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[MeasurableSpace H]
[BorelSpace H]
(u : ℕ → H)
(hu : DenseRange u)
{F : Ω → H}
(hNormEq : ∀ (x : H), ‖x‖ = ⨆ (n : ℕ), |inner ℝ (u n) x|)
(hInner : ∀ (n : ℕ), Measurable fun (ω : Ω) => inner ℝ (u n) (F ω))
:
theorem
HCPolySupport.measurable_of_measurable_inner_denseRange_polish
{Ω : Type u_1}
{H : Type u_2}
[MeasurableSpace Ω]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[MeasurableSpace H]
[BorelSpace H]
[PolishSpace H]
(u : ℕ → H)
(hu : DenseRange u)
{F : Ω → H}
(hInner : ∀ (n : ℕ), Measurable fun (ω : Ω) => inner ℝ (u n) (F ω))
:
theorem
HCPolySupport.measurable_of_measurable_norm_inner_denseSeq
{Ω : Type u_1}
{H : Type u_2}
[MeasurableSpace Ω]
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[MeasurableSpace H]
[BorelSpace H]
[SecondCountableTopology H]
[Nonempty H]
{F : Ω → H}
(hNorm : Measurable fun (ω : Ω) => ‖F ω‖)
(hInner : ∀ (n : ℕ), Measurable fun (ω : Ω) => inner ℝ (TopologicalSpace.denseSeq H n) (F ω))
: