OAI/Algebra/GroupRing/SeparatorLevels.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.SeparatorLevels.profile line 15

   Source documentation

   Canonical finite vertex level profile; its mass is not an extra assumption.

   def profile (level : V → ℤ) (z : ℤ) : ℕ :=
   …

2. theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.profile_mass line 18
3. theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.select_vertices line 25
4. theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.exists_median line 32

   Source documentation

   A median genuine BFS level, including the empty graph and repeated levels.

   theorem exists_median (level : V → ℕ) :
       ∃ center : ℕ,
         2*(Finset.univ.filter (fun v=>level v<center)).card ≤ Fintype.card V ∧
         2*(Finset.univ.filter (fun v=>center<level v)).card ≤ Fintype.card V := by
   …

5. theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.selected_levels line 68

   Source documentation

   The selected levels are literal finite graph levels, and both exterior regions already satisfy the stronger half-size bound.

   theorem selected_levels (level : V → ℕ) :
       ∃ center kL kR : ℕ,
         (profile (fun v=>(level v:ℤ)) ((center:ℤ)-kL) +
          profile (fun v=>(level v:ℤ)) ((center:ℤ)+kR) + 2*(kL+kR) : ℝ) ≤
           2*Real.sqrt 2*Real.sqrt (Fintype.card V) ∧
         2*(Finset.univ.filter (fun v=>(level v:ℤ)<(center:ℤ)-kL)).card ≤ Fintype.card V ∧
         2*(Finset.univ.filter (fun v=>(center:ℤ)+kR<(level v:ℤ))).card ≤ Fintype.card V := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.SeparatorLevels.profile

6. theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.below_closed line 96

   Source documentation

   A single removed level prevents an edge from passing across it.

   theorem below_closed {R : V → V → Prop} (level : V → ℤ)
       (hstep : ∀ x y,R x y → level y ≤ level x+1) {b : ℤ} {x y : V}
       (hx : level x<b) (hy : level y≠b) (hxy : R x y) : level y<b := by
   …

7. theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.above_closed line 103
8. theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.band_closed line 110
9. theorem OAI.TorsionFreeZeroDivisors.SeparatorLevels.bfs_step line 122
10. def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.of_fibers line 138
11. theorem OAI.TorsionFreeZeroDivisors.PlanarMap.Model.connected_split line 180
12. def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.map line 310