OAI/Geometry/HyperbolicGroups/StarRate.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.actualProbability line 18
2. lemma OAI.HyperbolicObstruction.IncidenceTemplate.actualProbability_mem line 22
3. lemma OAI.HyperbolicObstruction.IncidenceTemplate.actualProbability_pos line 28
4. def OAI.HyperbolicObstruction.IncidenceTemplate.extensionRate line 31
5. def OAI.HyperbolicObstruction.IncidenceTemplate.leafRate line 35
6. def OAI.HyperbolicObstruction.IncidenceTemplate.errorRate line 39
7. lemma OAI.HyperbolicObstruction.IncidenceTemplate.errorRate_tendsto line 43
8. theorem OAI.HyperbolicObstruction.IncidenceTemplate.expectedError_le line 63

   Source documentation

   All constants in the error estimate are independent of the alphabet, parameters and the pinned values. Only the fixed finite star template remains.

   theorem expectedError_le {α β δ : ℝ} (ha : 0 ≤ α) (hb : 7*α ≤ β) (hd : 0 ≤ δ)
       (hsmall : (Fintype.card B : ℝ) * (β+90*δ) ≤ 1/2)
       (U : Finset Field) (e : Field) (he : e ∉ U)
       (gap : ∀ W, W.Nonempty → Disjoint U W → 1 ≤ pattern.exponent (U ∪ W) - pattern.exponent U)
       (a₀ : A) (b₀ : B ↪ A) (hN : 4 * Fintype.card (StarModel.Var (B := B) U) ≤ Fintype.card A) :
   …

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.StarModel.Var