OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalReferenceSquare.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The physical positive main square is exactly the normalized reference square function times its coefficient normalization. This connects the symmetric frozen main term to three proved line estimates.

  1. def OAI.LipschitzHilbert.SourceLatticePacket.physicalReferenceLine line 17
  2. def OAI.LipschitzHilbert.SourceLatticePacket.physicalReferenceSquare line 25
  3. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalPositiveScale_eq_reference line 33
  4. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalPositiveScale_square_sum_eq line 43
  5. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredPositiveScale_square_reference line 54