OAI/NumberTheory/JointDickman/Probability/PartialWeightedChannel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.independentPairKernel_weighted line 13
2. theorem OAI.JointDickman.partialFairPrimeKernel_weighted_smooth_error line 24
3. theorem OAI.JointDickman.partialFairPrimeWeightedCoarse_square_bound line 61

   Source documentation

   The discarded weighted mass is controlled by the low union. This proves the coarse estimate for the actual partial-output channel.

   theorem partialFairPrimeWeightedCoarse_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 : ℕ → Option (D × R))
       (weight : (Q → Bool) → ℝ) (low : (Q → Bool) → Prop) [DecidablePred low]
       (hweight : ∀ e, 0 ≤ weight e ∧ weight e ≤ 1)
       (hhigh : ∀ e, ¬low e → weight e = 1)
       (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)
   …