SourceSingleScaleEnvelope.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The single-scale estimate in §5, conc:original-positive. The lattice estimate is summed at the source point before integrating. Only pointwise overlap of the label multipliers appears, so the estimate has no factor counting the available labels.

theorem OAI.LipschitzHilbert.planarPositiveConvolution_sum line 16
theorem OAI.LipschitzHilbert.planarPositiveConvolution_le line 27
theorem OAI.LipschitzHilbert.sum_planarPositiveConvolution_le line 60

theorem OAI.LipschitzHilbert.source_single_scale_envelope line 77

Source documentation

Each label may have its own translated lattice. They share the physical scale, transverse width, source test, and pointwise overlap budget. All analyzing coefficients are the actual integral coefficients.

theorem source_single_scale_envelope {Λ κ : Type*} [Fintype Λ] [Fintype κ]
    (ι : Λ → Type*) [∀ b, Fintype (ι b)]
    (site : ∀ b, ι b → ℤ×ℤ) (hinj : ∀ b, Function.Injective (site b))
    (originX originY : Λ → ℝ) {l W B : ℝ} (hl : 0 < l) (hW : 0 < W) (hB : 0 ≤ B)
    (source : Λ → ℝ×ℝ → ℝ) (hmeas : ∀ b, Measurable (source b))
    (hnonneg : ∀ b z, 0 ≤ source b z) (hoverlap : ∀ z, ∑ b, source b z ≤ B)
    (wave : ∀ b, ι b → κ → ℝ×ℝ → ℂ) (hwave : ∀ b i k, Measurable (wave b i k))
    (hbound : ∀ b i k z, ‖wave b i k z‖ ≤
      tileEnvelope (originX b+l*(site b i).1) (originY b+W*(site b i).2) l W 6 z*source b z)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1)
    (z : ℝ×ℝ) :
    (∑ b, ∑ i, ‖analyzingCoefficient volume (fun _ : ι b => l*W) (wave b) g i‖*
…

Mentions: OAI.LipschitzHilbert.tileEnvelope, OAI.LipschitzHilbert.analyzingCoefficient