SourcePhysicalSingleScale.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A single length of original physical packets has a uniform positive summation bound. Selector overlap is counted before convolution. The analyzing coefficients remain those of the original profiles, while the synthesis profiles may be any profiles with the same seminorm bound.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMultiplierCoefficient_shear line 21

Source documentation

The shear changes coordinates, not the original analyzing coefficient.

theorem physicalMultiplierCoefficient_shear (t : ℝ)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ)
    (j : Fin N) (l : P.labels j) (u : Item j l) :
    analyzingCoefficient volume (fun _ : Item j l => P.length j*P.width)
      (fun u k z => b j l k (v (slopeShear t z))*P.raw 0 j l u k z.2 z.1)
      (fun z => g (slopeShear t z)) u =
        P.physicalMultiplierCoefficient t b v g j l u := by
…

Mentions: OAI.LipschitzHilbert.analyzingCoefficient, OAI.LipschitzHilbert.slopeShear

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_single_scale_coefficients line 46

Source documentation

The positive coefficient sum has no factor for the total number of labels. Only the selector's local multiplicity enters.

theorem physical_single_scale_coefficients (horder : 6 ≤ P.order)
    (j : Fin N) (t d radius M : ℝ) (K H : ℕ)
    (hd : 0 < d) (hM : 0 ≤ M) (hK : radius ≤ K)
    (hlocal : SourceSlopeLabels.LocalMultiplicity Finset.univ
      (fun l : P.labels j => t+P.rowSlope j l) d H)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (hb : ∀ l k, Measurable (b j l k))
    (hbM : ∀ l k s, ‖b j l k s‖ ≤ M)
    (hsupport : ∀ l k s, b j l k s ≠ 0 →
      |s-(t+P.rowSlope j l)| ≤ radius*d)
    (v : ℝ×ℝ → ℝ) (hv : Measurable v)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_single_scale_raw_synthesis line 83

Source documentation

Any selected packets at the given length, with alternate synthesis and any of the three covariant jets, obey the same positive bound.

theorem physical_single_scale_raw_synthesis (horder : 6 ≤ P.order)
    (i : Fin 3) (j : Fin N) (t d radius M : ℝ) (K H : ℕ)
    (hd : 0 < d) (hM : 0 ≤ M) (hK : radius ≤ K)
    (hlocal : SourceSlopeLabels.LocalMultiplicity Finset.univ
      (fun l : P.labels j => t+P.rowSlope j l) d H)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (hb : ∀ l k, Measurable (b j l k))
    (hbM : ∀ l k s, ‖b j l k s‖ ≤ M)
    (hsupport : ∀ l k s, b j l k s ≠ 0 →
      |s-(t+P.rowSlope j l)| ≤ radius*d)
    (v : ℝ×ℝ → ℝ) (hv : Measurable v)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_single_scale_cross_packets line 126

Source documentation

The same bound in the original physical coordinates, restricted to any finite packet set at one length.

theorem physical_single_scale_cross_packets (horder : 6 ≤ P.order)
    (i : Fin 3) (j : Fin N) (t d radius M : ℝ) (K H : ℕ)
    (hd : 0 < d) (hM : 0 ≤ M) (hK : radius ≤ K)
    (hlocal : SourceSlopeLabels.LocalMultiplicity Finset.univ
      (fun l : P.labels j => t+P.rowSlope j l) d H)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (hb : ∀ l k, Measurable (b j l k))
    (hbM : ∀ l k s, ‖b j l k s‖ ≤ M)
    (hsupport : ∀ l k s, b j l k s ≠ 0 →
      |s-(t+P.rowSlope j l)| ≤ radius*d)
    (v : ℝ×ℝ → ℝ) (hv : Measurable v)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_single_scale_masked_packets line 161

Source documentation

Multiplying each synthesis packet by its actual top mask does not enlarge the single-scale bound.

theorem physical_single_scale_masked_packets (horder : 6 ≤ P.order)
    (j : Fin N) (t d radius M : ℝ) (K H : ℕ)
    (hd : 0 < d) (hM : 0 ≤ M) (hK : radius ≤ K)
    (hlocal : SourceSlopeLabels.LocalMultiplicity Finset.univ
      (fun l : P.labels j => t+P.rowSlope j l) d H)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ)
    (hb : ∀ l k, Measurable (b j l k))
    (hbM : ∀ l k s, ‖b j l k s‖ ≤ M)
    (hsupport : ∀ l k s, b j l k s ≠ 0 →
      |s-(t+P.rowSlope j l)| ≤ radius*d)
    (v : ℝ×ℝ → ℝ) (hv : Measurable v)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_single_scale_budget line 195

Source documentation

The fixed selector constants cost only one additional polynomial power, uniformly before choosing the packet family.

theorem eventually_single_scale_budget (q M : ℝ) (hM : 0 ≤ M) (K H : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ C : ℝ, 0 ≤ C → C ≤ L^q →
      C*((64*(4*Real.pi)^2)*((C*M*((2*K+1)*H:ℕ))*Real.pi^2)) ≤ L^(2*q+1) := by
…