SourceSlopeLabels.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The slope-label multiplicity assumption in §2 of the manuscript gives a uniform number of labels active at a fixed source direction. This includes vector-valued selectors: taking the union over all bin components does not increase the count. The last lemmas split the active labels at every scale into a fixed finite set of lattice slots.

def OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity line 28
Source documentation
The source's local label multiplicity, using half-open intervals to assign boundary labels unambiguously.
```
def LocalMultiplicity (labels : Finset ι) (slope : ι → ℝ) (d : ℝ) (M : ℕ) : Prop :=
…
```
def OAI.LipschitzHilbert.SourceSlopeLabels.window line 32
Source documentation
All labels whose slope lies in the indicated reference window.
```
def window (labels : Finset ι) (slope : ι → ℝ) (t d radius : ℝ) : Finset ι := by
…
```
theorem OAI.LipschitzHilbert.SourceSlopeLabels.window_card_le line 36
def OAI.LipschitzHilbert.SourceSlopeLabels.active line 87
Source documentation
Active labels for any number of components. The selector support is common to the label, so the bound has no component-count factor.
```
def active (labels : Finset ι) {κ : Type*} (selector : ι → κ → ℝ → ℂ)
    (t : ℝ) : Finset ι := by
…
```
theorem OAI.LipschitzHilbert.SourceSlopeLabels.active_card_le line 92

theorem OAI.LipschitzHilbert.SourceSlopeLabels.active_union_card_le line 109

Source documentation

For coefficient errors the original and frozen selectors contribute at most twice the same absolute label bound.

theorem active_union_card_le (labels : Finset ι) (slope : ι → ℝ)
    {κ : Type*} (selector : ι → κ → ℝ → ℂ)
    {t u d radius : ℝ} {M K : ℕ} (hd : 0 < d)
    (hlocal : LocalMultiplicity labels slope d M) (hK : radius ≤ K)
    (hsupport : ∀ i ∈ labels, ∀ k x, selector i k x ≠ 0 →
      |x - slope i| ≤ radius * d) :
    ((active labels selector u) ∪ (active labels selector t)).card ≤
      2 * ((2 * K + 1) * M) := by
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity, OAI.LipschitzHilbert.SourceSlopeLabels.active

def OAI.LipschitzHilbert.SourceSlopeLabels.slots line 129
Source documentation
Each scale has its own label assignment, but the same finite set of slots suffices for all scales. Inactive slots may be represented by an empty spatial lattice.
```
def slots {J : Type*} {Label : J → Type*} (labels : ∀ j, Finset (Label j))
    {B : ℕ} (hcard : ∀ j, (labels j).card ≤ B) (j : J) : labels j ↪ Fin B := by
…
```
theorem OAI.LipschitzHilbert.SourceSlopeLabels.slots_injective line 134

theorem OAI.LipschitzHilbert.SourceSlopeLabels.slot_fiber_card_le_one line 140

Source documentation

A slot contains at most one active label at a given scale.

theorem slot_fiber_card_le_one {J : Type*} {Label : J → Type*}
    (labels : ∀ j, Finset (Label j)) {B : ℕ}
    (hcard : ∀ j, (labels j).card ≤ B) (j : J) (b : Fin B) :
    (Finset.univ.filter (fun i : labels j => slots labels hcard j i = b)).card ≤ 1 := by
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.slots

theorem OAI.LipschitzHilbert.SourceSlopeLabels.sum_slots line 151

Source documentation

Exact splitting of a finite packet sum into its label slots.

theorem sum_slots {J : Type*} {Label : J → Type*}
    (labels : ∀ j, Finset (Label j)) {B : ℕ}
    (hcard : ∀ j, (labels j).card ≤ B) {E : Type*} [AddCommMonoid E]
    (j : J) (f : Label j → E) :
    ∑ i ∈ labels j, f i =
      ∑ b : Fin B, ∑ i : labels j, if slots labels hcard j i = b then f i else 0 := by
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.slots

def OAI.LipschitzHilbert.SourceSlopeLabels.labelAtSlot line 163
Source documentation
Recover the optional label for a slot without choosing any distinguished label at an empty scale.
```
def labelAtSlot {A : Type*} {B : ℕ} (e : A ↪ Fin B) (b : Fin B) : Option A :=
…
```
theorem OAI.LipschitzHilbert.SourceSlopeLabels.labelAtSlot_at line 166
theorem OAI.LipschitzHilbert.SourceSlopeLabels.labelAtSlot_eq_some line 175
def OAI.LipschitzHilbert.SourceSlopeLabels.SlotItem line 190
Source documentation
The spatial items retained in one label slot at a fixed scale.
```
def SlotItem {A : Type*} {B : ℕ} (e : A ↪ Fin B) (Item : A → Type*) (b : Fin B) :=
…
```
theorem OAI.LipschitzHilbert.SourceSlopeLabels.slotItem_label line 193
theorem OAI.LipschitzHilbert.SourceSlopeLabels.slotItem_site_injective line 201
Source documentation
Although labels can have overlapping integer sites, one slot never mixes two labels at a fixed scale. Its original spatial site map is therefore injective, as required by the packet-family constructor.
```
theorem slotItem_site_injective {A : Type*} {B : ℕ} (e : A ↪ Fin B)
    {Item : A → Type*} (site : ∀ i, Item i → ℤ × ℤ)
    (hsite : ∀ i, Function.Injective (site i)) (b : Fin B) :
    Function.Injective (fun p : SlotItem e Item b => site p.1.1 p.1.2) := by
…
```
Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.SlotItem