RowLeafProduct.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Product disintegration in actual row boxes

Neutral holonomy removes dependence of a normalized one-root leaf on the other row coordinates. Nested disintegration then gives the one-coordinate product step in a cubical row box.

theorem OAI.DukePrimeDegree.rowBox_ae_nested_of_single line 22

theorem OAI.DukePrimeDegree.rowBox_ae_real_conditionals_constant line 58

Source documentation

In a cubical row box, the selected real coordinate is independent of the other row coordinates, conditional on the transverse coordinate.

theorem rowBox_ae_real_conditionals_constant
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j) {k : Fin (d + 1)}
    (B : RowRootBox i k) {R : ℝ} (hR : 0 < R) (hT : B.time = rowCube i R)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    ∀ᵐ s ∂(rowSplitMeasure hij (B.coordinateMeasure μ)).fst,
      ∃ ν : Measure ℝ, IsProbabilityMeasure ν ∧
        ∀ᵐ w ∂((rowSplitMeasure hij (B.coordinateMeasure μ)).condKernel s).fst,
          ((rowSplitMeasure hij (B.coordinateMeasure μ)).condKernel s).condKernel w = ν := by
…

Mentions: OAI.DukePrimeDegree.RowRootBox, OAI.DukePrimeDegree.rowCube, OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.rowSplitMeasure

theorem OAI.DukePrimeDegree.rowBox_ae_conditional_eq_prod line 128

Source documentation

The actual conditional row measure splits into its marginal on the remaining coordinates and its marginal on the selected coordinate.

theorem rowBox_ae_conditional_eq_prod
    (d : ℕ) {i j : Fin (d + 1)} (hij : i ≠ j) {k : Fin (d + 1)}
    (B : RowRootBox i k) {R : ℝ} (hR : 0 < R) (hT : B.time = rowCube i R)
    (μ : Measure (X (d + 1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u)) = μ) :
    ∀ᵐ s ∂(rowSplitMeasure hij (B.coordinateMeasure μ)).fst,
      (rowSplitMeasure hij (B.coordinateMeasure μ)).condKernel s =
        ((rowSplitMeasure hij (B.coordinateMeasure μ)).condKernel s).fst.prod
          ((rowSplitMeasure hij (B.coordinateMeasure μ)).condKernel s).snd := by
…

Mentions: OAI.DukePrimeDegree.RowRootBox, OAI.DukePrimeDegree.rowCube, OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.rowSplitMeasure