OAI/NumberTheory/DukePrimeDegree/Entropy/NameErrorEntropy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.conditionalVectorEntropy_le_sum line 14
2. theorem OAI.DukePrimeDegree.conditionalNameEntropy_le_errors line 52
3. theorem OAI.DukePrimeDegree.nameEntropy_le_reference_errors line 72

   Source documentation

   A finite list of reference names pays its logarithmic cardinality; the remaining cost is proportional to the expected number of errors.

   theorem nameEntropy_le_reference_errors {Y α β : Type*} [MeasurableSpace Y]
       [MeasurableSpace α] [MeasurableSingletonClass α]
       [MeasurableSpace β] [MeasurableSingletonClass β]
       [Fintype α] [Nonempty α] [DecidableEq α] [Fintype β]
       (μ : Measure Y) [IsProbabilityMeasure μ] (N : ℕ)
       (P : Y → Fin N → α) (hP : Measurable P)
       (r : Y → β) (hr : Measurable r) (v : β → Fin N → α)
       {δ ε : ℝ} (hδ : 0 < δ) (hδ1 : δ < 1)
       (herr : (∑ i : Fin N, μ.real {y | P y i ≠ v (r y) i}) ≤ ε*N) :
       observationEntropy μ P ≤ Real.log (Fintype.card β) +
         (N : ℝ)*rareLabelCost (Fintype.card α) δ ε := by
   …

   Mentions: OAI.DukePrimeDegree.rareLabelCost

4. theorem OAI.DukePrimeDegree.observationEntropyRate_le_approximate_names line 106
5. theorem OAI.DukePrimeDegree.name_errors_le_bad_visits line 135

   Source documentation

   Orbit errors confined to a fixed measurable bad set cost at most its measure at each coordinate.

   theorem name_errors_le_bad_visits {Y α : Type*} [MeasurableSpace Y]
       (μ : Measure Y) [IsFiniteMeasure μ] {T : Y → Y}
       (hT : MeasurePreserving T μ μ) (P : Y → α) (N : ℕ)
       (R : Y → Fin N → α) (B : Set Y) (hB : MeasurableSet B)
       (hbad : ∀ y i, P (T^[i.val] y) ≠ R y i → T^[i.val] y ∈ B) :
       (∑ i : Fin N, μ.real {y | P (T^[i.val] y) ≠ R y i}) ≤ (N : ℝ)*μ.real B := by
   …

6. theorem OAI.DukePrimeDegree.observationEntropyRate_le_fixed_reference_errors line 153

   Source documentation

   A fixed finite list of reference trajectories has zero asymptotic coding cost. Only the coordinate errors contribute to the entropy rate.

   theorem observationEntropyRate_le_fixed_reference_errors
       {Y α : Type*} [MeasurableSpace Y]
       [MeasurableSpace α] [MeasurableSingletonClass α]
       [Fintype α] [Nonempty α] [DecidableEq α]
       (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
       (hT : MeasurePreserving T μ μ) (P : Y → α) (hP : Measurable P)
       (M : ℕ) (r : ℕ → Y → Fin M) (hr : ∀ N, Measurable (r N))
       (v : ∀ N, Fin M → Fin N → α)
       {ε δ : ℝ} (hδ : 0 < δ) (hδ1 : δ < 1)
       (herr : ∀ N,
         (∑ i : Fin N, μ.real {y | P (T^[i.val] y) ≠ v N (r N y) i}) ≤ ε*N) :
       observationEntropyRate μ T P ≤ rareLabelCost (Fintype.card α) δ ε := by
   …

   Mentions: OAI.DukePrimeDegree.rareLabelCost

7. theorem OAI.DukePrimeDegree.observationEntropyRate_le_zero_of_fixed_reference_approximations line 192

   Source documentation

   Arbitrarily accurate approximation by a fixed finite list of trajectories forces zero entropy for a finite observation.

   theorem observationEntropyRate_le_zero_of_fixed_reference_approximations
       {Y α : Type*} [MeasurableSpace Y]
       [MeasurableSpace α] [MeasurableSingletonClass α]
       [Fintype α] [Nonempty α] [DecidableEq α]
       (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
       (hT : MeasurePreserving T μ μ) (P : Y → α) (hP : Measurable P)
       (happrox : ∀ ε : ℝ, 0 < ε →
         ∃ (M : ℕ) (r : ℕ → Y → Fin M) (v : ∀ N, Fin M → Fin N → α),
           (∀ N, Measurable (r N)) ∧ ∀ N,
             (∑ i : Fin N, μ.real {y | P (T^[i.val] y) ≠ v N (r N y) i}) ≤ ε*N) :
       observationEntropyRate μ T P ≤ 0 := by
   …