TailMaskCollision.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual tail projection in the giant collision estimate

theorem OAI.Ostmann.tailSupport_cast_injective line 11
theorem OAI.Ostmann.sum_tailDensityMask line 19
def OAI.Ostmann.zmodResidueMass line 24
theorem OAI.Ostmann.tailDensityMask_collision_le line 27

theorem OAI.Ostmann.tailDensityMask_empirical_mean line 62

Source documentation

Projection to the actual finite mask preserves the endpoint average. No distributional approximation occurs in this identity.

theorem tailDensityMask_empirical_mean (A : Set ℕ) (N p : ℕ) (hp : 0 < p)
    (E : Finset ℕ) (μ : ℕ → ℝ) (F : ZMod p → ℝ)
    (hE : ∀ a ∈ E, a ∈ A ∧ N + p < a) :
    (∑ x ∈ tailDensityMask A N p, zmodResidueMass E μ p x * F x) =
      ∑ a ∈ E, μ a * F (a : ZMod p) := by
…

Mentions: OAI.Ostmann.tailDensityMask, OAI.Ostmann.zmodResidueMass

theorem OAI.Ostmann.tailDensityMask_weighted_collision line 82

Source documentation

Logarithmic collision stability also controls any smaller prime weights, including the localized harmonic weights in a giant cell family.

theorem tailDensityMask_weighted_collision {A B : Set ℕ}
    (hA : A.Infinite) (hB : B.Infinite) (N : ℕ)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (hdisjoint : ∀ p ∈ P, Disjoint (tailResidues A N p) (negTailResidues B N p))
    (E D : Finset ℕ) (μ ν : ℕ → ℝ) (w : P → ℝ) (G C : ℝ)
    (hG : 0 < G)
    (hweight : ∀ p : P, w p * (p : ℝ) ≤ Real.log (p : ℝ) / G)
    (hbudget : (∑ p ∈ P, Real.log (p : ℝ) * tailCollisionDefect A N p E D μ ν) ≤ C) :
    (∑ p : P, w p * ((p : ℝ) * ∑ x ∈ tailDensityMask A N p,
      (zmodResidueMass E μ p x - 1 / ((tailDensityMask A N p).card : ℝ)) ^ 2)) ≤ C / G := by
…

Mentions: OAI.Ostmann.tailResidues, OAI.Ostmann.negTailResidues, OAI.Ostmann.tailCollisionDefect, OAI.Ostmann.tailDensityMask, OAI.Ostmann.zmodResidueMass