SourceSlottedCoefficient.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Exact transport of selected analyzing integrals and cross-profile packet sums through the finite slope-label splitting. These are algebraic identities and require no concentration or integrability assumptions.

abbrev OAI.LipschitzHilbert.SourceLabeledLattice.PacketIndex line 24
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalSelectedWave line 26
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalCoefficient line 30

abbrev OAI.LipschitzHilbert.SourceLabeledLattice.withProfile line 38

Source documentation

Replace only the profiles in the original labeled collection.

abbrev withProfile (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ × ℝ) ℂ)
    (hAlt : ∀ j l u k,
      planarProfileConstant (alt j l u k) (2 * P.order) ≤ P.profileBound) :
    SourceLabeledLattice N κ Label Item :=
…

Mentions: OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SourceLabeledLattice

theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_physicalSelectedWave line 46
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_physicalCoefficient line 53

theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_mainCoefficient_physical line 66

Source documentation

The reference-line coefficient in each slot is precisely the original physical selected integral, with the same area normalization.

theorem slotted_mainCoefficient_physical (b : Fin B) (t : ℝ) (d : Fin N → ℝ)
    (v : ℝ × ℝ → ℝ) (g : ℝ × ℝ → EuclideanSpace ℂ κ)
    (j : Fin N) (p : P.SlotItem hcard b j) :
    (P.slotted hcard b).family.mainCoefficient d
        (fun z => v (sourceReferenceToPhysical t z))
        (fun z => g (sourceReferenceToPhysical t z)) j p =
      P.physicalCoefficient t d v g j p.1.1 p.1.2 := by
…

Mentions: OAI.LipschitzHilbert.sourceReferenceToPhysical

def OAI.LipschitzHilbert.SourceLabeledLattice.slottedAlt line 80
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slottedAlt_bound line 84
theorem OAI.LipschitzHilbert.SourceLabeledLattice.withProfile_slotted line 90
Source documentation
Profile replacement commutes with the actual slot constructor.
```
theorem withProfile_slotted (b : Fin B) :
    (P.withProfile alt hAlt).slotted hcard b =
      (P.slotted hcard b).withProfile (P.slottedAlt hcard alt b)
        (P.slottedAlt_bound hcard alt hAlt b) := by
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.slotted, OAI.LipschitzHilbert.SourceLabeledLattice.withProfile
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_alt_raw line 96
theorem OAI.LipschitzHilbert.SourceLabeledLattice.slotted_alt_physicalPacket line 104

def OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval line 113

Source documentation

The source interval before splitting labels into lattice slots.

def rawInterval (coeff : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (i : Fin 3) (lower upper : ℕ) (x y : ℝ) : EuclideanSpace ℂ κ :=
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval_scaled_covariant line 119
theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_slotted_rawInterval line 137
theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_slotted_covariant line 171
theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_slotted_cross_rawInterval line 196
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalSynthesis line 218
Source documentation
The finite physical adjoint sum over the original labeled packets.
```
def physicalSynthesis (coeff : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ)
    (t : ℝ) (z : ℝ × ℝ) : EuclideanSpace ℂ κ :=
…
```
theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_slotted_physicalSynthesis line 224
theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_slotted_cross_physicalSynthesis line 240