OAI/Geometry/HyperbolicGroups/RelativePartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.RelativePartBoundary line 20

   Source documentation

   One side of a selected INTERIOR fragment. The complement includes the protected outside, even when its arbitrary partition label agrees.

   abbrev RelativePartBoundary (i : I) :=
   …

2. instance OAI.HyperbolicObstruction.PictureSwitch.(instance at line 22) line 22
3. abbrev OAI.HyperbolicObstruction.PictureSwitch.OutsideContact line 24
4. instance OAI.HyperbolicObstruction.PictureSwitch.(instance at line 25) line 25
5. abbrev OAI.HyperbolicObstruction.PictureSwitch.RelativeCutContact line 27
6. instance OAI.HyperbolicObstruction.PictureSwitch.(instance at line 29) line 29
7. theorem OAI.HyperbolicObstruction.PictureSwitch.sum_relative_part_boundary line 34

   Source documentation

   Exact relative boundary accounting, retaining loops and parallel contacts: outside contacts occur once, contacts cut between interior parts twice.

   theorem sum_relative_part_boundary :
       (∑ i, Fintype.card (RelativePartBoundary P active part i)) =
         Fintype.card (OutsideContact P active) +
           2 * Fintype.card (RelativeCutContact P active part) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.RelativePartBoundary, OAI.HyperbolicObstruction.PictureSwitch.OutsideContact, OAI.HyperbolicObstruction.PictureSwitch.RelativeCutContact

8. theorem OAI.HyperbolicObstruction.PictureSwitch.outside_contacts_le_length line 85

   Source documentation

   Contacts from the interior to an enumerated outside are bounded by its literal length. Outside-to-outside free boundary folds are NOT counted.

   theorem outside_contacts_le_length (xs : List X)
       (ha : ∀ x, active x ↔ x ∉ xs) :
       Fintype.card (OutsideContact P active) ≤ xs.length := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.OutsideContact

9. theorem OAI.HyperbolicObstruction.PictureSwitch.sum_relative_boundary_le line 105

   Source documentation

   Source03's summation bound on a disk, before any separator existence or small-fragment estimate is used. This is a literal finite-side identity.

   theorem sum_relative_boundary_le (xs : List X)
       (ha : ∀ x, active x ↔ x ∉ xs) :
       (∑ i, Fintype.card (RelativePartBoundary P active part i)) ≤
         xs.length + 2 * Fintype.card (RelativeCutContact P active part) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.RelativePartBoundary, OAI.HyperbolicObstruction.PictureSwitch.RelativeCutContact