CoarseChannel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Coarse centering of a smooth mixture kernel

A bounded Lipschitz profile changes little inside each coarse cell. Its common-variable mixture is consequently close to a kernel depending only on the coarse indices. Combining this fact with a discarded row bound gives the finite coarse-channel estimate.

def OAI.JointDickman.smoothMixtureKernel line 19

theorem OAI.JointDickman.smoothMixtureKernel_oscillation line 25

Source documentation

Oscillation of the genuine mixture follows from the Lipschitz profiles, rather than from an assumed kernel oscillation estimate.

theorem smoothMixtureKernel_oscillation {C A : Type*} [Fintype C]
    (w : C → ℝ) (f : C → ℝ → ℝ) (location : A → ℝ)
    (hw : ∀ c, 0 ≤ w c) (hw1 : ∑ c, w c = 1)
    {M mesh : ℝ} {L₀ : ℝ≥0} (hM : 0 ≤ M) (hmesh : 0 ≤ mesh)
    (hf : ∀ c x, |f c x| ≤ M) (hLip : ∀ c, LipschitzWith L₀ (f c))
    (a a' b b' : A) (ha : |location a - location a'| ≤ mesh)
    (hb : |location b - location b'| ≤ mesh) :
    |smoothMixtureKernel w f location a b - smoothMixtureKernel w f location a' b'| ≤
      2 * M * (L₀ : ℝ) * mesh := by
…

Mentions: OAI.JointDickman.smoothMixtureKernel

theorem OAI.JointDickman.smoothMixtureKernel_coarse_error line 79

Source documentation

A chosen representative in each coarse fibre gives a genuinely coarse-only kernel, with the derived oscillation error.

theorem smoothMixtureKernel_coarse_error {C D R : Type*} [Fintype C]
    (w : C → ℝ) (f : C → ℝ → ℝ) (location : D × R → ℝ)
    (hw : ∀ c, 0 ≤ w c) (hw1 : ∑ c, w c = 1)
    {M mesh : ℝ} {L₀ : ℝ≥0} (hM : 0 ≤ M) (hmesh : 0 ≤ mesh)
    (hf : ∀ c x, |f c x| ≤ M) (hLip : ∀ c, LipschitzWith L₀ (f c))
    (hdiam : ∀ d r s, |location (d, r) - location (d, s)| ≤ mesh)
    (r₀ : R) (d e : D) (r s : R) :
    |smoothMixtureKernel w f location (d, r) (e, s) -
      smoothMixtureKernel w f location (d, r₀) (e, r₀)| ≤ 2 * M * (L₀ : ℝ) * mesh :=
…

Mentions: OAI.JointDickman.smoothMixtureKernel

theorem OAI.JointDickman.coarseChannel_square_bound line 94

Source documentation

The finite coarse-channel estimate. The channel kernel is actually decomposed, and only its retained part is approximated by the displayed smooth mixture. Centering is in the fine index inside each coarse cell.

theorem coarseChannel_square_bound {Ω C D R : Type*}
    [Fintype Ω] [Fintype C] [Fintype D] [Fintype R] [Nonempty R]
    (wΩ : Ω → ℝ) (p : Ω → D × R → ℝ) (w : C → ℝ)
    (f : C → ℝ → ℝ) (location : D × R → ℝ)
    (discarded retained : D × R → D × R → ℝ)
    (hwΩ : ∀ x, 0 ≤ wΩ x) (hw : ∀ c, 0 ≤ w c) (hw1 : ∑ c, w c = 1)
    {m B ε M mesh : ℝ} {L₀ : ℝ≥0}
    (hm : 0 < m) (hB : 0 ≤ B) (hε : 0 ≤ ε) (hM : 0 ≤ M) (hmesh : 0 ≤ mesh)
    (hf : ∀ c x, |f c x| ≤ M) (hLip : ∀ c, LipschitzWith L₀ (f c))
    (hdiam : ∀ d r s, |location (d, r) - location (d, s)| ≤ mesh)
    (hdiscarded : ∀ a b, 0 ≤ discarded a b)
    (hrows : ∀ a, (∑ b : D × R, m * discarded a b) ≤ B)
…