OAI/Geometry/HyperbolicGroups/StarVariance.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.StarModel.leafCount line 19
2. abbrev OAI.HyperbolicObstruction.StarModel.extensionCount line 24
3. lemma OAI.HyperbolicObstruction.StarModel.branch_pin_fieldwise line 30
4. lemma OAI.HyperbolicObstruction.StarModel.ext_injective line 40
5. lemma OAI.HyperbolicObstruction.StarModel.ext_surcharge_le line 46
6. instance OAI.HyperbolicObstruction.IncidenceTemplate.instRowFintype line 60

   Source documentation

   Named finite instances avoid repeatedly synthesizing the literal nested subtype.

   instance instRowFintype : Fintype Row := inferInstance

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Row

7. instance OAI.HyperbolicObstruction.IncidenceTemplate.instFieldFintype line 61
8. lemma OAI.HyperbolicObstruction.IncidenceTemplate.star_extension_actual_gap line 66
9. theorem OAI.HyperbolicObstruction.IncidenceTemplate.leaf_variance_bound line 84

   Source documentation

   Relative variance for the literal fieldwise-injective leaf count. The alphabet size threshold and constants are independent of pinned letter values.

   theorem leaf_variance_bound {α β δ : ℝ} (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)
       (ξ : StarModel.Var (B := B) U → A)
   …

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

10. theorem OAI.HyperbolicObstruction.IncidenceTemplate.extension_variance_bound line 108

    Source documentation

    Unconditioned variance for the residual trials of an extension. The next conditioning identity identifies this with variance given the fixed match.

    theorem extension_variance_bound {α β δ : ℝ} (ha : 0 ≤ α) (hb : 7 * α ≤ β) (hd : 0 ≤ δ)
        (hsmall : (Fintype.card B : ℝ) * (β + 90 * δ) ≤ 1 / 2)
        (U : Finset Field) (j₀ : B)
        (gap : ∀ W, W.Nonempty → Disjoint U W → 1 ≤ pattern.exponent (U ∪ W) - pattern.exponent U)
        (ξ : StarModel.Var (B := B) U → A)
    …

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