OAI/Analysis/LipschitzHilbert/Trees/SourcePolarizedInterval.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact cross-profile source intervals and their four self-family representation. Every coefficient is the original selected integral.

  1. theorem OAI.LipschitzHilbert.SourceLatticePacket.family_mainCoefficient_physical_zero line 20
  2. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_mainCoefficient line 28
  3. def OAI.LipschitzHilbert.SourceLatticePacket.rawInterval line 41
  4. theorem OAI.LipschitzHilbert.SourceLatticePacket.rawInterval_scaled_covariant line 45
  5. theorem OAI.LipschitzHilbert.SourceLatticePacket.polarize_rawInterval line 60
  6. theorem OAI.LipschitzHilbert.SourceLatticePacket.cross_rawInterval_polarization line 78
  7. theorem OAI.LipschitzHilbert.SourceLatticePacket.cross_covariant_polarization line 96
  8. theorem OAI.LipschitzHilbert.SourceLatticePacket.cross_interval_joint_bound line 132