RootItineraryMass.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Positive finite intrinsic mass of actual future-itinerary atoms

The good cuts supply neighborhoods in root time. The actual intrinsic product gives every such neighborhood positive mass. Intersecting with the normalizing unit cube makes these masses finite and at most one.

def OAI.DukePrimeDegree.upperRootTimeProduct line 19
def OAI.DukePrimeDegree.rootFutureAtom line 24
lemma OAI.DukePrimeDegree.rootFutureAtom_measurable line 28
theorem OAI.DukePrimeDegree.ae_upperRootTimeProduct_nhds_pos line 40
theorem OAI.DukePrimeDegree.ae_upperRootTimeProduct_unit line 48

theorem OAI.DukePrimeDegree.exists_cuts_with_positive_finite_itinerary_mass line 57

Source documentation

These are actual intrinsic masses, with no new entropy or leaf disintegration hypothesis.

theorem exists_cuts_with_positive_finite_itinerary_mass (d : ℕ)
    (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0) (ε : ℝ) (hε : 0<ε)
    (hgap : ∀ p : allPositiveRoots (d+1), ε ≤ ell p.val.2-ell p.val.1)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ] :
    ∃ r : QuotientCutIndex → ℝ,
      (∀ i, (i.2.val.1 : ℝ)<r i ∧ r i<(i.2.val.2 : ℝ)) ∧
      ∀ᵐ x ∂μ, ∀ n : ℕ,
        0 < upperRootTimeProduct (d+1) μ x
          (rootFutureAtom (fun y => rightAction y (diagonalOneParameter ell hell (-1)))
            (quotientCutObservation r n) x ∩ (completeRootChain (d+1)).cube 1) ∧
        upperRootTimeProduct (d+1) μ x
…

Mentions: OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.QuotientCutIndex, OAI.DukePrimeDegree.upperRootTimeProduct, OAI.DukePrimeDegree.rootFutureAtom, OAI.DukePrimeDegree.quotientCutObservation, OAI.DukePrimeDegree.completeRootChain