OAI/Geometry/HyperbolicGroups/Coincidence.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.Coincidence.signedAssignment line 20

   Source documentation

   Signs remain separate at every position, even inside one unsigned class.

   def signedAssignment {k n : ℕ} (c : V → Fin k) (ε : V → Bool) (a : Fin k → Fin (n+1)) :
       V → IncidenceTemplate.SymmetricAlphabet n := fun v => (a (c v), ε v)

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet

2. def OAI.HyperbolicObstruction.Coincidence.unsignedValues line 23
3. def OAI.HyperbolicObstruction.Coincidence.unsignedRank line 26
4. lemma OAI.HyperbolicObstruction.Coincidence.unsignedValues_card_le line 30
5. lemma OAI.HyperbolicObstruction.Coincidence.signed_factorization line 34
6. theorem OAI.HyperbolicObstruction.Coincidence.signed_pattern_bound line 48

   Source documentation

   A specified unsigned coincidence pattern is rare exactly when its number of classes is smaller than the total independent trial cost. Distinctness is explicit, so repeated occurrences are not incorrectly charged twice.

   theorem signed_pattern_bound {k n : ℕ} (c : V → Fin k) (ε : V → Bool)
       (row : (V → IncidenceTemplate.SymmetricAlphabet n) → S → I)
       (p : I → ℝ) (hp : ∀ i, p i ∈ Set.Icc (0:ℝ) 1)
       (q : S → ℝ) (hq : ∀ σ s, p (row σ s) = q s) :
       (FiniteLaw.bernoulliProduct p hp).prob (fun w => ∃ a : Fin k → Fin (n+1),
         Function.Injective (row (signedAssignment c ε a)) ∧
         BernoulliCandidates.Present row w (signedAssignment c ε a)) ≤
         (n+1:ℝ)^k * ∏ s, q s := by
   …

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.Coincidence.signedAssignment, OAI.HyperbolicObstruction.BernoulliCandidates.Present

7. lemma OAI.HyperbolicObstruction.Coincidence.patterns_bound line 78
8. def OAI.HyperbolicObstruction.Coincidence.rankRate line 97
9. lemma OAI.HyperbolicObstruction.Coincidence.rankRate_nonneg line 101
10. lemma OAI.HyperbolicObstruction.Coincidence.rankRate_tendsto line 108
11. def OAI.HyperbolicObstruction.Coincidence.RankBad line 121

    Source documentation

    Concrete bad event: an included collection of distinct trials has more unsigned coincidences than its information budget permits.

    def RankBad {n : ℕ} (row : (V → IncidenceTemplate.SymmetricAlphabet n) → S → I)
        (cost : ℝ) (w : I → Bool) : Prop :=
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet

12. instance OAI.HyperbolicObstruction.Coincidence.(instance at line 126) line 126
13. lemma OAI.HyperbolicObstruction.Coincidence.rank_bad_classes line 130
14. theorem OAI.HyperbolicObstruction.Coincidence.rank_bad_bound line 148

    Source documentation

    The finite first-moment coincidence estimate, including every sign choice and every unsigned partition.

    theorem rank_bad_bound {n : ℕ}
        (row : (V → IncidenceTemplate.SymmetricAlphabet n) → S → I)
        (p : I → ℝ) (hp : ∀ i, p i ∈ Set.Icc (0:ℝ) 1)
        (cost : S → ℝ) (hq : ∀ σ s,
          p (row σ s) = (Fintype.card (IncidenceTemplate.SymmetricAlphabet n):ℝ)^(cost s)) :
        (FiniteLaw.bernoulliProduct p hp).prob (RankBad row (∑ s, cost s)) ≤
          rankRate (Fintype.card V) (∑ s, cost s)
            (Fintype.card (IncidenceTemplate.SymmetricAlphabet n)) := by
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.Coincidence.RankBad, OAI.HyperbolicObstruction.Coincidence.rankRate