OAI/NumberTheory/DukePrimeDegree/Entropy/SmallReturnPartition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniformly small entropy for return partitions of small sections

  1. lemma OAI.DukePrimeDegree.firstReturnLevel_real_mass_sum_le line 13
  2. lemma OAI.DukePrimeDegree.firstReturnLevel_real_mean_le_one line 26
  3. lemma OAI.DukePrimeDegree.firstReturnPartitionCode_zero_mass line 41
  4. lemma OAI.DukePrimeDegree.firstReturnPartitionCode_entropy_eq line 66
  5. theorem OAI.DukePrimeDegree.exists_small_section_return_entropy line 91

    Source documentation

    The entropy threshold is uniform in the measure-preserving map and section. In particular it may be chosen before the transverse return box.

    theorem exists_small_section_return_entropy
    {Y : Type*} [MeasurableSpace Y] {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (μ : Measure Y) [IsProbabilityMeasure μ]
      {T : Y → Y} (_hT : MeasurePreserving T μ μ) (_hE : MeasurableEmbedding T)
      {S : Set Y} (_hS : MeasurableSet S), μ.real S ≤ δ →
        (∑' n, Real.negMulLog (μ.real {x | firstReturnPartitionCode T S x=n})) < ε := by
…

    Mentions: OAI.DukePrimeDegree.firstReturnPartitionCode