PrimeCoarseChannel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Coarse approximation of the actual fair-prime channel

Normalized high-exclusive cell probabilities are compared directly with bounded Lipschitz profiles. Their product yields the smooth mixture kernel; the actual two-split comparison and the low-union estimate then transfer the coarse approximation to the original fair-prime channel.

theorem OAI.JointDickman.product_error_of_bounded_profile line 21

Source documentation

The approximating factors are bounded; the actual factors acquire their bounds from the local errors.

theorem product_error_of_bounded_profile {a b u v M η : ℝ}
    (hM : 0 ≤ M) (hη : 0 ≤ η) (hu : |u| ≤ M) (hv : |v| ≤ M)
    (ha : |a - u| ≤ η) (hb : |b - v| ≤ η) :
    |a * b - u * v| ≤ 2 * M * η + η ^ 2 := by
…

theorem OAI.JointDickman.exclusiveProductKernel_eq_normalized line 41

Source documentation

Dividing the cell probabilities before taking their product gives exactly the normalized exclusive-product kernel.

theorem exclusiveProductKernel_eq_normalized {C D R : Type*} [Fintype C]
    (w : C → ℝ) (p : C → D × R → ℝ) {m : ℝ} (hm : m ≠ 0) (a b : D × R) :
    exclusiveProductKernel w (fun _ => m) p a b =
      ∑ c, w c * (p c a / m) * (p c b / m) := by
…

Mentions: OAI.JointDickman.exclusiveProductKernel

theorem OAI.JointDickman.exclusiveProductKernel_smooth_error line 53

Source documentation

The smooth mixture follows from the normalized cellwise local law; no kernel-approximation premise is needed.

theorem exclusiveProductKernel_smooth_error {C D R : Type*} [Fintype C]
    (w : C → ℝ) (p : C → D × R → ℝ) (f : C → ℝ → ℝ)
    (location : D × R → ℝ) (hw : ∀ c, 0 ≤ w c) (hw1 : ∑ c, w c = 1)
    {m M η : ℝ} (hm : m ≠ 0) (hM : 0 ≤ M) (hη : 0 ≤ η)
    (hf : ∀ c x, |f c x| ≤ M)
    (hlocal : ∀ c a, |p c a / m - f c (location a)| ≤ η) (a b : D × R) :
    |exclusiveProductKernel w (fun _ => m) p a b - smoothMixtureKernel w f location a b| ≤
      2 * M * η + η ^ 2 := by
…

Mentions: OAI.JointDickman.exclusiveProductKernel, OAI.JointDickman.smoothMixtureKernel

theorem OAI.JointDickman.fairPrimeKernel_discarded_smooth_error line 85

Source documentation

Remove the actual independent low union from the original channel kernel. The remaining smooth-mixture error is derived from the local probabilities and the proved actual-to-independent cell comparison.

theorem fairPrimeKernel_discarded_smooth_error {D R : Type*}
    [DecidableEq D] [DecidableEq R]
    (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime) {N : ℕ} (hN : N ≠ 0)
    (hcut : ∀ p ∈ Q, N < p) (cell : ℕ → D × R)
    (low : (Q → Bool) → Prop) [DecidablePred low]
    (f : (Q → Bool) → ℝ → ℝ) (location : D × R → ℝ)
    {m M η : ℝ} (hm : 0 < m) (hM : 0 ≤ M) (hη : 0 ≤ η)
    (hf : ∀ c x, |f c x| ≤ M)
    (hlocal : ∀ c a, |primeHighExclusiveCell Q cell low c a / m - f c (location a)| ≤ η)
    (a b : D × R) :
    |(finiteTwoSplitKernel (fullPrimeMass Q) (fun _ => m) (fairPrimeTransition Q cell) a b -
        primeLowUnionKernel Q cell low m a b) -
…

Mentions: OAI.JointDickman.primeHighExclusiveCell, OAI.JointDickman.finiteTwoSplitKernel, OAI.JointDickman.fullPrimeMass, OAI.JointDickman.fairPrimeTransition, OAI.JointDickman.primeLowUnionKernel

theorem OAI.JointDickman.fairPrimeCoarseChannel_square_bound line 125

Source documentation

Coarse compactness for the actual fair-prime channel, uniformly over every real input. The only arithmetic premises are the two low-event local mass bounds and the normalized high-exclusive local law.

theorem fairPrimeCoarseChannel_square_bound {D R : Type*}
    [Fintype D] [Fintype R] [Nonempty R] [DecidableEq D] [DecidableEq R]
    (Q : Finset ℕ) (hQ : ∀ p ∈ Q, p.Prime) {N : ℕ} (hN : N ≠ 0)
    (hcut : ∀ p ∈ Q, N < p) (cell : ℕ → D × R)
    (low : (Q → Bool) → Prop) [DecidablePred low]
    (f : (Q → Bool) → ℝ → ℝ) (location : D × R → ℝ)
    {m H M η mesh : ℝ} {L₀ : ℝ≥0}
    (hm : 0 < m) (hH : 0 ≤ H) (hM : 0 ≤ M) (hη : 0 ≤ η) (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)
    (hmarginal : ∀ a, independentCellMarginal (quarterPrimeMass Q) (quarterPrimeMass Q)
      (primeOutputCell Q cell) a ≤ H * m)
…

Mentions: OAI.JointDickman.independentCellMarginal, OAI.JointDickman.quarterPrimeMass, OAI.JointDickman.primeOutputCell