LocalFutureKernelConstancy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise constancy of the actual future kernel on a conull chart

The normalized leaf measure depends only on the transverse coordinate. After removing one null set, equal transverse coordinates and equal complete future names therefore give exactly the same ambient kernel. This is stronger than constancy for almost every pair sampled from that kernel, and is the local input for the refined-future entropy comparison.

lemma OAI.DukePrimeDegree.RootPrefixBox.ae_coordinates_mem_of_ae_coordinateMeasure line 28
theorem OAI.DukePrimeDegree.RootPrefixBox.exists_conull_futureKernel_coordinate_constancy line 47

theorem OAI.DukePrimeDegree.RootPrefixBox.exists_conull_futureKernel_chart_constancy line 96

Source documentation

One ambient conull set works for every pair of coordinates in this actual injective box, rather than merely for almost every sampled pair.

theorem exists_conull_futureKernel_chart_constancy
    (B : RootPrefixBox C c hP hf g) (R : ℝ) (hBR : B.time ⊆ c.remainingWindow R 0)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    (hfree : ∀ᵐ x ∂μ, ∀ v ∈ positiveRootGeneratedGroup (allPositiveRoots (d+1)),
      rightAction x v=x → v=1)
    (ell : Fin (d+1) → ℝ) (hell : ∑ k, ell k=0)
    (Q : X (d+1) → ℕ)
    (κ : Kernel (X (d+1)) (X (d+1)))
    (hκ : ∀ᵐ x ∂μ, κ x=
      ((anchorNormalize (c.remainingTimeProduct hP hf μ x)
        (c.remainingFutureAtom ell hell Q 1 x)).restrict
…

Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.positiveRootGeneratedGroup, OAI.DukePrimeDegree.allPositiveRoots