OAI/Analysis/LipschitzHilbert/Packets/PacketDataSelectedDuality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.PacketLatticeData.ordinaryCoefficient line 18

   Source documentation

   Coefficients of the original physical packets, before selector masks.

   def ordinaryCoefficient (g : ℝ×ℝ → EuclideanSpace ℂ κ)
       (j : Fin N) (l : P.labels j) (u : Item j l) : EuclideanSpace ℂ κ :=
   …

2. theorem OAI.LipschitzHilbert.PacketLatticeData.selected_ordinary_coefficient_energy line 23