ResidueAttenuation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform residue attenuation from a two-split kernel estimate

This is the finite operator step in the residue-flattening argument. Its hypothesis concerns the kernel, and its conclusion holds simultaneously for every input, including an input chosen using an external parameter.

theorem OAI.JointDickman.residueChannel_square_bound line 20

Source documentation

A uniform residue-independent kernel approximation controls the whole unit ball of the channel, rather than just a fixed input.

theorem residueChannel_square_bound {Ω D R : Type*}
    [Fintype Ω] [Fintype D] [Fintype R] [Nonempty R]
    (w : Ω → ℝ) (μ : D → ℝ) (p : Ω → D × R → ℝ)
    (hw : ∀ s, 0 ≤ w s) (hμ : ∀ d, 0 < μ d)
    (G : D → D → ℝ) {ε : ℝ} (hε : 0 ≤ ε)
    (hK : ∀ d e r s,
      |finiteTwoSplitKernel w (fun a : D × R => μ a.1) p (d, r) (e, s) - G d e| ≤ ε)
    (f : Ω → ℝ) :
    (∑ a : D × R, μ a.1 *
      (finiteChannel w (fun a : D × R => μ a.1) p f a -
        finiteResidueAverage (fun t => finiteChannel w (fun a : D × R => μ a.1) p f (a.1, t))) ^ 2) ≤
      (4 * ε * ∑ a : D × R, μ a.1) * ∑ s, w s * f s ^ 2 := by
…

Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.finiteChannel, OAI.JointDickman.finiteResidueAverage