SourceLabeledErrorConvolution.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Angular errors are summed over their active labels at the source point, before the lattice convolution. Consequently the wide reference cone contributes no factor counting all available labels.

theorem OAI.LipschitzHilbert.sum_planarPositiveConvolution_le_source line 18

Source documentation

Pointwise domination of the sum of sources passes through the common positive convolution, with the same constant.

theorem sum_planarPositiveConvolution_le_source {Λ : Type*} [Fintype Λ]
    (f : Λ → ℝ×ℝ → ℝ) (hf : ∀ b, Measurable (f b)) (hf0 : ∀ b z, 0 ≤ f b z)
    (source : ℝ×ℝ → ℝ) (hs : Measurable source) (hs0 : ∀ z, 0 ≤ source z)
    {l W C B : ℝ} (hl : 0 < l) (hW : 0 < W) (hC : 0 ≤ C) (_hB : 0 ≤ B)
    (hsB : ∀ z, source z ≤ B) (hoverlap : ∀ z, ∑ b, f b z ≤ C*source z)
    (x y : ℝ) :
    (∑ b, planarPositiveConvolution l W (f b) x y) ≤
      C*planarPositiveConvolution l W source x y := by
…

Mentions: OAI.LipschitzHilbert.planarPositiveConvolution

theorem OAI.LipschitzHilbert.source_labeled_error_convolution line 49

Source documentation

The actual coefficient error for a finite family of translated lattices. Only active selector labels enter the source overlap.

theorem source_labeled_error_convolution {Λ κ : Type*} [Fintype Λ] [Fintype κ]
    (ι : Λ → Type*) [∀ b, Fintype (ι b)]
    (site : ∀ b, ι b → ℤ×ℤ) (hinj : ∀ b, Function.Injective (site b))
    (originX originY slope : Λ → ℝ) {l W d radius C M Lip small wide : ℝ} {K H : ℕ}
    (hl : 0 < l) (hW : 0 < W) (hd : 0 < d)
    (hC : 0 ≤ C) (hM : 0 ≤ M) (hLip : 0 ≤ Lip)
    (hsmall : 0 < small) (hsmall1 : small ≤ 1) (hwide : 1 ≤ wide)
    (hlocal : SourceSlopeLabels.LocalMultiplicity Finset.univ slope d H) (hK : radius ≤ K)
    (selector : Λ → κ → ℝ → ℂ) (hselector : ∀ b k, Measurable (selector b k))
    (hselectorBound : ∀ b k s, ‖selector b k s‖ ≤ M)
    (hsupport : ∀ b k s, selector b k s ≠ 0 → |s-slope b| ≤ radius*d)
    (direction : ℝ×ℝ → ℝ) (hdirection : Measurable direction) (t : ℝ)
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity