OAI/NumberTheory/DukePrimeDegree/Entropy/BoundedFutureObservation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.exists_bounded_low_entropy_subordinate_observation_with_lifts line 18

   Source documentation

   A bounded subordinate observation retaining its radial height, injectivity radius, and the smallness of every future conjugate lift.

   theorem exists_bounded_low_entropy_subordinate_observation_with_lifts (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 μ]
       (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
       {ε : ℝ} (hε : 0 < ε) :
       ∃ (B r₀ : ℝ) (H Q : X (d+1) → ℕ),
         0 < B ∧ 0 < r₀ ∧ r₀ ≤ 1 ∧ Measurable H ∧ Measurable Q ∧
         (∀ x, H (rightAction x (diagonalOneParameter ell hell (-1))) ≤ H x+1 ∧
           H x ≤ H (rightAction x (diagonalOneParameter ell hell (-1)))+1) ∧
         (∀ x, quotientLogDistance (Quotient.mk _ (1 : G (d+1))) x ≤ 2*B*(H x:ℝ)+B) ∧
         (∀ m, IsCompact {x | H x ≤ m}) ∧
   …

   Mentions: OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.quotientLogDistance

2. theorem OAI.DukePrimeDegree.exists_bounded_low_entropy_subordinate_observation line 124

   Source documentation

   A bounded subordinate observation with small radial lifts.

   theorem exists_bounded_low_entropy_subordinate_observation (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 μ]
       (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
       {ε : ℝ} (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 y, (∀ k : ℕ,
   …

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