OAI/Analysis/LipschitzHilbert/Estimates/StripSubdivision.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact binary subdivision of the reference strips. Shared boundary fibers have zero planar measure, so closed strip masses add exactly.

  1. theorem OAI.LipschitzHilbert.Rectangle.stripSlab_children line 13
  2. theorem OAI.LipschitzHilbert.Rectangle.volume_coordinate_fiber line 25
  3. theorem OAI.LipschitzHilbert.Rectangle.stripSlab_children_null_inter line 32
  4. theorem OAI.LipschitzHilbert.Rectangle.intersection_stripSlab_children line 45
  5. def OAI.LipschitzHilbert.stripMass line 65
  6. theorem OAI.LipschitzHilbert.stripMass_children line 68