OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledSelectedVariation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact stopping prefixes for the fixed residual subset. The variation is that of its literal restricted physical family; subset selection causes no additional factor in any profile or geometric constant.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.selectedPhysicalPrefix line 22
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedPhysicalPrefix_eq_restricted line 27
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.selectedPhysicalPrefix_good_bound line 46

    Source documentation

    The original fixed residual subset has the required clamped prefix bound on its own reference event, for every angular horizon.

    theorem selectedPhysicalPrefix_good_bound (Q : Finset P.PacketIndex)
    (stop : Fin N → ℕ) (hstop : Antitone stop) (y x : ℝ) (H : ℕ) {V : ℝ}
    (hV : (P.restrictPackets Q).physicalMaskedVariation (P.restrictedAlternate alt Q)
      (P.restrictedAlternate_bound alt hAlt Q) t b v g (fun j l u => T j l u.val)
      L A y x ≤ V) :
    finiteCubicVariation (fun k =>
      P.selectedPhysicalPrefix alt hAlt t b v g T L A Q stop (x,y+t*x) (min k H)) (2*H) ≤ V^3 := by
…

    Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedVariation, OAI.LipschitzHilbert.finiteCubicVariation