OAI/NumberTheory/JointDickman/Probability/LowExclusiveKernel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.optionCellMass line 22
2. theorem OAI.JointDickman.optionCellMass_nonneg line 26
3. theorem OAI.JointDickman.optionCellMass_sum_le line 32
4. def OAI.JointDickman.lowExclusiveProbability line 42
5. theorem OAI.JointDickman.lowExclusiveProbability_nonneg line 45
6. def OAI.JointDickman.independentCellMarginal line 51
7. def OAI.JointDickman.lowExclusiveMass line 57

   Source documentation

   The common mass is integrated after multiplying the two independent exclusive cell probabilities; only the second exclusive is restricted.

   noncomputable def lowExclusiveMass (w : C → ℝ) (v : E → ℝ)
       (cell : C → E → Option A) (low : E → Prop) [DecidablePred low] (a b : A) : ℝ :=
   …

8. theorem OAI.JointDickman.lowExclusiveMass_nonneg line 63
9. theorem OAI.JointDickman.lowExclusiveMass_eq_triple line 75

   Source documentation

   This factorized definition is precisely the restricted independent triple law; it includes no assumption about its row or column behavior.

   theorem lowExclusiveMass_eq_triple (w : C → ℝ) (v : E → ℝ)
       (cell : C → E → Option A) (low : E → Prop) [DecidablePred low] (a b : A) :
       lowExclusiveMass w v cell low a b =
         ∑ c, ∑ e₂, ∑ e₁, if low e₂ ∧ cell c e₁ = some a ∧ cell c e₂ = some b then
           w c * v e₁ * v e₂ else 0 := by
   …

   Mentions: OAI.JointDickman.lowExclusiveMass

10. theorem OAI.JointDickman.lowExclusiveMass_row line 93

    Source documentation

    The row estimate uses the fact that an exclusive output belongs to at most one retained cell.

    theorem lowExclusiveMass_row (w : C → ℝ) (v : E → ℝ)
        (cell : C → E → Option A) (low : E → Prop) [DecidablePred low]
        (hw : ∀ c, 0 ≤ w c) (hv : ∀ e, 0 ≤ v e) (a : A) :
        (∑ b, lowExclusiveMass w v cell low a b) ≤
          lowExclusiveProbability v low * independentCellMarginal w v cell a := by
    …

    Mentions: OAI.JointDickman.lowExclusiveMass, OAI.JointDickman.lowExclusiveProbability, OAI.JointDickman.independentCellMarginal

11. theorem OAI.JointDickman.lowExclusiveMass_integrate_common line 117

    Source documentation

    Integrating the common variable after conditioning on the restricted exclusive variable. This is the precise conditional mass used for columns.

    theorem lowExclusiveMass_integrate_common (w : C → ℝ) (v : E → ℝ)
        (cell : C → E → Option A) (low : E → Prop) [DecidablePred low] (b : A) :
        (∑ c, w c * optionCellMass (fun e => if low e then v e else 0) (cell c) b) =
          ∑ e, if low e then v e * optionCellMass w (fun c => cell c e) b else 0 := by
    …

    Mentions: OAI.JointDickman.optionCellMass

12. theorem OAI.JointDickman.lowExclusiveMass_column line 135

    Source documentation

    The column estimate uses the normalized first exclusive law and a uniform conditional common-variable cell estimate at every low exclusive.

    theorem lowExclusiveMass_column (w : C → ℝ) (v : E → ℝ)
        (cell : C → E → Option A) (low : E → Prop) [DecidablePred low]
        (hw : ∀ c, 0 ≤ w c) (hv : ∀ e, 0 ≤ v e) (hv1 : ∑ e, v e = 1)
        {H : ℝ} (hcommon : ∀ e, low e → ∀ b, optionCellMass w (fun c => cell c e) b ≤ H)
        (b : A) : (∑ a, lowExclusiveMass w v cell low a b) ≤ lowExclusiveProbability v low * H := by
    …

    Mentions: OAI.JointDickman.optionCellMass, OAI.JointDickman.lowExclusiveMass, OAI.JointDickman.lowExclusiveProbability

13. def OAI.JointDickman.lowExclusiveKernel line 172

    Source documentation

    Equal cell atom weights give the manuscript's m⁻² kernel.

    noncomputable def lowExclusiveKernel (w : C → ℝ) (v : E → ℝ)
        (cell : C → E → Option A) (low : E → Prop) [DecidablePred low]
        (m : ℝ) (a b : A) : ℝ := lowExclusiveMass w v cell low a b / (m * m)

    Mentions: OAI.JointDickman.lowExclusiveMass

14. theorem OAI.JointDickman.lowExclusiveKernel_weighted_row line 176
15. theorem OAI.JointDickman.lowExclusiveKernel_weighted_column line 191
16. theorem OAI.JointDickman.lowExclusiveKernel_square_bound line 209

    Source documentation

    A finite Schur conclusion derived from the two distinct local-law estimates; neither a discarded-event operator bound nor a row bound is assumed.

    theorem lowExclusiveKernel_square_bound (w : C → ℝ) (v : E → ℝ)
        (cell : C → E → Option A) (low : E → Prop) [DecidablePred low]
        (hw : ∀ c, 0 ≤ w c) (hv : ∀ e, 0 ≤ v e) (hv1 : ∑ e, v e = 1)
        {m H : ℝ} (hm : 0 < m) (hH : 0 ≤ H)
        (hmarginal : ∀ a, independentCellMarginal w v cell a ≤ H * m)
        (hcommon : ∀ e, low e → ∀ b, optionCellMass w (fun c => cell c e) b ≤ H * m)
        (f : A → ℝ) :
        (∑ a, m * finiteKernelAction (fun _ => m) (lowExclusiveKernel w v cell low m) f a ^ 2) ≤
          (lowExclusiveProbability v low * H) ^ 2 * ∑ a, m * f a ^ 2 := by
    …

    Mentions: OAI.JointDickman.independentCellMarginal, OAI.JointDickman.optionCellMass, OAI.JointDickman.finiteKernelAction, OAI.JointDickman.lowExclusiveKernel, OAI.JointDickman.lowExclusiveProbability