FlatExclusiveKernel.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Flattening the retained exclusive-product kernel

Conditioned on the common variable, the two retained exclusive outputs are independent. An additive local-law error for each cell therefore gives an explicit error for their product and for the integrated kernel. The approximating profile may be signed: its required bound follows from the local law and the fact that the actual cell probabilities lie in [0,1].

def OAI.JointDickman.exclusiveProductKernel line 21
Source documentation
Kernel of two conditionally independent exclusive outputs sharing the common variable. The denominators are the output-cell masses.
```
noncomputable def exclusiveProductKernel {C D R : Type*} [Fintype C]
    (w : C → ℝ) (μ : D → ℝ) (p : C → D × R → ℝ) (a b : D × R) : ℝ :=
…
```

def OAI.JointDickman.flatExclusiveKernel line 26

Source documentation

The local-law profile is independent of the residue coordinate.

noncomputable def flatExclusiveKernel {C D : Type*} [Fintype C]
    (w : C → ℝ) (μ : D → ℝ) (v : C → D → ℝ) (d e : D) : ℝ :=
…

theorem OAI.JointDickman.exclusiveProductKernel_eq_finiteTwoSplitKernel line 30
theorem OAI.JointDickman.local_profile_abs_le line 36

theorem OAI.JointDickman.exclusive_probability_product_error line 46

Source documentation

Product error from two genuine cell probabilities and their additive local laws. No separate size bound for the profile is assumed.

theorem exclusive_probability_product_error {a b u v η : ℝ}
    (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) (hb₀ : 0 ≤ b) (hb₁ : b ≤ 1)
    (hη : 0 ≤ η) (ha : |a - u| ≤ η) (hb : |b - v| ≤ η) :
    |a * b - u * v| ≤ 2 * η + η ^ 2 := by
…

theorem OAI.JointDickman.exclusiveProductKernel_flat_error line 63

Source documentation

Integrating the local-law product error against the actual common law does not increase it.

theorem exclusiveProductKernel_flat_error {C D R : Type*} [Fintype C]
    (w : C → ℝ) (μ : D → ℝ) (p : C → D × R → ℝ) (v : C → D → ℝ)
    (hw : ∀ c, 0 ≤ w c) (hwnorm : ∑ c, w c = 1)
    (hμ : ∀ d, 0 < μ d) (hp₀ : ∀ c a, 0 ≤ p c a) (hp₁ : ∀ c a, p c a ≤ 1)
    {η : ℝ} (hη : 0 ≤ η)
    (hlocal : ∀ c d r, |p c (d, r) - v c d| ≤ η) (d e : D) (r s : R) :
    |exclusiveProductKernel w μ p (d, r) (e, s) - flatExclusiveKernel w μ v d e| ≤
      (2 * η + η ^ 2) / (μ d * μ e) := by
…

Mentions: OAI.JointDickman.exclusiveProductKernel, OAI.JointDickman.flatExclusiveKernel

theorem OAI.JointDickman.exclusiveProductKernel_flat_error_uniform line 97

Source documentation

A common positive lower bound for the cell weights makes the kernel error uniform over all pairs of output cells.

theorem exclusiveProductKernel_flat_error_uniform {C D R : Type*} [Fintype C]
    (w : C → ℝ) (μ : D → ℝ) (p : C → D × R → ℝ) (v : C → D → ℝ)
    (hw : ∀ c, 0 ≤ w c) (hwnorm : ∑ c, w c = 1)
    {m : ℝ} (hm : 0 < m) (hmin : ∀ d, m ≤ μ d)
    (hp₀ : ∀ c a, 0 ≤ p c a) (hp₁ : ∀ c a, p c a ≤ 1)
    {η : ℝ} (hη : 0 ≤ η)
    (hlocal : ∀ c d r, |p c (d, r) - v c d| ≤ η) (d e : D) (r s : R) :
    |exclusiveProductKernel w μ p (d, r) (e, s) - flatExclusiveKernel w μ v d e| ≤
      (2 * η + η ^ 2) / (m * m) := by
…

Mentions: OAI.JointDickman.exclusiveProductKernel, OAI.JointDickman.flatExclusiveKernel

theorem OAI.JointDickman.residueChannel_square_of_exclusive_local_law line 115

Source documentation

The finite cutoff and flattening step for the actual channel. The high kernel is the independently retained exclusive-product law; only its cellwise local law is required, not an assumed kernel approximation.

theorem residueChannel_square_of_exclusive_local_law {Ω C D R : Type*}
    [Fintype Ω] [Fintype C] [Fintype D] [Fintype R] [Nonempty R]
    (wΩ : Ω → ℝ) (μ : D → ℝ) (q : Ω → D × R → ℝ)
    (w : C → ℝ) (p : C → D × R → ℝ) (v : C → D → ℝ)
    (L : D × R → D × R → ℝ)
    (hwΩ : ∀ x, 0 ≤ wΩ x) (hw : ∀ c, 0 ≤ w c) (hwnorm : ∑ c, w c = 1)
    {m : ℝ} (hm : 0 < m) (hmin : ∀ d, m ≤ μ d)
    (hp₀ : ∀ c a, 0 ≤ p c a) (hp₁ : ∀ c a, p c a ≤ 1)
    (hL : ∀ a b, 0 ≤ L a b)
    (hdecomp : ∀ a b, finiteTwoSplitKernel wΩ (fun a : D × R => μ a.1) q a b =
      L a b + exclusiveProductKernel w μ p a b)
    {B η : ℝ} (hB : 0 ≤ B) (hη : 0 ≤ η)
…

Mentions: OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.exclusiveProductKernel