OAI/NumberTheory/DukePrimeDegree/Dynamics/SmallReturnRefinement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DukePrimeDegree.refined_return_information_le line 14
2. lemma OAI.DukePrimeDegree.tsum_option_eq line 53
3. theorem OAI.DukePrimeDegree.returnRefinement_information_le line 68

   Source documentation

   The refinement cost splits into section mass times a fixed grid cost, plus the chosen exponential rate times the Kac return-time moment.

   theorem returnRefinement_information_le
       {Y : Type*} [MeasurableSpace Y] (μ : Measure Y) [IsProbabilityMeasure μ]
       {T : Y → Y} (hT : MeasurePreserving T μ μ) (hE : MeasurableEmbedding T)
       {S : Set Y} (hS : MeasurableSet S)
       (K : ℕ → ℕ) (B : ∀ n, Y → Fin (K n)) (hB : ∀ n, Measurable (B n))
       {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b)
       (hcard : ∀ n, Real.log (K n) ≤ a+b*(n+1)) :
       (∑' z : Option (Σ n : ℕ, Fin (K n)),
         Real.negMulLog (μ.real {x | returnRefinement T S B x=z})) ≤
       (∑' n, Real.negMulLog (μ.real {x | firstReturnPartitionCode T S x=n}))+
         a*μ.real S+b := by
   …

   Mentions: OAI.DukePrimeDegree.returnRefinement, OAI.DukePrimeDegree.firstReturnPartitionCode