OAI/Analysis/LipschitzHilbert/Geometry/SourceSizeSelectionEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Disjoint recorded tests and the exact energy bookkeeping for the finite signed size-selection run.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.recordedSizeTests line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recordedSizeTests_subset line 23
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recordedSizeTests_disjoint line 35
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.packetEnergySum line 52
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.recordedSizeTests_energy_le line 56
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.top_area_energy line 88
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.top_area_le line 108

    Source documentation

    Selection charges top area to the actual disjoint coefficient energy.

    theorem top_area_le (h : P.SizeStoppingRun negative w cb tau sigma epsilon A cell grid c
    initial tops remaining) (hsigma : 0<sigma) (hA : 1/2≤A) :
    (tops.map SlopeBox.area).sum≤2/sigma^2*P.packetEnergySum c initial := by
…

    Mentions: OAI.LipschitzHilbert.SlopeBox.area