OAI/Analysis/LipschitzHilbert/Trees/SourceOrdinarySizeTest.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.SourceLabeledLattice.sizeDirection line 18
  2. def OAI.LipschitzHilbert.SourceLabeledLattice.sizeTestPackets line 20
  3. def OAI.LipschitzHilbert.SourceLabeledLattice.sizeTestEnergy line 28
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.sizeTestFails line 35
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sizeTestEnergy_mono line 42
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.sizeTestFails_mono line 51
  7. theorem OAI.LipschitzHilbert.SourceLabeledLattice.failing_size_test_nonempty line 59
  8. theorem OAI.LipschitzHilbert.SourceLabeledLattice.size_test_direction_lower line 72
  9. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_near_first_size_test line 84

    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.SourceLabeledLattice.sizeDirection