OAI/NumberTheory/DukePrimeDegree/Entropy/FiniteBlockEntropy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.observationEntropyRate_le_of_refines line 16
2. theorem OAI.DukePrimeDegree.observationEntropyRate_comp_commuting line 35
3. def OAI.DukePrimeDegree.blockWordEquiv line 52
4. lemma OAI.DukePrimeDegree.orbitName_blocks line 62
5. theorem OAI.DukePrimeDegree.observationEntropyRate_blocks line 73
6. theorem OAI.DukePrimeDegree.observationEntropyRate_sampled_window_le line 108

   Source documentation

   Observing a fixed finite window at every q-th step has at most q times the entropy rate of the underlying observation.

   theorem observationEntropyRate_sampled_window_le {Y α : Type*}
       [MeasurableSpace Y] [Fintype α]
       (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
       (hT : MeasurePreserving T μ μ) (P : Y → α)
       (hP : ∀ a, MeasurableSet {y | P y=a}) {q : ℕ} (hq : 0 < q) (W : ℕ) :
       observationEntropyRate μ (T^[q]) (orbitName T P W) ≤
         (q : ℝ)*observationEntropyRate μ T P := by
   …

7. theorem OAI.DukePrimeDegree.observationEntropyRate_iterate_le line 163

   Source documentation

   Sampling a finite observation every q steps costs at most q times its original entropy rate.

   theorem observationEntropyRate_iterate_le {Y α : Type*}
       [MeasurableSpace Y] [Fintype α]
       (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
       (hT : MeasurePreserving T μ μ) (P : Y → α)
       (hP : ∀ a, MeasurableSet {y | P y=a}) {q : ℕ} (hq : 0 < q) :
       observationEntropyRate μ (T^[q]) P ≤ (q : ℝ)*observationEntropyRate μ T P := by
   …

8. theorem OAI.DukePrimeDegree.observationEntropyRate_le_block_conditional line 176
9. theorem OAI.DukePrimeDegree.observationEntropyRate_le_window_conditional line 195

   Source documentation

   A long block of the first observation can be conditioned on any fixed window of the second observation.

   theorem observationEntropyRate_le_window_conditional
       {Y α β : Type*} [MeasurableSpace Y] [Fintype α] [Fintype β]
       (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
       (hT : MeasurePreserving T μ μ) (P : Y → α) (Q : Y → β)
       (hP : ∀ a, MeasurableSet {y | P y=a})
       (hQ : ∀ a, MeasurableSet {y | Q y=a}) {q : ℕ} (hq : 0 < q) (W : ℕ) :
       observationEntropyRate μ T P ≤ observationEntropyRate μ T Q+
         conditionalObservationEntropy μ (orbitName T P q) (orbitName T Q W)/(q : ℝ) := by
   …