OAI/Algebra/GroupRing/FiniteClusters.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic localization of finite-cluster mass and comparison bounds.

  1. def OAI.TorsionFreeZeroDivisors.FiniteClusters.block line 13
  2. lemma OAI.TorsionFreeZeroDivisors.FiniteClusters.mem_block line 15
  3. lemma OAI.TorsionFreeZeroDivisors.FiniteClusters.block_nonempty line 17
  4. lemma OAI.TorsionFreeZeroDivisors.FiniteClusters.same_of_adj line 20
  5. lemma OAI.TorsionFreeZeroDivisors.FiniteClusters.reachable_closed line 24
  6. lemma OAI.TorsionFreeZeroDivisors.FiniteClusters.block_card line 32
  7. lemma OAI.TorsionFreeZeroDivisors.FiniteClusters.sum_blocks line 43
  8. lemma OAI.TorsionFreeZeroDivisors.FiniteClusters.block_sum_le line 51
  9. abbrev OAI.TorsionFreeZeroDivisors.PairingClusters.Vertex line 62
  10. def OAI.TorsionFreeZeroDivisors.PairingClusters.Rel line 63
  11. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.rel_symm line 66
  12. def OAI.TorsionFreeZeroDivisors.PairingClusters.graph line 69
  13. abbrev OAI.TorsionFreeZeroDivisors.PairingClusters.Cluster line 76
  14. def OAI.TorsionFreeZeroDivisors.PairingClusters.cluster line 78
  15. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.cluster_some line 81
  16. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.cluster_none line 84
  17. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.cluster_exists line 86
  18. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.cluster_pair line 91
  19. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.same_cluster_partner line 100
  20. def OAI.TorsionFreeZeroDivisors.PairingClusters.bad line 108
  21. def OAI.TorsionFreeZeroDivisors.PairingClusters.localBad line 109
  22. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.localBad_iff line 113
  23. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.local_bad_sum line 122
  24. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.total_bad_bound line 137
  25. lemma OAI.TorsionFreeZeroDivisors.PairingClusters.total_local_bad_bound line 160
  26. lemma OAI.TorsionFreeZeroDivisors.PlanarLocalization.bad_mass line 172
  27. theorem OAI.TorsionFreeZeroDivisors.PlanarLocalization.exists_good_cluster line 183

    Source documentation

    Three exact exclusions leave a positive amount of source length.

    theorem exists_good_cluster {Z : Type} [Fintype Z]
    (h b i : Z → ℝ) (H₀ L ε C C₂ : ℝ)
    (hH₀ : 0 < H₀) (hL : 0 < L) (hε : 0 < ε) (hC₂ : 0 < C₂)
    (hh : ∀ z,0 ≤ h z) (hb : ∀ z,0 ≤ b z) (hi : ∀ z,0 ≤ i z)
    (hupper : ∀ z,h z ≤ C*L)
    (hretained : 15/16*H₀ ≤ ∑ z,h z)
    (hunpaired : ∑ z,b z ≤ ε/16*H₀)
    (hcomparisons : ∑ z,i z ≤ C₂/(16*L)*H₀)
    (hshort : ∑ z∈Finset.univ.filter (fun z => h z < L),h z ≤ H₀/2) :
    ∃ z,L ≤ h z ∧ h z ≤ C*L ∧ b z ≤ ε*h z ∧ i z ≤ C₂*h z/L := by
…
  28. lemma OAI.TorsionFreeZeroDivisors.PlanarLocalization.exceptional_short_cost line 246

    Source documentation

    The discarded short exceptional cluster really costs less than half; the ordinary girth-length boundary is accounted for separately, not silently lost.

    lemma exceptional_short_cost (h L H₀ : ℝ) (hlen : h < L) (hordinary : h+L ≤ H₀) :
    h < H₀/2 := by linarith
…
  29. abbrev OAI.TorsionFreeZeroDivisors.ClusterLocalization.graph line 257
  30. abbrev OAI.TorsionFreeZeroDivisors.ClusterLocalization.Cluster line 259
  31. def OAI.TorsionFreeZeroDivisors.ClusterLocalization.cluster line 261
  32. abbrev OAI.TorsionFreeZeroDivisors.ClusterLocalization.belongs line 263
  33. abbrev OAI.TorsionFreeZeroDivisors.ClusterLocalization.localC line 264
  34. def OAI.TorsionFreeZeroDivisors.ClusterLocalization.mass line 265
  35. def OAI.TorsionFreeZeroDivisors.ClusterLocalization.bad line 266
  36. def OAI.TorsionFreeZeroDivisors.ClusterLocalization.comparisons line 269
  37. def OAI.TorsionFreeZeroDivisors.ClusterLocalization.paths line 271
  38. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.cluster_exists line 274
  39. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.mass_pos line 276
  40. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.mass_sum line 284
  41. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.mass_original_loss line 296
  42. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.bad_sum line 300
  43. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.comparisons_sum line 310
  44. def OAI.TorsionFreeZeroDivisors.ClusterLocalization.fixedEquiv line 334

    Source documentation

    The fixed positions in the literal restricted comparison system are exactly this cluster's old fixed or lost-partner occurrences.

    def fixedEquiv (c : Cluster C keep) :
    {x : Position (RestrictComparisons.Length (belongs C keep c) (len:=len)) //
…

    Mentions: OAI.TorsionFreeZeroDivisors.ClusterLocalization.Cluster, OAI.TorsionFreeZeroDivisors.RestrictComparisons.Length, OAI.TorsionFreeZeroDivisors.ClusterLocalization.belongs

  45. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.fixed_card line 349
  46. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.local_mass line 353
  47. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.short_member line 357
  48. lemma OAI.TorsionFreeZeroDivisors.ClusterLocalization.short_mass line 364

    Source documentation

    With at most one short exceptional piece there is at most one short cluster. The estimate counts actual retained path lengths, not abstract cluster masses.

    lemma short_mass {L : ℕ} (root : Option T)
    (ho : ∀ t,root≠some t → L≤len t) :
    (∑ c∈Finset.univ.filter (fun c=>mass C keep c<L),mass C keep c)≤
      ∑ t∈Finset.univ.filter (fun t=>root=some t),len t := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ClusterLocalization.mass