OAI/NumberTheory/DukePrimeDegree/Entropy/BoundedFutureMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.exists_low_entropy_positive_future_mass line 17

   Source documentation

   The entire future atom has positive finite intrinsic mass. No intersection with an auxiliary bounded leaf box is needed.

   theorem exists_low_entropy_positive_future_mass (d : ℕ)
       (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
       (hgap : ∀ p : allPositiveRoots (d+1), Real.log 4 ≤ ell p.val.2-ell p.val.1)
       (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
       [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
       {ε : ℝ} (hε : 0 < ε) :
       ∃ H Q : X (d+1) → ℕ, Measurable H ∧ Measurable Q ∧
         (∀ m, IsCompact {x | H x ≤ m}) ∧
         (∀ m, (Q '' {x | H x ≤ m}).Finite) ∧
         (∀ N, observationEntropyRate μ
           (fun x => rightAction x (diagonalOneParameter ell hell (-1))) (heightClip H N) < ε) ∧
         ∀ᵐ x ∂μ,
   …

   Mentions: OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.heightClip

2. theorem OAI.DukePrimeDegree.exists_low_entropy_integrable_future_information line 61

   Source documentation

   The subordinate observation can be chosen with arbitrarily small height entropy and an integrable whole-future information function. Its canonical mean is proved, rather than assumed as leaf data.

   theorem exists_low_entropy_integrable_future_information (d : ℕ)
       (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
       (hgap : ∀ p : allPositiveRoots (d+1), Real.log 4 ≤ ell p.val.2-ell p.val.1)
       (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
       [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
       {ε : ℝ} (hε : 0 < ε) :
       ∃ H Q : X (d+1) → ℕ, Measurable H ∧ Measurable Q ∧
         (∀ m, IsCompact {x | H x ≤ m}) ∧
         (∀ m, (Q '' {x | H x ≤ m}).Finite) ∧
         (∀ N, observationEntropyRate μ
           (fun x => rightAction x (diagonalOneParameter ell hell (-1))) (heightClip H N) < ε) ∧
         let c := completeRootChain (d+1)
   …

   Mentions: OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.heightClip, OAI.DukePrimeDegree.completeRootChain