OAI/NumberTheory/DukePrimeDegree/Entropy/RootPrefixFutureMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DukePrimeDegree.RootPrefixBox.uncenteredIntrinsicProduct_eq_rebase_map line 24
2. lemma OAI.DukePrimeDegree.RootPrefixBox.uncenteredIntrinsicProduct_apply line 47
3. lemma OAI.DukePrimeDegree.RootPrefixBox.rebase_image_futureFiber line 61
4. lemma OAI.DukePrimeDegree.RootPrefixBox.uncenteredIntrinsicProduct_wholeFuture line 88

   Source documentation

   A box containing its whole future fiber computes the unrestricted intrinsic future mass exactly after rebasing at the sampled point.

   lemma uncenteredIntrinsicProduct_wholeFuture
       (B : RootPrefixBox C c hP₀ hf g)
       (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
       (ell : Fin (d+1) → ℝ) (hell : ∑ k, ell k=0) (Q : X (d+1) → ℕ)
       (hQ : Measurable Q) (m : ℕ)
       (z : (UpperRootTransverse (d+1) × V) × c.Time)
       (hcontained : {t | ∀ k : ℕ,
           Q ((fun x => rightAction x (diagonalOneParameter ell hell (-1)))^[k+m]
             (C.timeParam c hP₀ hf g (z.1,t))) =
           Q ((fun x => rightAction x (diagonalOneParameter ell hell (-1)))^[k+m]
             (C.timeParam c hP₀ hf g z))} ⊆ B.time) :
       B.uncenteredIntrinsicProduct μ z
   …

   Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.UpperRootTransverse

5. theorem OAI.DukePrimeDegree.RootPrefixBox.conditionalInformation_eq_wholeFuture_ratio line 119

   Source documentation

   Once a box contains the entire future fiber, its conditional present information is exactly the ratio of the two intrinsic future masses.

   theorem conditionalInformation_eq_wholeFuture_ratio
       (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)) μ]
       (ell : Fin (d+1) → ℝ) (hell : ∑ k, ell k=0) (Q : X (d+1) → ℕ)
       (hQ : Measurable Q)
       (hgood : ∀ᵐ x ∂μ, ∀ᶠ v in 𝓝 (completeRootChain (d+1)).zeroTime, ∀ k : ℕ,
         Q ((fun x => rightAction x (diagonalOneParameter ell hell (-1)))^[k]
           (rightAction x ((completeRootChain (d+1)).word v))) =
         Q ((fun x => rightAction x (diagonalOneParameter ell hell (-1)))^[k] x))
       (hcontained : ∀ᵐ z ∂B.coordinateMeasure μ,
         countableFutureFiber (fun x => rightAction x (diagonalOneParameter ell hell (-1)))
   …

   Mentions: OAI.DukePrimeDegree.RootPrefixBox, OAI.DukePrimeDegree.completeRootChain, OAI.DukePrimeDegree.countableFutureFiber