OAI/NumberTheory/JointDickman/Probability/SignedHistogramError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.signedSplitProductMass_cell_error line 13

   Source documentation

   Replacing a test on one cell only costs its oscillation times the positive half-prime mass of that cell.

   theorem signedSplitProductMass_cell_error {A : Type*} [DecidableEq A]
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
       (g : Finset ℕ → ℝ) (hg : ∀ S ⊆ P, |g S| ≤ 1)
       (cell : ℕ → Option A) (a : A) (F : ℕ → ℂ) (c : ℂ) (E : ℝ)
       (hosc : ∀ n ∈ primeSplitProductSupport P, cell n = some a → ‖F n-c‖ ≤ E) :
       ‖(∑ n ∈ primeSplitProductSupport P, if cell n = some a then
           (signedSplitProductMass P g n : ℂ)*F n else 0) -
         ((∑ n ∈ primeSplitProductSupport P, if cell n = some a then
           signedSplitProductMass P g n else 0) : ℝ)*c‖ ≤
         E * ∑ n ∈ primeSplitProductSupport P, if cell n = some a then
           primeProductMass P (1/2) n else 0 := by
   …

   Mentions: OAI.JointDickman.primeSplitProductSupport, OAI.JointDickman.signedSplitProductMass, OAI.JointDickman.primeProductMass

2. theorem OAI.JointDickman.manuscriptChannel_cell_average_error line 51

   Source documentation

   The per-cell error in (38), with exactly the delta/phi channel normalization.

   theorem manuscriptChannel_cell_average_error {m₁ B q : ℕ} [NeZero q]
       (hm : 0 < m₁) (hB : 0 < B)
       (g : (auxiliaryPrimes B → Bool) → ℝ) (hg : ∀ x, |g x| ≤ 1)
       (a : Fin (channelFineCount m₁ B) × (ZMod q)ˣ)
       (F : ℝ → ℂ) {L : ℝ} (hL : 0 ≤ L)
       (hF : IntervalIntegrable F volume (channelLower (channelFineCount m₁ B) a.1)
         (channelUpper (channelFineCount m₁ B) a.1))
       (hLip : ∀ u ∈ Set.Icc (channelLower (channelFineCount m₁ B) a.1)
           (channelUpper (channelFineCount m₁ B) a.1),
         ∀ v ∈ Set.Icc (channelLower (channelFineCount m₁ B) a.1)
           (channelUpper (channelFineCount m₁ B) a.1), ‖F u-F v‖ ≤ L*|u-v|) :
       let n := channelFineCount m₁ B
   …

   Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.channelFineCount, OAI.JointDickman.channelLower, OAI.JointDickman.channelUpper