OAI/Geometry/HyperbolicGroups/GenericTable.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.BernoulliCandidates.Present line 19

    Source documentation

    Row positions of a candidate may belong to the same array. Actual trials, not row positions, are the independent Bernoulli variables.

    def Present (row : (V → A) → S → I) (w : I → Bool) (σ : V → A) : Prop :=
…
  2. instance OAI.HyperbolicObstruction.BernoulliCandidates.(instance at line 22) line 22
  3. def OAI.HyperbolicObstruction.BernoulliCandidates.count line 25
  4. def OAI.HyperbolicObstruction.BernoulliCandidates.shared line 28
  5. lemma OAI.HyperbolicObstruction.BernoulliCandidates.shared_image line 32
  6. lemma OAI.HyperbolicObstruction.BernoulliCandidates.prob_present line 46
  7. lemma OAI.HyperbolicObstruction.BernoulliCandidates.prob_pair line 60
  8. lemma OAI.HyperbolicObstruction.BernoulliCandidates.expect_count line 89
  9. lemma OAI.HyperbolicObstruction.BernoulliCandidates.variance_count line 112
  10. abbrev OAI.HyperbolicObstruction.BernoulliCandidates.OverlapType line 151

    Source documentation

    A fixed, finite overcount of all nonempty matching types. Types with incompatible coordinate constraints simply have zero realizations.

    abbrev OverlapType (S : Type*) [Fintype S] := {J : Finset S // J.Nonempty} × (S → S)
  11. def OAI.HyperbolicObstruction.BernoulliCandidates.OverlapEvent line 153
  12. instance OAI.HyperbolicObstruction.BernoulliCandidates.(instance at line 156) line 156
  13. lemma OAI.HyperbolicObstruction.BernoulliCandidates.inverse_overlap_le line 160
  14. lemma OAI.HyperbolicObstruction.BernoulliCandidates.overlap_assignment_count line 188

    Source documentation

    Once one admissible second assignment is fixed, every other realization of an overlap type agrees with it on the union of the selected row supports. This is a counting fact, not an independence claim about different coordinate fields.

    lemma overlap_assignment_count (row : (V → A) → S → I) (support : S → Finset V)
    (read : ∀ σ τ s, row σ s = row τ s → ∀ v ∈ support s, σ v = τ v)
    (C : Finset (V → A)) (σ : V → A) (o : OverlapType S) :
    (∑ τ ∈ C, if OverlapEvent row σ τ o then (1 : ℝ) else 0) ≤
      (Fintype.card A : ℝ) ^ (Fintype.card V - (o.1.val.biUnion support).card) := by
…

    Mentions: OAI.HyperbolicObstruction.BernoulliCandidates.OverlapType, OAI.HyperbolicObstruction.BernoulliCandidates.OverlapEvent