OAI/NumberTheory/DukePrimeDegree/Entropy/FirstReturnPartition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The actual measurable first-return partition

The positive return levels cover almost every point of the section. The exceptional nonreturning set is included with the complement of the section in the zero label, so the resulting partition is defined everywhere.

  1. lemma OAI.DukePrimeDegree.exists_firstReturnLevel_of_return line 18
  2. theorem OAI.DukePrimeDegree.ae_section_mem_firstReturnLevel line 29
  3. def OAI.DukePrimeDegree.firstReturnPartitionAtom line 40
  4. lemma OAI.DukePrimeDegree.firstReturnPartition_covers line 44
  5. def OAI.DukePrimeDegree.firstReturnPartitionCode line 52
  6. lemma OAI.DukePrimeDegree.firstReturnPartitionCode_mem line 55
  7. lemma OAI.DukePrimeDegree.firstReturnPartitionAtom_unique line 59
  8. lemma OAI.DukePrimeDegree.firstReturnPartitionCode_eq_iff line 72
  9. lemma OAI.DukePrimeDegree.measurable_firstReturnPartitionCode line 80
  10. lemma OAI.DukePrimeDegree.firstReturnPartitionCode_eq_of_future_section line 91

    Source documentation

    Passing from section membership to the first-return code does not change equality of future itineraries (EL, paragraph 7.49).

    lemma firstReturnPartitionCode_eq_of_future_section
    {Y : Type*} (T : Y → Y) (S : Set Y) (x y : Y)
    (hxy : ∀ k : ℕ, T^[k] x ∈ S ↔ T^[k] y ∈ S) :
    firstReturnPartitionCode T S x=firstReturnPartitionCode T S y := by
…

    Mentions: OAI.DukePrimeDegree.firstReturnPartitionCode

  11. lemma OAI.DukePrimeDegree.firstReturnPartitionCode_future_eq_of_future_section line 119
  12. theorem OAI.DukePrimeDegree.firstReturnPartitionCode_information_summable line 130

    Source documentation

    The everywhere-defined return code has finite Shannon entropy.

    theorem firstReturnPartitionCode_information_summable
    {Y : Type*} [MeasurableSpace Y] (μ : Measure Y) [IsProbabilityMeasure μ]
    {T : Y → Y} (hT : MeasurePreserving T μ μ) (hE : MeasurableEmbedding T)
    {S : Set Y} (hS : MeasurableSet S) :
    Summable (fun n => Real.negMulLog (μ.real {x | firstReturnPartitionCode T S x=n})) := by
…

    Mentions: OAI.DukePrimeDegree.firstReturnPartitionCode