SourceReferenceUnion.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

A common reference lattice collects the uniquely assigned packets from all tops. Disjointness is imposed on the actual sites, not paid for by summing bounds over top labels. Profiles and waves are unchanged.

theorem OAI.LipschitzHilbert.sigma_site_injective line 15

def OAI.LipschitzHilbert.SourceLabeledLattice.referenceItems line 34

Source documentation

Retain the common scale/label geometry while supplying actual packet sites and profiles from a subcollection or disjoint union.

def referenceItems (I : ∀ j, Label j → Type) [∀ j l, Fintype (I j l)]
    (site : ∀ j (l : P.labels j), I j l → ℤ×ℤ)
    (hinj : ∀ j l, Function.Injective (site j l))
    (profile : ∀ j (l : P.labels j), I j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hprofile : ∀ j l u k, planarProfileConstant (profile j l u k) (2*P.order) ≤ P.profileBound) :
    SourceLabeledLattice N κ Label I where
…

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

def OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference line 75
Source documentation
The common reference collection has the original profile bound. Its constant contains no factor counting the source tops.
```
def flattenReference : SourceLabeledLattice N κ Label (fun j l => Σ t, I t j l) :=
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference_constant line 81
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference_actualX line 84
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference_actualZ line 88
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference_physicalPacket line 92

theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference_sum line 103

Source documentation

Recombination is an exact finite sum, before any norm estimate.

theorem flattenReference_sum {E : Type*} [AddCommMonoid E]
    (f : ∀ t j (l : P.labels j), I t j l → E) :
    (∑ j, ∑ l : P.labels j, ∑ u : Σ t, I t j l, f u.1 j l u.2) =
      ∑ t : τ, ∑ j, ∑ l : P.labels j, ∑ u : I t j l, f t j l u := by
…

def OAI.LipschitzHilbert.SourceLabeledLattice.referenceComponent line 116
Source documentation
The component top inside the same common reference geometry.
```
def referenceComponent (t : τ) : SourceLabeledLattice N κ Label (I t) :=
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference_component_raw line 124
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference_component_physicalCoefficient line 129

theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenReference_rawInterval line 137

Source documentation

Recombine source amplitudes before taking a norm or invoking a reference moment estimate.

theorem flattenReference_rawInterval
    (coeff : ∀ t j (l : P.labels j), I t j l → EuclideanSpace ℂ κ)
    (i : Fin 3) (lower upper : ℕ) (x y : ℝ) :
    (P.flattenReference I site hjoint profile hprofile).rawInterval
      (fun j l u => coeff u.1 j l u.2) i lower upper x y =
      ∑ t : τ, (P.referenceComponent I site hjoint profile hprofile t).rawInterval
        (coeff t) i lower upper x y := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice.rawInterval

theorem OAI.LipschitzHilbert.SourceLabeledLattice.owner_union_site_injective line 187
Source documentation
Site injection of a unique packet-to-top assignment is automatic: forgetting the owner is the natural equivalence of all ownership fibers with the original packet set.
```
theorem owner_union_site_injective (owner : ∀ j (l : P.labels j), Item j l → τ)
    (j : Fin N) (l : P.labels j) :
    Function.Injective (fun u : Σ t, {i : Item j l // owner j l i = t} => P.site j l u.2.val) :=
…
```
def OAI.LipschitzHilbert.SourceLabeledLattice.flattenOwnedReference line 194
Source documentation
The actual ownership-fiber union, preserving every original profile and integer site without repetition.
```
def flattenOwnedReference (owner : ∀ j (l : P.labels j), Item j l → τ) :
    SourceLabeledLattice N κ Label
      (fun j l => Σ t, {i : Item j l // ∃ h : l ∈ P.labels j, owner j ⟨l,h⟩ i = t}) :=
…
```
Mentions: OAI.LipschitzHilbert.SourceLabeledLattice
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenOwnedReference_constant line 219
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenOwnedReference_physicalPacket line 222

def OAI.LipschitzHilbert.SourceLabeledLattice.ownedReferenceEquiv line 230

Source documentation

Forgetting an owner is a bijection, rather than a bounded-multiplicity map. This is why recombination has no top-count loss.

def ownedReferenceEquiv (owner : ∀ j (l : P.labels j), Item j l → τ)
    (j : Fin N) (l : P.labels j) :
    (Σ t, {i : Item j l // ∃ h : l.val ∈ P.labels j, owner j ⟨l.val,h⟩ i = t}) ≃ Item j l :=
…

theorem OAI.LipschitzHilbert.SourceLabeledLattice.sum_ownedReference line 239
theorem OAI.LipschitzHilbert.SourceLabeledLattice.flattenOwnedReference_physicalCoefficient line 246