OAI/Analysis/LipschitzHilbert/Packets/SourceFrozenLongInterval.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The hard angular cutoff in the frozen long-tree expression selects one exact interval of the original scale indices.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.angularStart line 15
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.angularStart_le line 18
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.angularStart_spec line 23
  4. def OAI.LipschitzHilbert.SourceLabeledLattice.frozenLongValue line 36
  5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenLongValue_eq_interval line 45

    Source documentation

    The frozen selector tail, intersected with the long prefix, is a literal interval difference, including the empty-interval case.

    theorem frozenLongValue_eq_interval (t r w s : ℝ) (hw : 0≤w)
    (c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ) (z : ℝ×ℝ) :
    P.frozenLongValue t r w s c z=
      P.physicalLongIntervalSchwartz t r c (P.angularStart w |s-t|) N z := by
…
  6. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenLongValue_norm line 64