OAI/Geometry/HyperbolicGroups/GenericMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.BernoulliCandidates.overlap_power_bound line 19
2. lemma OAI.HyperbolicObstruction.BernoulliCandidates.sum_inverse_overlap_power line 35
3. theorem OAI.HyperbolicObstruction.BernoulliCandidates.variance_power line 77

   Source documentation

   The complete overlap-counting rule for row positions in possibly repeated arrays, before substituting a candidate-cardinality lower bound.

   theorem variance_power [Nonempty A] (row : (V → A) → S → I)
       (support : S → Finset V)
       (read : ∀ σ τ s, row σ s = row τ s → ∀ v ∈ support s, σ v = τ v)
       (p : I → ℝ) (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1) (C : Finset (V → A))
       (hi : ∀ σ ∈ C, Function.Injective (row σ)) (c : S → ℝ)
       (hq : ∀ σ ∈ C, ∀ s, p (row σ s) = (Fintype.card A : ℝ) ^ (-c s))
       {ε : ℝ} (gap : ∀ J : Finset S, J.Nonempty →
         ε ≤ ((J.biUnion support).card : ℝ) - ∑ s ∈ J, c s) :
       (FiniteLaw.bernoulliProduct p hp).variance (fun w => (count row C w : ℝ)) ≤
         (∏ s, (Fintype.card A : ℝ) ^ (-c s)) ^ 2 * C.card *
         (Fintype.card (OverlapType S) * (Fintype.card A : ℝ) ^ Fintype.card V *
           (Fintype.card A : ℝ) ^ (-ε)) := by
   …

   Mentions: OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.BernoulliCandidates.count, OAI.HyperbolicObstruction.BernoulliCandidates.OverlapType

4. theorem OAI.HyperbolicObstruction.BernoulliCandidates.relative_variance_power line 102

   Source documentation

   Explicit relative variance; the lower cardinality is proved below from fieldwise injectivity, not assumed as a sampling conclusion.

   theorem relative_variance_power [Nonempty A] (row : (V → A) → S → I)
       (support : S → Finset V)
       (read : ∀ σ τ s, row σ s = row τ s → ∀ v ∈ support s, σ v = τ v)
       (p : I → ℝ) (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1) (C : Finset (V → A))
       (hi : ∀ σ ∈ C, Function.Injective (row σ)) (c : S → ℝ)
       (hq : ∀ σ ∈ C, ∀ s, p (row σ s) = (Fintype.card A : ℝ) ^ (-c s))
       (hC : ((Fintype.card A : ℝ) / 2) ^ Fintype.card V ≤ C.card)
       {ε : ℝ} (gap : ∀ J : Finset S, J.Nonempty →
         ε ≤ ((J.biUnion support).card : ℝ) - ∑ s ∈ J, c s) :
       (FiniteLaw.bernoulliProduct p hp).variance (fun w => (count row C w : ℝ)) ≤
         Fintype.card (OverlapType S) * 2 ^ Fintype.card V * (Fintype.card A : ℝ) ^ (-ε) *
         ((FiniteLaw.bernoulliProduct p hp).expect (fun w => (count row C w : ℝ))) ^ 2 := by
   …

   Mentions: OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.BernoulliCandidates.count, OAI.HyperbolicObstruction.BernoulliCandidates.OverlapType