OAI/Analysis/LipschitzHilbert/Trees/SourceSelectedDuality.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual analyzing coefficients and L2 duality for a selected packet set. Only the synthesis estimate for those same coefficients is needed.

  1. theorem OAI.LipschitzHilbert.l2_self_pairing_energy_le line 13
  2. theorem OAI.LipschitzHilbert.finite_analyzing_self_pairing line 35
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.ordinaryCoefficient line 69

    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 ℂ κ :=
…
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selected_ordinary_coefficient_energy line 74