ResidueCentering.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Centering finite channels in the residue coordinate

All residues above the same base cell carry the same atom weight. Thus subtracting the residue average of the transition subtracts exactly the residue average of the channel. The corresponding two-split kernel is centered in both coordinates. A residue-independent approximation cancels, at a loss of at most four in its uniform error.

def OAI.JointDickman.finiteResidueAverage line 19
theorem OAI.JointDickman.finiteResidueAverage_add line 22
theorem OAI.JointDickman.finiteResidueAverage_sub line 27
theorem OAI.JointDickman.finiteResidueAverage_mul_const line 32
theorem OAI.JointDickman.finiteResidueAverage_const_mul line 37
theorem OAI.JointDickman.finiteResidueAverage_div_const line 42
theorem OAI.JointDickman.finiteResidueAverage_sum line 47
theorem OAI.JointDickman.finiteResidueAverage_const line 52
theorem OAI.JointDickman.finiteResidueAverage_abs_le line 58

def OAI.JointDickman.residueCenteredTransition line 73

Source documentation

Subtract the uniform residue average within each base cell.

noncomputable def residueCenteredTransition {Ω D R : Type*} [Fintype R]
    (p : Ω → D × R → ℝ) (s : Ω) (a : D × R) : ℝ :=
…

theorem OAI.JointDickman.residueCenteredTransition_average line 77

theorem OAI.JointDickman.finiteChannel_residueCentered line 87

Source documentation

Equal cell weights make transition centering exactly channel centering. The identity also holds at zero weights, under the usual totalized division.

theorem finiteChannel_residueCentered {Ω D R : Type*} [Fintype Ω] [Fintype D] [Fintype R]
    (w : Ω → ℝ) (μ : D → ℝ) (p : Ω → D × R → ℝ) (f : Ω → ℝ) (d : D) (r : R) :
    finiteChannel w (fun a : D × R => μ a.1) (residueCenteredTransition p) f (d, r) =
      finiteChannel w (fun a : D × R => μ a.1) p f (d, r) -
        finiteResidueAverage (fun t => finiteChannel w (fun a : D × R => μ a.1) p f (d, t)) := by
…

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

def OAI.JointDickman.residueCenteredKernel line 102

Source documentation

Center a kernel in both of its residue coordinates.

noncomputable def residueCenteredKernel {D R : Type*} [Fintype R]
    (K : D × R → D × R → ℝ) (a b : D × R) : ℝ :=
…

theorem OAI.JointDickman.finiteTwoSplitKernel_residueCentered line 110

Source documentation

The kernel of the centered channel is the actual four-term centered two-split kernel. No nonzero-weight assumption is needed for this identity.

theorem finiteTwoSplitKernel_residueCentered {Ω D R : Type*}
    [Fintype Ω] [Fintype R] (w : Ω → ℝ) (μ : D → ℝ) (p : Ω → D × R → ℝ)
    (d e : D) (r s : R) :
    finiteTwoSplitKernel w (fun a : D × R => μ a.1) (residueCenteredTransition p) (d, r) (e, s) =
      residueCenteredKernel (finiteTwoSplitKernel w (fun a : D × R => μ a.1) p) (d, r) (e, s) := by
…

Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.residueCenteredTransition, OAI.JointDickman.residueCenteredKernel

theorem OAI.JointDickman.residueCenteredKernel_sub_base line 128

theorem OAI.JointDickman.residueCenteredKernel_abs_le line 138

Source documentation

A residue-independent approximating kernel disappears after centering; the four remaining averages each contribute at most the uniform error.

theorem residueCenteredKernel_abs_le {D R : Type*} [Fintype R] [Nonempty R]
    (K : D × R → D × R → ℝ) (G : D → D → ℝ) {ε : ℝ}
    (hK : ∀ d e r s, |K (d, r) (e, s) - G d e| ≤ ε) (d e : D) (r s : R) :
    |residueCenteredKernel K (d, r) (e, s)| ≤ 4 * ε := by
…

Mentions: OAI.JointDickman.residueCenteredKernel

theorem OAI.JointDickman.finiteTwoSplitKernel_centered_abs_le line 158

Source documentation

Application of the uniform centering bound to the actual centered two-split kernel of the transition.

theorem finiteTwoSplitKernel_centered_abs_le {Ω D R : Type*}
    [Fintype Ω] [Fintype R] [Nonempty R]
    (w : Ω → ℝ) (μ : D → ℝ) (p : Ω → D × R → ℝ) (G : D → D → ℝ) {ε : ℝ}
    (hK : ∀ d e r s,
      |finiteTwoSplitKernel w (fun a : D × R => μ a.1) p (d, r) (e, s) - G d e| ≤ ε)
    (d e : D) (r s : R) :
    |finiteTwoSplitKernel w (fun a : D × R => μ a.1) (residueCenteredTransition p)
      (d, r) (e, s)| ≤ 4 * ε := by
…

Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.residueCenteredTransition