OAI/Geometry/HyperbolicGroups/Concentration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.TableModel.powerProbability_mem line 18
2. lemma OAI.HyperbolicObstruction.TableModel.powerProbability_pos line 24
3. lemma OAI.HyperbolicObstruction.TableModel.inverse_cost_product line 28
4. lemma OAI.HyperbolicObstruction.TableModel.cost_term_bound line 43
5. theorem OAI.HyperbolicObstruction.TableModel.variance_pinned_power line 69

   Source documentation

   A uniform, explicit finite relative-variance bound for pinned master matches. No numerical values of the pinned letters occur in this bound.

   theorem variance_pinned_power [Nonempty A] (support : R → Finset F) (c : R → ℝ)
       (hc : ∀ r, 0 ≤ c r) (I : Finset F) (ξ : F → A) {ε : ℝ}
       (gap : ∀ J : Finset R, J.Nonempty →
         ε ≤ ((J.biUnion support \ I).card : ℝ) - ∑ r ∈ J, c r) :
       let N : ℝ := Fintype.card A
   …

6. theorem OAI.HyperbolicObstruction.IncidenceTemplate.master_variance_bound line 115

   Source documentation

   Source single-copy concentration, also for every singleton-pinned count, with a common actual-parameter half-unit margin.

   theorem master_variance_bound {A : Type*} [Fintype A] [Nonempty A] [DecidableEq A]
       {α β δ : ℝ} (ha : 0 ≤ α) (hb : 7 * α ≤ β) (hd : 0 ≤ δ)
       (hsmall : β + 90 * δ ≤ 1 / 2) (I : Finset Field) (hI : I.card ≤ 1) (ξ : Field → A) :
       let N : ℝ := Fintype.card A
   …

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Field