OAI/Algebra/GroupRing/ClusterLocalization.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.ClusterLocalization.pathEquiv line 17
2. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.paths_card line 32
3. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.member_exists line 34
4. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.paths_card_le line 41

   Source documentation

   A closed retained subset supplied by recursive separation bounds the actual connected component, even when the pairing has loops or parallel arcs.

   lemma paths_card_le {K : ℕ}
       (hs : ∀ t,keep t → ∃ B : Finset T,t∈B ∧ B.card≤K ∧
         ∀ x∈B,∀ y,keep y → PairingClusters.Rel (fun x : Position len=>x.1) C.pairing.partner x y → y∈B)
       (c : Cluster C keep) : (paths C keep c).card≤K := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.PairingClusters.Rel, OAI.TorsionFreeZeroDivisors.ClusterLocalization.Cluster, OAI.TorsionFreeZeroDivisors.ClusterLocalization.paths

5. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.mass_upper line 57
6. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.mass_lower line 64
7. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.short_mass_refined line 69
8. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.short_mass_half line 95
9. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.retained_original line 124

   Source documentation

   Retained closures are nonnegative; only deleted original positions are charged in the lower bound for retained mass.

   lemma retained_original (old : T → ℕ) (ho : ∀ t,old t≤len t) :
       (∑t,old t)≤(∑c,mass C keep c)+∑t∈Finset.univ.filter (fun t=>¬keep t),old t := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.ClusterLocalization.mass

10. theorem OAI.TorsionFreeZeroDivisors.ClusterLocalization.exists_selected line 134

    Source documentation

    An averaging argument on the actual connected components of the retained pairing graph. E counts oriented interval sides, hence its factor 2.

    theorem exists_selected (old : T → ℕ) (ho : ∀ t,old t≤len t)
        (root : Option T) (L K cap : ℕ) (H₀ ε C₂ : ℝ)
        (hH₀ : 0<H₀) (hL : 0<L) (hε : 0<ε) (hC₂ : 0<C₂)
        (hsize : ∀ c : Cluster C keep,(paths C keep c).card≤K)
        (hcap : ∀ t,len t≤cap*L)
        (hbase : H₀≤∑t,(old t:ℝ))
        (hdelete : (∑t∈Finset.univ.filter (fun t=>¬keep t),(old t:ℝ))≤H₀/16)
        (hbad : ((Finset.univ.filter (fun x : Position len=>C.pairing.partner x=x)).card:ℝ)+
          ((Finset.univ.filter (fun x : Position len=>¬keep x.1 ∧ C.pairing.partner x≠x)).card:ℝ)≤ε/16*H₀)
        (hcompare : (Fintype.card E:ℝ)/2≤C₂/(16*L)*H₀)
        (hlong : ∀ t,root≠some t → L≤len t)
        (hroot : ∀ t,root=some t → len t<L → (len t:ℝ)≤H₀/2) :
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ClusterLocalization.Cluster, OAI.TorsionFreeZeroDivisors.ClusterLocalization.paths

11. def OAI.TorsionFreeZeroDivisors.RestrictComparisons.rootPath line 185
12. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.rootPath_some line 186
13. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.rootPath_cyclic line 194
14. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.rootPath_map line 196
15. structure OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem line 211

    Source documentation

    Literal path/comparison data before the separator and averaging step. Unlike BoundedSystem it makes no quantitative smallness or pairing assumption.

    structure PathSystem (rep : ℕ) (r : Match rep) (x : VA rep) (y : VB rep) where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.SampleGraph.VA, OAI.TorsionFreeZeroDivisors.SampleGraph.VB

16. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.dart_embed line 242
17. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.restrict line 246
18. def OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.bounded line 283

    Source documentation

    Bounding a literal system adds no realizability or word constraints.

    def bounded {Bnd K I : ℕ}
        (hP : Fintype.card s.P≤K) (hE : Fintype.card s.E≤I)
        (hlo : L (size rep)≤∑p,(s.paths p).length)
        (hhi : (∑p,(s.paths p).length)≤Bnd*L (size rep))
        (hbad : ((Finset.univ.filter (fun p=>s.comparisons.pairing.partner p=p)).card:ℝ)≤
          StageFusion.epsilon (1/600) 256*(∑p,(s.paths p).length:ℕ)) : BoundedSystem Bnd K I rep r x y where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageFusion.epsilon, OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem

19. def OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.selected_bounded line 323

    Source documentation

    Realizes the selected component by exactly its literal retained paths and interval sides, with the same signs, noncoincident lifts, and prescribed root.

    def selected_bounded {Bnd K I : ℕ} (c : Cluster s.comparisons keep)
        (hP : (ClusterLocalization.paths s.comparisons keep c).card≤K)
        (hE : ClusterLocalization.comparisons s.comparisons keep c≤I)
        (hlo : L (size rep) ≤ mass s.comparisons keep c)
        (hhi : mass s.comparisons keep c≤Bnd*L (size rep))
        (hbad : (bad s.comparisons keep c:ℝ)≤
          StageFusion.epsilon (1/600) 256*mass s.comparisons keep c) :
        BoundedSystem Bnd K I rep r x y := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ClusterLocalization.paths, OAI.TorsionFreeZeroDivisors.ClusterLocalization.comparisons, OAI.TorsionFreeZeroDivisors.StageFusion.epsilon, OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem

20. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.excluded_of_local_totals line 369

    Source documentation

    The analytic union bound excludes the localized system using the sharp mass and interval estimates.

    theorem excluded_of_local_totals (K cap : ℕ) (C₂ H₀ : ℝ) (old : s.P → ℕ)
        (ho : ∀ t,old t≤(s.paths t).length)
        (hH₀ : 0<H₀) (hL : 0<L (size rep)) (hC₂ : 0<C₂)
        (hsize : ∀ c : Cluster s.comparisons keep,(ClusterLocalization.paths s.comparisons keep c).card≤K)
        (hcap : ∀ t,(s.paths t).length≤cap*L (size rep))
        (hbase : H₀≤∑t,(old t:ℝ))
        (hdelete : (∑t∈Finset.univ.filter (fun t=>¬keep t),(old t:ℝ))≤H₀/16)
        (hbad : ((Finset.univ.filter (fun p=>s.comparisons.pairing.partner p=p)).card:ℝ)+
          ((Finset.univ.filter (fun p=>¬keep p.1 ∧ s.comparisons.pairing.partner p≠p)).card:ℝ)≤
            StageFusion.epsilon (1/600) 256/16*H₀)
        (hcompare : (Fintype.card s.E:ℝ)/2≤C₂/(16*L (size rep))*H₀)
        (hlong : ∀ t,s.root≠some t → L (size rep)≤(s.paths t).length)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ClusterLocalization.paths, OAI.TorsionFreeZeroDivisors.StageFusion.epsilon