OAI/Geometry/HyperbolicGroups/Moment.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.FiniteLaw.variance line 16
2. lemma OAI.HyperbolicObstruction.FiniteLaw.variance_nonneg line 19
3. lemma OAI.HyperbolicObstruction.FiniteLaw.variance_eq line 22
4. lemma OAI.HyperbolicObstruction.FiniteLaw.expect_abs_sub_le line 29
5. lemma OAI.HyperbolicObstruction.FiniteLaw.markov line 33
6. lemma OAI.HyperbolicObstruction.FiniteLaw.chebyshev line 44
7. def OAI.HyperbolicObstruction.TableModel.candidateCount line 59
8. lemma OAI.HyperbolicObstruction.TableModel.expect_candidateCount line 63
9. lemma OAI.HyperbolicObstruction.TableModel.expect_candidateCount_sq line 83
10. def OAI.HyperbolicObstruction.TableModel.pinCandidates line 109

    Source documentation

    Arbitrary fixed named fields, not pairwise-distinct numerical letters.

    def pinCandidates (P : Finset F) (ξ : F → A) : Finset (F → A) :=
    …

11. lemma OAI.HyperbolicObstruction.TableModel.card_pinCandidates line 112
12. lemma OAI.HyperbolicObstruction.TableModel.sum_pin_coincidence line 117
13. lemma OAI.HyperbolicObstruction.TableModel.sum_pin_inverse_overlap line 141
14. lemma OAI.HyperbolicObstruction.TableModel.expect_pinCount_sq line 158

    Source documentation

    Exact second moment, uniform in all pinned values.

    lemma expect_pinCount_sq (support : R → Finset F) (p : R → ℝ)
        (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) (hpos : ∀ r, 0 < p r)
        (P : Finset F) (ξ : F → A) :
        (law support p hp).expect (fun w => (candidateCount support (pinCandidates P ξ) w : ℝ) ^ 2) =
          (∏ r, p r) ^ 2 * (Fintype.card A : ℝ) ^ (Fintype.card F - P.card) *
          ∑ J : Finset R, (Fintype.card A : ℝ) ^
            (Fintype.card F - (J.biUnion support ∪ P).card) *
            ∏ r ∈ J, ((p r)⁻¹ - 1) := by
    …

    Mentions: OAI.HyperbolicObstruction.TableModel.law, OAI.HyperbolicObstruction.TableModel.candidateCount, OAI.HyperbolicObstruction.TableModel.pinCandidates

15. lemma OAI.HyperbolicObstruction.TableModel.variance_pinCount line 181

    Source documentation

    Every nonempty row overlap, and only those overlaps, contributes to variance.

    lemma variance_pinCount (support : R → Finset F) (p : R → ℝ)
        (hp : ∀ r, p r ∈ Set.Icc (0 : ℝ) 1) (hpos : ∀ r, 0 < p r)
        (P : Finset F) (ξ : F → A) :
        (law support p hp).variance (fun w => (candidateCount support (pinCandidates P ξ) w : ℝ)) =
          (∏ r, p r) ^ 2 * (Fintype.card A : ℝ) ^ (Fintype.card F - P.card) *
          ∑ J ∈ (Finset.univ : Finset (Finset R)).erase ∅, (Fintype.card A : ℝ) ^
            (Fintype.card F - (J.biUnion support ∪ P).card) *
            ∏ r ∈ J, ((p r)⁻¹ - 1) := by
    …

    Mentions: OAI.HyperbolicObstruction.TableModel.law, OAI.HyperbolicObstruction.TableModel.candidateCount, OAI.HyperbolicObstruction.TableModel.pinCandidates