OAI/Analysis/LipschitzHilbert/Packets/LinePacketFamily.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Actual finite packet data on a reference line, with local coefficient budgets kept explicit. No concentration or synthesis estimate is part of the data.

  1. structure OAI.LipschitzHilbert.LinePacketFamily line 19
  2. def OAI.LipschitzHilbert.LinePacketFamily.length line 49
  3. def OAI.LipschitzHilbert.LinePacketFamily.centerX line 50
  4. def OAI.LipschitzHilbert.LinePacketFamily.centerZ line 52
  5. def OAI.LipschitzHilbert.LinePacketFamily.packets line 54
  6. def OAI.LipschitzHilbert.LinePacketFamily.shortPackets line 56
  7. def OAI.LipschitzHilbert.LinePacketFamily.longPackets line 58
  8. def OAI.LipschitzHilbert.LinePacketFamily.variation line 60
  9. def OAI.LipschitzHilbert.LinePacketFamily.HasLocalBudget line 63
  10. theorem OAI.LipschitzHilbert.LinePacketFamily.length_pos line 68
  11. theorem OAI.LipschitzHilbert.LinePacketFamily.continuous_variation line 71
  12. theorem OAI.LipschitzHilbert.LinePacketFamily.partial_sum_split line 74
  13. theorem OAI.LipschitzHilbert.LinePacketFamily.long_oscillation line 95
  14. theorem OAI.LipschitzHilbert.LinePacketFamily.short_energy line 103