OAI/Analysis/LipschitzHilbert/Packets/PositivePacketSquare.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The positive lattice square estimate and local coefficient energy on one reference line.

  1. def OAI.LipschitzHilbert.LinePacketFamily.envelope line 20
  2. def OAI.LipschitzHilbert.LinePacketFamily.positiveScale line 23
  3. def OAI.LipschitzHilbert.LinePacketFamily.coefficientEnergy line 26
  4. theorem OAI.LipschitzHilbert.LinePacketFamily.envelope_nonneg line 29
  5. theorem OAI.LipschitzHilbert.LinePacketFamily.envelope_integrable line 32
  6. theorem OAI.LipschitzHilbert.LinePacketFamily.envelope_overlap line 36
  7. theorem OAI.LipschitzHilbert.LinePacketFamily.positiveScale_square line 41
  8. theorem OAI.LipschitzHilbert.LinePacketFamily.positiveScale_bound line 52
  9. theorem OAI.LipschitzHilbert.LinePacketFamily.box_coefficient_energy line 60