OAI/Analysis/LipschitzHilbert/Estimates/SegmentWeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Weight variation on a later segment, paid for by full-root mass loss.

  1. def OAI.LipschitzHilbert.segmentLog line 13
  2. def OAI.LipschitzHilbert.segmentWeight line 16
  3. def OAI.LipschitzHilbert.boundaryLog line 19
  4. theorem OAI.LipschitzHilbert.boundaryLog_nonnegative line 21
  5. theorem OAI.LipschitzHilbert.boundaryLog_le_root_ratio line 25
  6. theorem OAI.LipschitzHilbert.segmentLog_re_le line 30
  7. theorem OAI.LipschitzHilbert.segmentLog_increment line 42
  8. theorem OAI.LipschitzHilbert.segmentLog_variation line 50
  9. theorem OAI.LipschitzHilbert.segmentWeight_variation line 84
  10. theorem OAI.LipschitzHilbert.boundary_weight_variation line 121