OAI/Algebra/GroupRing/ExpansionDiameter.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.ExpansionDiameter.ball line 12
2. lemma OAI.TorsionFreeZeroDivisors.ExpansionDiameter.mem_ball line 15
3. lemma OAI.TorsionFreeZeroDivisors.ExpansionDiameter.self_mem_ball line 18
4. lemma OAI.TorsionFreeZeroDivisors.ExpansionDiameter.ball_mono line 20
5. def OAI.TorsionFreeZeroDivisors.ExpansionDiameter.neighbors line 24
6. lemma OAI.TorsionFreeZeroDivisors.ExpansionDiameter.neighbors_ball line 27
7. theorem OAI.TorsionFreeZeroDivisors.ExpansionDiameter.ball_large line 43

   Source documentation

   Doubling small sets forces every logarithmic-radius ball above the expansion threshold, uniformly over all connected components.

   theorem ball_large (B R : ℕ)
       (hexp : ∀ S : Finset V, S.Nonempty → S.card ≤ B → 2*S.card  ≤  (neighbors G S).card)
       (hR : B<2^R) (v : V) : B<(ball G v R).card := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.ExpansionDiameter.neighbors, OAI.TorsionFreeZeroDivisors.ExpansionDiameter.ball

8. lemma OAI.TorsionFreeZeroDivisors.ExpansionDiameter.shortest_prefix line 67
9. lemma OAI.TorsionFreeZeroDivisors.ExpansionDiameter.spaced_balls_disjoint line 75
10. theorem OAI.TorsionFreeZeroDivisors.ExpansionDiameter.diameter_bound line 102

    Source documentation

    Quantitative packing: a shortest walk carries disjoint large balls at uniformly spaced centers.

    theorem diameter_bound (B R : ℕ)
        (hexp : ∀ S : Finset V, S.Nonempty → S.card ≤ B → 2*S.card  ≤  (neighbors G S).card)
        (hR : B<2^R) {u v : V} (huv : G.Reachable u v) :
        G.dist u v < (Fintype.card V/(B+1)+1)*(2*R+1) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ExpansionDiameter.neighbors

11. lemma OAI.TorsionFreeZeroDivisors.DiameterProbability.choose_bound line 144
12. lemma OAI.TorsionFreeZeroDivisors.DiameterProbability.witness_envelope line 163

    Source documentation

    A summable envelope with exponent 62, sufficient to obtain an o(1) event.

    lemma witness_envelope (n k r : ℕ) (d p R : ℝ)
        (hk : 0<k) (hn : (k:ℝ) ≤ n) (hd : 1 ≤ d) (hp : 0<p) (hp1 : p ≤ 1) (hR : p*n ≤ R)
        (hr₁ : 64*k ≤ r) (hr₂ : r ≤ 65*k) (hm : ℕ) (hhm : (hm:ℝ) ≤ (2*k*d)^2) :
        (n.choose (2*k):ℝ)*(hm.choose r:ℝ)/R^r ≤
          (9*(12*d^2/p)^65*((k:ℝ)/n)^62)^k := by
    …

13. def OAI.TorsionFreeZeroDivisors.DiameterProbability.witnessTerm line 231
14. lemma OAI.TorsionFreeZeroDivisors.DiameterProbability.witnessTerm_nonneg line 234
15. lemma OAI.TorsionFreeZeroDivisors.DiameterProbability.witnessTerm_majorant line 239
16. lemma OAI.TorsionFreeZeroDivisors.DiameterProbability.witnessTerm_tendsto line 252
17. theorem OAI.TorsionFreeZeroDivisors.DiameterProbability.witness_sum_tendsto line 269

    Source documentation

    The full varying-size union bound tends to zero by dominated convergence.

    theorem witness_sum_tendsto {C ρ : ℝ} (hC : 0 ≤ C)
        (hsmall : C*ρ^62 ≤ 1/2) :
        Tendsto (fun n : ℕ => ∑' k : ℕ, witnessTerm C ρ n k) atTop (𝓝 0) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.DiameterProbability.witnessTerm

18. def OAI.TorsionFreeZeroDivisors.MatchingDiameter.simpleGraph line 290

    Source documentation

    Forgetting multiplicities, with loops contributing only the already present vertex to a closed neighborhood.

    def simpleGraph (r : Matching label bar) : SimpleGraph V where
    …

19. lemma OAI.TorsionFreeZeroDivisors.MatchingDiameter.neighbors_eq line 297
20. def OAI.TorsionFreeZeroDivisors.MatchingDiameter.Expands line 313
21. def OAI.TorsionFreeZeroDivisors.MatchingDiameter.failure line 316
22. theorem OAI.TorsionFreeZeroDivisors.MatchingDiameter.failure_subset_dense line 319
23. lemma OAI.TorsionFreeZeroDivisors.MatchingDiameter.r_bounds line 333
24. theorem OAI.TorsionFreeZeroDivisors.MatchingDiameter.failure_probability_bound line 338

    Source documentation

    A failure of doubling in the actual conditioned port graph is bounded by the summable analytic witness envelope.

    theorem failure_probability_bound (B N d R : ℕ) (p ρ : ℝ)
        (hbar : ∀ t, bar t ≠ t) (hd2 : 2 ≤ d)
        (hd₀ : ∀ v, 129 ≤ Nat.card {e : D // origin e=v})
        (hd : ∀ v, Nat.card {e : D // origin e=v} ≤ d)
        (hB : 2*B ≤ Fintype.card V) (hBρ : (B:ℝ) ≤ ρ*Fintype.card V)
        (hp : 0<p) (hp1 : p ≤ 1) (hρ : ρ ≤ 1)
        (hRreal : p*Fintype.card V ≤ R) (hR0 : 0<R)
        (hR : ∀ x, R+65*B+4*d^(2*N+1) ≤ Nat.card {e : D // label e=label x})
        (hΩ : (Matching.conditioned (label:=label) (bar:=bar) origin N ∅).Nonempty)
    …

25. theorem OAI.TorsionFreeZeroDivisors.MatchingDiameter.diameter_of_not_failure line 400

    Source documentation

    On the complement of the counted event the diameter conclusion follows with an explicit bound, including components of disconnected graphs.

    theorem diameter_of_not_failure (B N R : ℕ) (r : Matching label bar)
        (hr : r∈Matching.conditioned (label:=label) (bar:=bar) origin N ∅)
    …