NormalizedSections.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem358.NormalizedSections.sectionMass line 14
def OAI.Problem358.NormalizedSections.sectionDensity line 17
def OAI.Problem358.NormalizedSections.sectionLaw line 20

theorem OAI.Problem358.NormalizedSections.sectionMass_const_mul line 24

Source documentation

A constant normalization of the joint density scales each marginal mass.

theorem sectionMass_const_mul (ν : Measure B)
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (c : ℝ≥0∞) (a : A) :
    sectionMass ν (fun a b => c * q a b) a = c * sectionMass ν q a := by
…

Mentions: OAI.Problem358.NormalizedSections.sectionMass

theorem OAI.Problem358.NormalizedSections.sectionDensity_const_mul line 32
Source documentation
The conditional density is unaffected by any positive finite normalization of the whole joint density, including on zero or infinite sections.
```
theorem sectionDensity_const_mul (ν : Measure B)
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (c : ℝ≥0∞) (hc0 : c ≠ 0) (hctop : c ≠ ∞) :
    sectionDensity ν (fun a b => c * q a b) = sectionDensity ν q := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionDensity
theorem OAI.Problem358.NormalizedSections.sectionLaw_const_mul line 42
Source documentation
Uniform-region sampling can use the unscaled conditional laws while its joint density and section-mass marginal carry the total-volume normalization.
```
theorem sectionLaw_const_mul (ν : Measure B)
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (c : ℝ≥0∞) (hc0 : c ≠ 0) (hctop : c ≠ ∞) (a : A) :
    sectionLaw ν (fun a b => c * q a b) a = sectionLaw ν q a := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionLaw
theorem OAI.Problem358.NormalizedSections.measurable_sectionMass line 48
theorem OAI.Problem358.NormalizedSections.measurable_sectionDensity line 52

theorem OAI.Problem358.NormalizedSections.lintegral_sectionDensity_eq_one line 58

Source documentation

Every nonzero finite section has a normalized probability density.

theorem lintegral_sectionDensity_eq_one (ν : Measure B)
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (a : A) (h0 : sectionMass ν q a ≠ 0) (hfin : sectionMass ν q a ≠ ∞) :
    (∫⁻ b, sectionDensity ν q a b ∂ν) = 1 := by
…

Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.sectionDensity

theorem OAI.Problem358.NormalizedSections.isProbabilityMeasure_sectionLaw line 66
theorem OAI.Problem358.NormalizedSections.sectionMass_mul_lintegral_sectionLaw line 76
Source documentation
Multiplication by the section mass cancels conditional normalization, including zero-mass sections; only infinite-mass sections have to be excluded.
```
theorem sectionMass_mul_lintegral_sectionLaw (ν : Measure B)
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (a : A) (hfin : sectionMass ν q a ≠ ∞)
    {f : B → ℝ≥0∞} (hf : Measurable f) :
    sectionMass ν q a * (∫⁻ b, f b ∂sectionLaw ν q a) =
      ∫⁻ b, q a b * f b ∂ν := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.sectionLaw

theorem OAI.Problem358.NormalizedSections.measurable_lintegral_sectionLaw line 103

Source documentation

Conditional integration preserves measurability in the parameter.

theorem measurable_lintegral_sectionLaw (ν : Measure B) [SFinite ν]
    {q f : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (hf : Measurable (Function.uncurry f)) :
    Measurable (fun a => ∫⁻ b, f a b ∂sectionLaw ν q a) := by
…

Mentions: OAI.Problem358.NormalizedSections.sectionLaw

theorem OAI.Problem358.NormalizedSections.lintegral_reassemble_sections line 117

Source documentation

Exact disintegration of a product density into its section mass and normalized section laws. The finite-mass hypothesis is only almost everywhere.

theorem lintegral_reassemble_sections (μ : Measure A) (ν : Measure B) [SFinite ν]
    {q f : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (hf : Measurable (Function.uncurry f))
    (hfin : ∀ᵐ a ∂μ, sectionMass ν q a ≠ ∞) :
    (∫⁻ a, ∫⁻ b, f a b ∂sectionLaw ν q a ∂μ.withDensity (sectionMass ν q)) =
      ∫⁻ p, f p.1 p.2 ∂(μ.prod ν).withDensity (Function.uncurry q) := by
…

Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.sectionLaw

def OAI.Problem358.NormalizedSections.sectionKernel line 133
Source documentation
The normalized section laws form a genuine measurable kernel.
```
def sectionKernel (ν : Measure B) [SFinite ν] (q : A → B → ℝ≥0∞) :
    ProbabilityTheory.Kernel A B :=
…
```
theorem OAI.Problem358.NormalizedSections.sectionKernel_apply line 137
theorem OAI.Problem358.NormalizedSections.isMarkovKernel_sectionKernel line 144
theorem OAI.Problem358.NormalizedSections.isFiniteKernel_sectionKernel line 154
Source documentation
The conditional kernel is uniformly finite, including its zero/infinite section defaults.
```
theorem isFiniteKernel_sectionKernel (ν : Measure B) [SFinite ν]
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q)) :
    ProbabilityTheory.IsFiniteKernel (sectionKernel ν q) := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionKernel
theorem OAI.Problem358.NormalizedSections.compProd_sectionKernel line 167
Source documentation
Measure-level disintegration, ready to compose with conditional quantile laws. Zero-mass fibers require no arbitrary probability choice because their marginal weight vanishes.
```
theorem compProd_sectionKernel (μ : Measure A) [SFinite μ]
    (ν : Measure B) [SFinite ν]
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (hfin : ∀ᵐ a ∂μ, sectionMass ν q a ≠ ∞) :
    (μ.withDensity (sectionMass ν q)).compProd (sectionKernel ν q) =
      (μ.prod ν).withDensity (Function.uncurry q) := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.sectionKernel
def OAI.Problem358.NormalizedSections.setDensity line 183
Source documentation
Indicator density of a measurable region in a product space.
```
def setDensity (U : Set (A × B)) (a : A) (b : B) : ℝ≥0∞ :=
…
```
theorem OAI.Problem358.NormalizedSections.measurable_setDensity line 186
theorem OAI.Problem358.NormalizedSections.sectionMass_setDensity line 191
Source documentation
The marginal density of a uniform region is exactly its section volume.
```
theorem sectionMass_setDensity (ν : Measure B) {U : Set (A × B)}
    (hU : MeasurableSet U) (a : A) :
    sectionMass ν (setDensity U) a = ν (Prod.mk a ⁻¹' U) := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.setDensity
theorem OAI.Problem358.NormalizedSections.sectionLaw_setDensity line 201
Source documentation
The conditional law of a region is the normalized restricted volume of its fiber.
```
theorem sectionLaw_setDensity (ν : Measure B) {U : Set (A × B)}
    (hU : MeasurableSet U) (a : A) :
    sectionLaw ν (setDensity U) a =
      (ν (Prod.mk a ⁻¹' U))⁻¹ • ν.restrict (Prod.mk a ⁻¹' U) := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionLaw, OAI.Problem358.NormalizedSections.setDensity

theorem OAI.Problem358.NormalizedSections.compProd_setSections line 215

Source documentation

Disintegrating the restriction to a region gives its volume marginal and uniform fibers.

theorem compProd_setSections (μ : Measure A) [SFinite μ]
    (ν : Measure B) [SFinite ν] {U : Set (A × B)} (hU : MeasurableSet U)
    (hfin : ∀ᵐ a ∂μ, ν (Prod.mk a ⁻¹' U) ≠ ∞) :
    (μ.withDensity (sectionMass ν (setDensity U))).compProd
      (sectionKernel ν (setDensity U)) = (μ.prod ν).restrict U := by
…

Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.setDensity, OAI.Problem358.NormalizedSections.sectionKernel

theorem OAI.Problem358.NormalizedSections.compProd_setSections_of_finite line 230
Source documentation
Finite mass of the whole region discharges the only section-finiteness premise.
```
theorem compProd_setSections_of_finite (μ : Measure A) [SFinite μ]
    (ν : Measure B) [SFinite ν] {U : Set (A × B)} (hU : MeasurableSet U)
    (hfin : (μ.prod ν) U ≠ ∞) :
    (μ.withDensity (sectionMass ν (setDensity U))).compProd
      (sectionKernel ν (setDensity U)) = (μ.prod ν).restrict U := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.setDensity, OAI.Problem358.NormalizedSections.sectionKernel
def OAI.Problem358.NormalizedSections.goodSections line 243
Source documentation
Positive, finite fibers form a measurable parameter set.
```
def goodSections (ν : Measure B) (q : A → B → ℝ≥0∞) : Set A :=
…
```
theorem OAI.Problem358.NormalizedSections.measurableSet_goodSections line 246

def OAI.Problem358.NormalizedSections.completedSectionKernel line 253

Source documentation

Complete the conditional kernel by any fixed point on exceptional fibers.

def completedSectionKernel (ν : Measure B) [SFinite ν]
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q)) (b₀ : B) :
    ProbabilityTheory.Kernel A B :=
…

theorem OAI.Problem358.NormalizedSections.isMarkovKernel_completedSectionKernel line 259
theorem OAI.Problem358.NormalizedSections.completedSectionKernel_ae_eq line 274
Source documentation
Exceptional-fiber completion does not change the conditional law marginal-a.e.
```
theorem completedSectionKernel_ae_eq (μ : Measure A) (ν : Measure B) [SFinite ν]
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q)) (b₀ : B)
    (hfin : ∀ᵐ a ∂μ, sectionMass ν q a ≠ ∞) :
    completedSectionKernel ν hq b₀ =ᵐ[μ.withDensity (sectionMass ν q)] sectionKernel ν q := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.completedSectionKernel, OAI.Problem358.NormalizedSections.sectionKernel

theorem OAI.Problem358.NormalizedSections.compProd_completedSectionKernel line 284

Source documentation

Exact disintegration with a total Markov kernel, hence ready for measurable sampling.

theorem compProd_completedSectionKernel (μ : Measure A) [SFinite μ]
    (ν : Measure B) [SFinite ν]
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q)) (b₀ : B)
    (hfin : ∀ᵐ a ∂μ, sectionMass ν q a ≠ ∞) :
    (μ.withDensity (sectionMass ν q)).compProd (completedSectionKernel ν hq b₀) =
      (μ.prod ν).withDensity (Function.uncurry q) := by
…

Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.completedSectionKernel

theorem OAI.Problem358.NormalizedSections.isProbabilityMeasure_normalizedSetMarginal line 297

Source documentation

The section-mass marginal of a finite positive region, after normalization, is a probability measure.

theorem isProbabilityMeasure_normalizedSetMarginal (μ : Measure A) [SFinite μ]
    (ν : Measure B) [SFinite ν] {U : Set (A × B)} (hU : MeasurableSet U)
    (h0 : (μ.prod ν) U ≠ 0) (hfin : (μ.prod ν) U ≠ ∞) :
    IsProbabilityMeasure
      (((μ.prod ν) U)⁻¹ • μ.withDensity (sectionMass ν (setDensity U))) := by
…

Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.setDensity

theorem OAI.Problem358.NormalizedSections.compProd_uniformSetSections line 311
Source documentation
Exact probability-level disintegration of a uniform region. The total Markov kernel still uses the unnormalized fiber density, so all normalization of the whole region is confined to the prefix marginal.
```
theorem compProd_uniformSetSections (μ : Measure A) [SFinite μ]
    (ν : Measure B) [SFinite ν] {U : Set (A × B)} (hU : MeasurableSet U)
    (b₀ : B) (hfin : (μ.prod ν) U ≠ ∞) :
    (((μ.prod ν) U)⁻¹ • μ.withDensity (sectionMass ν (setDensity U))).compProd
      (completedSectionKernel ν (measurable_setDensity hU) b₀) =
      ((μ.prod ν) U)⁻¹ • (μ.prod ν).restrict U := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.setDensity, OAI.Problem358.NormalizedSections.completedSectionKernel, OAI.Problem358.NormalizedSections.measurable_setDensity
def OAI.Problem358.normalizedDensityMeasure line 341
Source documentation
A density section normalized to have total mass one.
```
def normalizedDensityMeasure {A : Type*} (f : A × ℝ → ℝ≥0∞) (a : A) : Measure ℝ :=
…
```
lemma OAI.Problem358.normalizedDensityMeasure_isProbability line 344
lemma OAI.Problem358.measurable_normalizedDensityMeasure_apply line 353
lemma OAI.Problem358.measurable_cdf_normalizedDensityMeasure line 360
def OAI.Problem358.normalizedDensityKernel line 377
Source documentation
The normalized sections form a measurable kernel, even before probability assumptions are imposed on their total masses.
```
def normalizedDensityKernel {A : Type*} [MeasurableSpace A]
    (f : A × ℝ → ℝ≥0∞) (hf : Measurable f) : Kernel A ℝ where
…
```
lemma OAI.Problem358.normalizedDensityKernel_apply line 383
lemma OAI.Problem358.normalizedDensityKernel_isMarkov line 387
lemma OAI.Problem358.normalizedDensityMeasure_eq_withDensity line 396
lemma OAI.Problem358.cdf_normalizedDensityMeasure_eq line 402
lemma OAI.Problem358.cdf_normalizedDensityMeasure_ofReal line 412
lemma OAI.Problem358.measurableSet_validDensityParameters line 432
def OAI.Problem358.probabilityDensityKernel line 439
Source documentation
A globally Markov version, using a fixed point mass at invalid density sections.
```
def probabilityDensityKernel {A : Type*} [MeasurableSpace A]
    (f : A × ℝ → ℝ≥0∞) (hf : Measurable f) (x₀ : ℝ) : Kernel A ℝ :=
…
```
lemma OAI.Problem358.probabilityDensityKernel_apply line 444
instance OAI.Problem358.probabilityDensityKernel_isMarkov line 452
lemma OAI.Problem358.probabilityDensityKernel_apply_of_valid line 462
lemma OAI.Problem358.measurable_cdf_probabilityDensityKernel line 468
lemma OAI.Problem358.measurable_cdf_kernel_joint line 476
Source documentation
The CDF of a real-valued Markov kernel is jointly measurable in the parameter and the evaluation point.
```
lemma measurable_cdf_kernel_joint {A : Type*} [MeasurableSpace A]
    (κ : Kernel A ℝ) [IsMarkovKernel κ] :
    Measurable (fun p : A × ℝ => cdf (κ p.1) p.2) := by
…
```
theorem OAI.Problem358.NormalizedSections.ae_goodSections_normalizedSetMarginal line 503
Source documentation
Under the section-mass marginal, zero and infinite fibers are negligible as soon as the whole region has finite mass. This remains true after the total-volume normalization.
```
theorem ae_goodSections_normalizedSetMarginal
    (μ : Measure A) [SFinite μ] (ν : Measure B) [SFinite ν]
    {U : Set (A × B)} (hU : MeasurableSet U)
    (hfin : (μ.prod ν) U ≠ ∞) :
    ∀ᵐ a ∂(((μ.prod ν) U)⁻¹ •
      μ.withDensity (sectionMass ν (setDensity U))),
      a ∈ goodSections ν (setDensity U) := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.setDensity, OAI.Problem358.NormalizedSections.goodSections

theorem OAI.Problem358.NormalizedSections.map_prod_uniformSet_of_sectionLaws line 523

Source documentation

Sampling the normalized prefix marginal and then the uniform conditional fiber gives exactly the uniform law on the whole region. Conditional laws are required only on positive finite fibers; no choice on exceptional fibers is part of the interface.

theorem map_prod_uniformSet_of_sectionLaws
    (μ : Measure A) [SFinite μ] (ν : Measure B) [SFinite ν]
    (σ : Measure S) [SFinite σ] (η : Measure T) [SFinite η]
    {U : Set (A × B)} (hU : MeasurableSet U)
    (hfin : (μ.prod ν) U ≠ ∞)
    (b₀ : B) (F : S → A) (Q : A → T → B)
    (hF : Measurable F) (hQ : Measurable (Function.uncurry Q))
    (hbase : Measure.map F σ =
      ((μ.prod ν) U)⁻¹ • μ.withDensity (sectionMass ν (setDensity U)))
    (hfiber : ∀ a ∈ goodSections ν (setDensity U),
      Measure.map (Q a) η = sectionLaw ν (setDensity U) a) :
    Measure.map (fun p : S × T => (F p.1, Q (F p.1) p.2)) (σ.prod η) =
…

Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.setDensity, OAI.Problem358.NormalizedSections.goodSections, OAI.Problem358.NormalizedSections.sectionLaw

theorem OAI.Problem358.NormalizedSections.ae_goodSections_smul_marginal line 560
Source documentation
Arbitrary joint densities have good fibers almost everywhere under their section-mass marginal. Finite section mass is only required base-almost everywhere.
```
theorem ae_goodSections_smul_marginal
    (μ : Measure A) (ν : Measure B) [SFinite ν]
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (c : ℝ≥0∞) (hfin : ∀ᵐ a ∂μ, sectionMass ν q a ≠ ∞) :
    ∀ᵐ a ∂c • μ.withDensity (sectionMass ν q), a ∈ goodSections ν q := by
…
```
Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.goodSections

theorem OAI.Problem358.NormalizedSections.map_prod_smulDensity_of_sectionLaws line 573

Source documentation

Density version of the sampling bridge, applicable when the joint density is a residual-tail volume rather than the indicator of a region. All global normalization is confined to the scalar c and the prefix marginal.

theorem map_prod_smulDensity_of_sectionLaws
    (μ : Measure A) [SFinite μ] (ν : Measure B) [SFinite ν]
    (σ : Measure S) [SFinite σ] (η : Measure T) [SFinite η]
    {q : A → B → ℝ≥0∞} (hq : Measurable (Function.uncurry q))
    (c : ℝ≥0∞) (hfin : ∀ᵐ a ∂μ, sectionMass ν q a ≠ ∞)
    (b₀ : B) (F : S → A) (Q : A → T → B)
    (hF : Measurable F) (hQ : Measurable (Function.uncurry Q))
    (hbase : Measure.map F σ = c • μ.withDensity (sectionMass ν q))
    (hfiber : ∀ a ∈ goodSections ν q,
      Measure.map (Q a) η = sectionLaw ν q a) :
    Measure.map (fun p : S × T => (F p.1, Q (F p.1) p.2)) (σ.prod η) =
      c • (μ.prod ν).withDensity (Function.uncurry q) := by
…

Mentions: OAI.Problem358.NormalizedSections.sectionMass, OAI.Problem358.NormalizedSections.goodSections, OAI.Problem358.NormalizedSections.sectionLaw