OAI/NumberTheory/DukePrimeDegree/Geometry/RowIndependentCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Every row conditional is a product of its root coordinates

The neutral-holonomy splitting holds for each coordinate. This gives mutual independence, not just pairwise independence, because each coordinate is independent of the entire tuple of remaining coordinates.

  1. abbrev OAI.DukePrimeDegree.RowCoordinate line 20
  2. def OAI.DukePrimeDegree.rowCoordinates line 22
  3. lemma OAI.DukePrimeDegree.rowSplitMeasure_fst line 25
  4. theorem OAI.DukePrimeDegree.rowBox_ae_mapped_conditional_eq_prod line 33
  5. theorem OAI.DukePrimeDegree.rowCoordinates_independent_of_splittings line 51
  6. theorem OAI.DukePrimeDegree.rowBox_ae_joint_law_eq_pi line 88

    Source documentation

    The actual row leaf law in elementary-root coordinates is the product of its one-root marginals.

    theorem rowBox_ae_joint_law_eq_pi
    (d : ℕ) {i 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 ∂(B.coordinateMeasure μ).fst,
      (B.conditionalKernel μ s).map (rowCoordinates i) =
        Measure.pi (fun j : RowCoordinate i =>
          (B.conditionalKernel μ s).map (fun a => a.val j.val)) := by
…

    Mentions: OAI.DukePrimeDegree.RowRootBox, OAI.DukePrimeDegree.rowCube, OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.rowCoordinates, OAI.DukePrimeDegree.RowCoordinate