SourceParentReferenceEvents.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Reference events at the path-top slope keep the original packets and selectors. The angular mesh is w/topLength, independently of the exponent used in the path weights. One parent event and all continuing-shift events form a single finite, phase-independent union.

abbrev OAI.LipschitzHilbert.SourceLabeledLattice.recenteredReferenceData line 28
Source documentation
Literal recentering of original physical reference data.
```
abbrev recenteredReferenceData : PhysicalReferenceData N κ Label Item where
…
```
Mentions: OAI.LipschitzHilbert.PhysicalReferenceData
def OAI.LipschitzHilbert.SourceLabeledLattice.recenteredReferenceSelection line 40
Source documentation
Original packet indices are selected through the exact reference-label map.
```
def recenteredReferenceSelection (S : Finset P.PacketIndex) :
    Finset (P.referenceFamily oldSlope newSlope R cone w F hw hcone hF hwide hfrequency).PacketIndex :=
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.PacketIndex
theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenteredReferenceData_slope line 45
theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenteredReferenceData_angle line 49
theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenteredReferenceData_short line 53
theorem OAI.LipschitzHilbert.SourceLabeledLattice.recenteredReferenceData_bad line 60

def OAI.LipschitzHilbert.parentShiftReferenceData line 81

Source documentation

none denotes the parent square; some shift denotes its continuing path.

def parentShiftReferenceData
    (parent : ι → PhysicalReferenceData N κ Label Item)
    (child : ι → Fin K → PhysicalReferenceData N κ Label Item)
    (t : ι) : Option (Fin K) → PhysicalReferenceData N κ Label Item
  | none => parent t
  | some shift => child t shift

Mentions: OAI.LipschitzHilbert.PhysicalReferenceData

def OAI.LipschitzHilbert.parentShiftReferenceSelection line 88

def OAI.LipschitzHilbert.parentShiftReferenceBad line 98

Source documentation

The common union is literal, with no dependence on an imaginary phase.

def parentShiftReferenceBad
    (parent : ι → PhysicalReferenceData N κ Label Item)
    (child : ι → Fin K → PhysicalReferenceData N κ Label Item)
    (parentSelected : ∀ t, Finset (parent t).family.PacketIndex)
    (childSelected : ∀ t i, Finset (child t i).family.PacketIndex)
    (L A e s r : ℝ) (t : ι) : Set (ℝ×ℝ) :=
…

Mentions: OAI.LipschitzHilbert.PhysicalReferenceData

theorem OAI.LipschitzHilbert.parentShiftReferenceBad_eq_union line 107
theorem OAI.LipschitzHilbert.parentShiftReferenceBad_measurable line 129
theorem OAI.LipschitzHilbert.parentShiftReferenceBad_compl line 140
theorem OAI.LipschitzHilbert.parentShiftReference_card_le line 153