BranchingSubordinateObservation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded future observation with finite branching

The same low-entropy height and small relative charts provide the weak-stable and neutral fiber properties, with uniformly finite predecessor labels.

theorem OAI.DukePrimeDegree.exists_bounded_branching_subordinate_observation_with_lifts line 25

Source documentation

The branching observation also retains the uniform radial injectivity radius and a single lift whose every future conjugate is radially small.

theorem exists_bounded_branching_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, quotientLogDistance (Quotient.mk _ (1 : G (d+1))) x ≤ 2*B*(H x:ℝ)+B) ∧
      (∀ x, Set.InjOn (fun g => rightAction x g)
        (matrixBall (d+1) (r₀*Real.exp (-(4*B)*(H x:ℝ))))) ∧
      (∀ m, IsCompact {x | H x ≤ m}) ∧
…

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

theorem OAI.DukePrimeDegree.exists_bounded_branching_subordinate_observation line 203

Source documentation

A bounded subordinate observation with uniformly finite branching.

theorem exists_bounded_branching_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