OAI/Analysis/LipschitzHilbert/Trees/SourceCrossAdjointEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cross-profile adjoint energy from four genuine ordinary packet families.

  1. theorem OAI.LipschitzHilbert.four_polarization_norm_sq line 13
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_cross_adjoint_energy line 33