OAI/Analysis/LipschitzHilbert/Packets/PacketDataSelectedGram.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact far-Gram grouping over the actual selected records, followed by the global near/far energy assembly.

  1. def OAI.LipschitzHilbert.PacketLatticeData.farPairing line 19
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.farPairing_eq_gram line 24
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.selected_far_gram_sum line 36
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.selected_gram_energy line 60

    Source documentation

    The exact near/far assembly for a selected set. Its two estimates follow from local multiplicity and the per-record far theorem.

    theorem selected_gram_energy
    (negative : Bool) (w cb A : ℝ) (hA : 1/2≤A)
    (cell : ∀ j, P.labels j → ℤ) (grid : ℤ)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (initial : Finset P.PacketIndex) (tops : List SlopeBox) (gap : ℕ)
    (Cnear Cfar : ℝ)
    (hnear : let S := P.selectedPackets negative w cb A cell grid initial tops
…

    Mentions: OAI.LipschitzHilbert.SlopeBox