OAI/NumberTheory/DukePrimeDegree/Dynamics/SmallFineReturnRefinement.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DukePrimeDegree.log_scaled_exponential_grid_bound line 12
2. theorem OAI.DukePrimeDegree.exists_small_entropy_return_refinement line 42

   Source documentation

   The section mass threshold is chosen before its transverse geometry. The positive exponential rate can be arbitrarily small and still forces arbitrarily fine cells on unbounded return levels.

   theorem exists_small_entropy_return_refinement
       {Y : Type*} [MeasurableSpace Y] {d : ℕ} {R ε : ℝ}
       (hR : 0 ≤ R) (hε : 0 < ε) :
       ∃ δ : ℝ, 0 < δ ∧ ∀ (μ : Measure Y) [IsProbabilityMeasure μ]
         {T : Y → Y} (_hT : MeasurePreserving T μ μ) (_hE : MeasurableEmbedding T)
         {S : Set Y} (_hS : MeasurableSet S), μ.real S ≤ δ →
         ∀ (f : Y → Fin d → ℝ), Measurable f →
           (∀ x ∈ S, ∀ i, |f x i| ≤ R) →
         ∃ (α : ℝ) (K : ℕ → ℕ) (B : ∀ n, Y → Fin (K n)), 0 < α ∧
           (∀ n, Measurable (B n)) ∧
           Summable (fun z : Option (Σ n : ℕ, Fin (K n)) =>
             Real.negMulLog (μ.real {x | returnRefinement T S B x=z})) ∧
   …

   Mentions: OAI.DukePrimeDegree.returnRefinement