RadonFactorization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Doob--Dynkin factorization of a locally finite Radon kernel through countably many real compact tests. The factor is regular on every input and is reconstructed in the target data space, without ambient null-set changes.

lemma OAI.SLEExactGauge.exists_measurable_nat_choice line 18

theorem OAI.SLEExactGauge.LocalTestFamily.measurable_radon_factor line 43

Source documentation

Countable compact tests suffice for a raw measurable Radon factor. The factorization equality holds at every original input.

theorem LocalTestFamily.measurable_radon_factor
    (D : LocalTestFamily X) {Ω Y : Type*} [MeasurableSpace Y]
    (F : Ω → Y) (μ : Ω → Measure X) (hμ : ∀ ω, (μ ω).Regular)
    (htest : ∀ j, Measurable[MeasurableSpace.comap F inferInstance]
      (fun ω => ∫ x, D.test j x ∂μ ω)) :
    ∃ ν : Y → Measure X, Measurable ν ∧ (∀ y, (ν y).Regular) ∧ ∀ ω, ν (F ω)=μ ω := by
…

Mentions: OAI.SLEExactGauge.LocalTestFamily