OAI/Algebra/GroupRing/TypedDiameter.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.TypedDiameter.p₀ line 15

   Source documentation

   A conservative effective prescription coefficient, for the diameter union bound only. The empirical letter density remains 129/16513.

   def p₀ : ℝ := 129/(4*16513)

2. def OAI.TorsionFreeZeroDivisors.TypedDiameter.C₀ line 16
3. def OAI.TorsionFreeZeroDivisors.TypedDiameter.ρ line 17
4. def OAI.TorsionFreeZeroDivisors.TypedDiameter.B line 18
5. def OAI.TorsionFreeZeroDivisors.TypedDiameter.R line 19
6. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.p₀_pos line 21
7. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.p₀_le_one line 22
8. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.C₀_pos line 23
9. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.ρ_pos line 25
10. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.ρ_le_quarter line 30
11. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.ρ_le_one line 31
12. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.ρ_small line 32
13. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.B_le line 42
14. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.twice_B_le line 44
15. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.sixtyfive_B_le line 50
16. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.R_eq line 56
17. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.carrier_eq line 61
18. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.eventual_denom line 66
19. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.witness_summable line 79
20. abbrev OAI.TorsionFreeZeroDivisors.TypedDiameter.ΩA line 86

    Source documentation

    The exact empirical A-side conditioned sample space.

    abbrev ΩA (rep : ℕ) := Matching.conditioned
    …

21. abbrev OAI.TorsionFreeZeroDivisors.TypedDiameter.ΩB line 89
22. def OAI.TorsionFreeZeroDivisors.TypedDiameter.badA line 93
23. def OAI.TorsionFreeZeroDivisors.TypedDiameter.badB line 96
24. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.typed_bound line 102

    Source documentation

    Instantiation retains the actual vertex types, degree range, letter carriers and prescribed girth conditioning.

    theorem typed_bound {V : Type*} [Fintype V] (outgoing : V → Finset Letter)
        (rep : ℕ) (hrep : 0<rep) (hc : Fintype.card V=size rep)
        (hd : ∀ v, 129 ≤ (outgoing v).card ∧ (outgoing v).card ≤ 132)
        (hl : ∀ t, Fintype.card {v : V // t∈outgoing v}=4260354*rep)
        (hden : R rep+65*B (size rep)+4*132^(2*(3*L (size rep))+1) ≤ 4260354*rep)
        (hΩ : (Matching.conditioned (label:=TypedGraphs.label outgoing) (bar:=inverse)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.TypedDiameter.R, OAI.TorsionFreeZeroDivisors.TypedDiameter.B, OAI.TorsionFreeZeroDivisors.TypedGraphs.label

25. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.eventual_bound line 129
26. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.failureA_tendsto line 136
27. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.failureB_tendsto line 142
28. def OAI.TorsionFreeZeroDivisors.TypedDiameter.A₀ line 149

    Source documentation

    The deterministic constant in the manifestation of the diameter lemma.

    def A₀ : ℕ := ⌈1/ρ⌉₊

    Mentions: OAI.TorsionFreeZeroDivisors.TypedDiameter.ρ

29. def OAI.TorsionFreeZeroDivisors.TypedDiameter.D₀ line 150
30. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.packing_bound line 152
31. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.log_radius_bound line 164
32. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.component_diameter line 182

    Source documentation

    This is the precise fixed-constant O(L) conclusion on the expansion complement, with no degree or matching independence assumption.

    theorem component_diameter {V D T : Type*} [Fintype V] [Fintype D]
        (origin : D → V) {label : D → T} {bar : T → T} (n N : ℕ)
        (hc : Fintype.card V=n) (hL : 1 ≤ L n) (r : Matching label bar)
        (hr : r∈Matching.conditioned (label:=label) (bar:=bar) origin N ∅)
    …

33. def OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterBadA line 203

    Source documentation

    The A-side actual diameter-failure event, still conditioned on girth.

    def diameterBadA (rep : ℕ) := (ΩA rep).filter fun r =>
    …

    Mentions: OAI.TorsionFreeZeroDivisors.TypedDiameter.ΩA

34. def OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterBadB line 206
35. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterBadA_subset line 210
36. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterBadB_subset line 217
37. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterA_tendsto line 225

    Source documentation

    Diameter bound for the literal A empirical type table.

    theorem diameterA_tendsto :
        Tendsto (fun rep : ℕ => (diameterBadA rep).card/((ΩA rep).card:ℝ)) atTop (𝓝 0) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterBadA, OAI.TorsionFreeZeroDivisors.TypedDiameter.ΩA

38. theorem OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterB_tendsto line 233

    Source documentation

    Diameter bound for the literal B empirical type table.

    theorem diameterB_tendsto :
        Tendsto (fun rep : ℕ => (diameterBadB rep).card/((ΩB rep).card:ℝ)) atTop (𝓝 0) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.TypedDiameter.diameterBadB, OAI.TorsionFreeZeroDivisors.TypedDiameter.ΩB

39. lemma OAI.TorsionFreeZeroDivisors.FiniteJointAvoidance.exists_outside line 243
40. lemma OAI.TorsionFreeZeroDivisors.MatchingAlias.conditioned_eq line 277
41. lemma OAI.TorsionFreeZeroDivisors.GraphSample.samples_eq line 291
42. def OAI.TorsionFreeZeroDivisors.GraphSample.Diameters line 301

    Source documentation

    Both exact component diameter conclusions, including disconnected graphs.

    def Diameters (rep : ℕ) (r : Match rep) : Prop :=
    …

43. lemma OAI.TorsionFreeZeroDivisors.GraphSample.diameters_of_not_bad line 307
44. theorem OAI.TorsionFreeZeroDivisors.GraphSample.bounded_with_diameter line 323

    Source documentation

    The diameter event and the entire bounded-pattern avoidance event occur simultaneously in the literal conditional product sample.

    theorem bounded_with_diameter (R K T I B Q M J : ℕ)
        (hR : 0<R) (hK : 0<K) (hI : 0<I) (hM : 0<M) :
        ∀ᶠ rep in atTop,∀ (x : Types.VertexA rep) (y : Types.VertexB rep),
          ∃ r∈samples rep,Diameters rep r ∧ ∀ a : BoundedPattern.Data R K T I (B*L (size rep)),
            a.Good B Q M J rep → ¬a.event rep x y r := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB, OAI.TorsionFreeZeroDivisors.GraphSample.Diameters, OAI.TorsionFreeZeroDivisors.BoundedPattern.Data

45. theorem OAI.TorsionFreeZeroDivisors.GraphSample.raw_with_diameter line 360

    Source documentation

    Source entropy proposition for arbitrary literal immersed path systems, with the independent short-closure diameter event included.

    theorem raw_with_diameter (B K I : ℕ) (hK : 0<K) (hI : 0<I) :
        ∀ᶠ rep in atTop,∀ (x : Types.VertexA rep) (y : Types.VertexB rep),
          ∃ r∈samples rep,Diameters rep r ∧ ∀ a : RawSourcePattern.Data B K I rep,¬a.event x y r := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.Types.VertexA, OAI.TorsionFreeZeroDivisors.Types.VertexB, OAI.TorsionFreeZeroDivisors.GraphSample.Diameters, OAI.TorsionFreeZeroDivisors.RawSourcePattern.Data