CenteredKernelRows.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Centered rows after discarding a small part of a kernel

Uniform averaging in a residue coordinate preserves weighted sums because all residues over a base cell have the same weight. A nonnegative discarded kernel therefore costs at most four times its row bound after centering. The remaining kernel can be compared with a residue-independent kernel.

theorem OAI.JointDickman.finiteResidueAverage_nonneg line 18
theorem OAI.JointDickman.finiteResidueAverage_mono line 22
theorem OAI.JointDickman.finiteResidueAverage_le line 28
theorem OAI.JointDickman.sum_finiteResidueAverage line 33

theorem OAI.JointDickman.weighted_sum_residueAverage line 40

Source documentation

Averaging within an equal-weight residue fibre preserves total mass.

theorem weighted_sum_residueAverage {D R : Type*}
    [Fintype D] [Fintype R] [Nonempty R] (μ : D → ℝ) (f : D × R → ℝ) :
    (∑ a : D × R, μ a.1 * finiteResidueAverage (fun t => f (a.1, t))) =
      ∑ a : D × R, μ a.1 * f a := by
…

Mentions: OAI.JointDickman.finiteResidueAverage

theorem OAI.JointDickman.residueCenteredKernel_add line 50

theorem OAI.JointDickman.residueCenteredKernel_nonneg_rows line 60

Source documentation

All four nonnegative terms of the centering formula have controlled weighted row sums. Only equality of weights inside each fibre is used.

theorem residueCenteredKernel_nonneg_rows {D R : Type*}
    [Fintype D] [Fintype R] [Nonempty R]
    (μ : D → ℝ) (K : D × R → D × R → ℝ)
    (hμ : ∀ d, 0 ≤ μ d) (hK : ∀ a b, 0 ≤ K a b) {C : ℝ}
    (hrow : ∀ a, (∑ b : D × R, μ b.1 * K a b) ≤ C) (a : D × R) :
    (∑ b : D × R, μ b.1 * |residueCenteredKernel K a b|) ≤ 4 * C := by
…

Mentions: OAI.JointDickman.residueCenteredKernel

theorem OAI.JointDickman.residueCenteredKernel_rows_of_discarded line 111

Source documentation

Decompose the actual kernel into a nonnegative discarded part with small row mass and a part uniformly close to a residue-independent kernel.

theorem residueCenteredKernel_rows_of_discarded {D R : Type*}
    [Fintype D] [Fintype R] [Nonempty R]
    (μ : D → ℝ) (K L H : D × R → D × R → ℝ) (G : D → D → ℝ)
    (hμ : ∀ d, 0 ≤ μ d) (hL : ∀ a b, 0 ≤ L a b)
    (hdecomp : ∀ a b, K a b = L a b + H a b) {C ε : ℝ}
    (hrow : ∀ a, (∑ b : D × R, μ b.1 * L a b) ≤ C)
    (hflat : ∀ d e r s, |H (d, r) (e, s) - G d e| ≤ ε) (a : D × R) :
    (∑ b : D × R, μ b.1 * |residueCenteredKernel K a b|) ≤
      4 * C + 4 * ε * ∑ b : D × R, μ b.1 := by
…

Mentions: OAI.JointDickman.residueCenteredKernel

theorem OAI.JointDickman.residueChannel_square_of_discarded line 140

Source documentation

The discarded-plus-flat kernel estimate controls the entire centered channel, uniformly for every real input.

theorem residueChannel_square_of_discarded {Ω D R : Type*}
    [Fintype Ω] [Fintype D] [Fintype R] [Nonempty R]
    (w : Ω → ℝ) (μ : D → ℝ) (p : Ω → D × R → ℝ)
    (L H : D × R → D × R → ℝ) (G : D → D → ℝ)
    (hw : ∀ x, 0 ≤ w x) (hμ : ∀ d, 0 < μ d) (hL : ∀ a b, 0 ≤ L a b)
    (hdecomp : ∀ a b, finiteTwoSplitKernel w (fun a : D × R => μ a.1) p a b =
      L a b + H a b) {C ε : ℝ} (hC : 0 ≤ C) (hε : 0 ≤ ε)
    (hrow : ∀ a, (∑ b : D × R, μ b.1 * L a b) ≤ C)
    (hflat : ∀ d e r s, |H (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 =>
…

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