OAI/NumberTheory/DukePrimeDegree/Entropy/RobustFiniteObservations.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DukePrimeDegree.continuous_quotientLogDistance_pair line 16
2. theorem OAI.DukePrimeDegree.compact_finite_observation_separation line 41
3. theorem OAI.DukePrimeDegree.compact_finite_reference_labels line 68

   Source documentation

   A reference point can be assigned a robust label even when the reference point itself lies outside the good compact set.

   theorem compact_finite_reference_labels {n M : ℕ}
       (K : Set (X n)) (hK : IsCompact K) (P : X n → Fin M)
       (hP : ContinuousOn P K) :
       ∃ (δ : ℝ) (R : X n → Fin M), 0 < δ ∧
         ∀ z y, y ∈ K → quotientLogDistance z y < δ → P y=R z := by
   …

   Mentions: OAI.DukePrimeDegree.quotientLogDistance

4. theorem OAI.DukePrimeDegree.exists_robust_finite_observation line 91