OAI/Analysis/LipschitzHilbert/Packets/PacketDataSignedSizeTest.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The signed size tests used in ordinary tree selection. Failing tests have a packet witness and admit the manuscript's near-extremal direction.

  1. def OAI.LipschitzHilbert.PacketLatticeData.sizeDirection line 16
  2. def OAI.LipschitzHilbert.PacketLatticeData.sizeTestPackets line 18
  3. def OAI.LipschitzHilbert.PacketLatticeData.sizeTestEnergy line 26
  4. def OAI.LipschitzHilbert.PacketLatticeData.sizeTestFails line 33
  5. theorem OAI.LipschitzHilbert.PacketLatticeData.sizeTestEnergy_mono line 40
  6. theorem OAI.LipschitzHilbert.PacketLatticeData.sizeTestFails_mono line 49
  7. theorem OAI.LipschitzHilbert.PacketLatticeData.failing_size_test_nonempty line 57
  8. theorem OAI.LipschitzHilbert.PacketLatticeData.size_test_direction_lower line 70
  9. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_near_first_size_test line 82

    Source documentation

    Near-infimum selection is valid even though test directions vary continuously. The finite packet family supplies the lower bound.

    theorem exists_near_first_size_test (negative : Bool) (w cb tau sigma epsilon : ℝ)
    (hw : 0≤w) (hcb : 0≤cb) (hepsilon : 0<epsilon)
    (cell : ∀ j, P.labels j → ℤ) (grid : ℤ)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (R : Finset P.PacketIndex)
    (hex : ∃ T, P.sizeTestFails negative w cb tau sigma cell grid c R T) :
    ∃ T, P.sizeTestFails negative w cb tau sigma cell grid c R T ∧
      ∀ U, P.sizeTestFails negative w cb tau sigma cell grid c R U →
        sizeDirection negative T.slope<sizeDirection negative U.slope+epsilon := by
…

    Mentions: OAI.LipschitzHilbert.PacketLatticeData.sizeDirection