SourceSlotTails.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Fixed slope slots are summed before taking the source square or variation. Only the fixed slot count enters the union bound; empty slots are allowed. The polynomial threshold and exponential rate absorb this count uniformly before any packet family is chosen.

theorem OAI.LipschitzHilbert.source_slot_square_le line 18
Source documentation
The square of the recombined positive scales costs the sum of the individual slot squares, with constant one.
```
theorem source_slot_square_le {B N : ℕ} (f : Fin B → Fin N → ℝ) :
    Real.sqrt (∑ j, (∑ b, f b j)^2) ≤
      ∑ b, Real.sqrt (∑ j, f b j^2) := by
…
```
theorem OAI.LipschitzHilbert.source_slot_packet_variation_le line 33
Source documentation
Recombining slots before partial sums does not enlarge cubic variation beyond the sum of the separate slot variations.
```
theorem source_slot_packet_variation_le {B N : ℕ} {E : Type*}
    [NormedAddCommGroup E] (f : Fin B → Fin N → E) :
    cubicVariation (packetPartialSum (fun j => ∑ b, f b j)) N ≤
      ∑ b, cubicVariation (packetPartialSum (f b)) N := by
…
```
Mentions: OAI.LipschitzHilbert.cubicVariation, OAI.LipschitzHilbert.packetPartialSum

theorem OAI.LipschitzHilbert.source_slot_bad_subset line 52

Source documentation

A positive extra threshold absorbs every fixed finite slot count, including zero slots.

theorem source_slot_bad_subset {B : ℕ} {X : Type*}
    (f : Fin B → X → ℝ) (F : X → ℝ) {small large : ℝ}
    (_hsmall : 0 < small) (hlarge : (B:ℝ)*small < large)
    (hF : ∀ x, |F x| ≤ ∑ b, |f b x|) :
    {x | large ≤ |F x|} ⊆ ⋃ b, {x | small ≤ |f b x|} := by
…

theorem OAI.LipschitzHilbert.source_slot_tail line 72

Source documentation

General finite-slot union estimate, with an arbitrary reference mass (in the application it is the physical interval length).

theorem source_slot_tail {B : ℕ} {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (f : Fin B → X → ℝ) (F : X → ℝ)
    {small large : ℝ} (hsmall : 0 < small)
    (hlarge : (B:ℝ)*small < large) (hF : ∀ x, |F x| ≤ ∑ b, |f b x|)
    (δ mass : ℝ≥0∞) (htail : ∀ b, μ {x | small ≤ |f b x|} ≤ δ*mass) :
    μ {x | large ≤ |F x|} ≤ (B:ℝ≥0∞)*δ*mass := by
…

theorem OAI.LipschitzHilbert.eventually_source_fixed_slot_tail line 89

Source documentation

The constants are chosen before the slot functions, underlying space or interval. One polynomial power and one exponential unit pay for the fixed number of slots.

theorem eventually_source_fixed_slot_tail (B : ℕ) (a J : ℝ) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (X : Type*) [MeasurableSpace X] (μ : Measure X)
      (f : Fin B → X → ℝ) (F : X → ℝ) (mass : ℝ≥0∞),
      (∀ x, |F x| ≤ ∑ b, |f b x|) →
      (∀ b, μ {x | L^a ≤ |f b x|} ≤
        ENNReal.ofReal (Real.exp (-(J+1)*L))*mass) →
      μ {x | L^(a+1) ≤ |F x|} ≤ ENNReal.ofReal (Real.exp (-J*L))*mass := by
…

theorem OAI.LipschitzHilbert.SourceLatticePacket.physical_centered_square_slot_tail line 126

Source documentation

The actual centered positive squares of all narrow-label slots have one physical exceptional threshold. Each slot may have a different item type, including an empty item type at any scale.

theorem physical_centered_square_slot_tail (hVariation : LepingleInput)
    {lo hi : ℝ} (hlo : 0 < lo) (hhi : 0 ≤ hi)
    (B : ℕ) (q J : ℝ) (hq : 0 ≤ q) (hJ : 0 ≤ J) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (N : ℕ) (κ : Type) (ι : Fin B → Fin N → Type)
      [Fintype κ] [∀ b j, Fintype (ι b j)]
      (P : ∀ b, SourceLatticePacket N κ (ι b)),
      (∀ b, (P b).constant ≤ L^q) →
    ∀ (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ) (_hv : Measurable v)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (_hg : Measurable g) (_hg1 : ∀ z, ‖g z‖ ≤ 1),
      (∀ j, 0 ≤ d j) → Monotone d →
      (∀ b j u k y xi, |xi| < (lo/(P b).topLength)*(2:ℝ)^j.val →
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.SourceLatticePacket.constant

theorem OAI.LipschitzHilbert.SourceLatticePacket.physical_centered_masked_variation_slot_tail line 161

Source documentation

The actual centered masked variations of the fixed narrow-label slots have a common physical tail. Recombining their packet bands is controlled by source_slot_packet_variation_le.

theorem physical_centered_masked_variation_slot_tail (hVariation : LepingleInput)
    {lo hi : ℝ} (hlo : 0 < lo) (hhi : 0 ≤ hi)
    (B : ℕ) (q J A cone : ℝ) (hq : 0 ≤ q) (hJ : 0 ≤ J)
    (hA : 1 < A) (hcone : 0 ≤ cone) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (N : ℕ) (κ : Type) (ι : Fin B → Fin N → Type)
      [Fintype κ] [∀ b j, Fintype (ι b j)]
      (P : ∀ b, SourceLatticePacket N κ (ι b)),
      (∀ b, (P b).constant ≤ L^q) →
    ∀ (c : ∀ b j, ι b j → κ → ℂ) (hc : ∀ b j u k, ‖c b j u k‖ ≤ 1)
      (alt : ∀ b j, ι b j → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ b j u k,
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.SourceLatticePacket.constant