OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationActive.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Only frozen-active labels enter the centered main term. Their actual angular separation bounds the modulation parameter, independently of the wide cone used for the positive angular error.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenActive_carrier_bound line 20
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.activeMainFamily line 35

    Source documentation

    Changing a bound field changes no packet; the centered family uses the narrow modulation bound supplied by active labels.

    def activeMainFamily (w F Cb : ℝ) (hw : 0 < w) (hF : 0 ≤ F) (hCb : 0 ≤ Cb)
    (hfreq : ∀ k, |P.frequency k| ≤ F/w)
    (hangle : ∀ j l, (∃ k, b j l k t ≠ 0) → |P.rowSlope j l| ≤ Cb*w/P.length j) :
    SourceLabeledLattice N κ Label Item :=
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice

  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.activeMainFamily_constant line 49
  4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.activeMainFamily_topGeometry line 53
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.activeMainFamily_rawInterval line 62