Projection.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Residue projection of finite probability measures

These identities connect the pair count in WeightedCollision with the collision norm of a projected measure, as used in Lemma 2.5 of the paper.

def OAI.Ostmann.fiberMass line 17

Source documentation

Mass of a fiber of a map, for a measure supported on a finite set.

noncomputable def fiberMass {α β : Type*} [DecidableEq β]
    (s : Finset α) (μ : α → ℝ) (f : α → β) (y : β) : ℝ :=
…

theorem OAI.Ostmann.sum_fiberMass_mul line 21
theorem OAI.Ostmann.sum_fiberMass line 35
theorem OAI.Ostmann.sum_fiberMass_sq line 41
def OAI.Ostmann.residueMass line 57
Source documentation
The probability mass function obtained by reduction modulo p.
```
noncomputable def residueMass (s : Finset ℕ) (μ : ℕ → ℝ) (p r : ℕ) : ℝ :=
…
```
theorem OAI.Ostmann.residueMass_total line 60
theorem OAI.Ostmann.residueMass_sq line 66

theorem OAI.Ostmann.weighted_residueMass_sq line 74

Source documentation

Reorder the weighted residue collisions as a sum over integer pairs.

theorem weighted_residueMass_sq (P s : Finset ℕ) (μ : ℕ → ℝ)
    (hP : ∀ p ∈ P, p.Prime) :
    (∑ p ∈ P, Real.log (p : ℝ) *
      ∑ r ∈ Finset.range p, (residueMass s μ p r) ^ 2) =
    ∑ a ∈ s, ∑ b ∈ s, μ a * μ b * primeCollisionWeight P a b := by
…

Mentions: OAI.Ostmann.residueMass, OAI.Ostmann.primeCollisionWeight

theorem OAI.Ostmann.residue_collision_bound line 104

Source documentation

The quantitative weighted collision bound for projected probabilities.

theorem residue_collision_bound (P s : Finset ℕ) (μ : ℕ → ℝ) (X : ℕ) (m : ℝ)
    (hX : 1 ≤ X) (hP : ∀ p ∈ P, p.Prime)
    (hs : ∀ a ∈ s, a ≤ X) (hμ : ∀ a ∈ s, 0 ≤ μ a)
    (hmass : ∑ a ∈ s, μ a = 1) (hatom : ∀ a ∈ s, μ a ≤ m) :
    (∑ p ∈ P, Real.log (p : ℝ) *
      ∑ r ∈ Finset.range p, (residueMass s μ p r) ^ 2) ≤
      Real.log (X : ℝ) + m * ∑ p ∈ P, Real.log (p : ℝ) := by
…

Mentions: OAI.Ostmann.residueMass

theorem OAI.Ostmann.residue_collision_bound_of_diameter line 115

Source documentation

The projected bound for a translated interval uses only its diameter.

theorem residue_collision_bound_of_diameter (P s : Finset ℕ) (μ : ℕ → ℝ)
    (X : ℕ) (m : ℝ) (hX : 1 ≤ X) (hP : ∀ p ∈ P, p.Prime)
    (hD : ∀ a ∈ s, ∀ b ∈ s, Nat.dist a b ≤ X) (hμ : ∀ a ∈ s, 0 ≤ μ a)
    (hmass : ∑ a ∈ s, μ a = 1) (hatom : ∀ a ∈ s, μ a ≤ m) :
    (∑ p ∈ P, Real.log (p : ℝ) *
      ∑ r ∈ Finset.range p, (residueMass s μ p r) ^ 2) ≤
      Real.log (X : ℝ) + m * ∑ p ∈ P, Real.log (p : ℝ) := by
…

Mentions: OAI.Ostmann.residueMass

theorem OAI.Ostmann.fiberMass_sq_eq_residueMass_sq line 127

Source documentation

Residue labels may be changed (in particular, negated) without changing the collision norm, provided they identify exactly the congruent pairs.

theorem fiberMass_sq_eq_residueMass_sq (s t : Finset ℕ) (μ : ℕ → ℝ)
    (f : ℕ → ℕ) {p : ℕ} (hp : 0 < p)
    (hf : ∀ a ∈ s, f a ∈ t)
    (hcongr : ∀ a ∈ s, ∀ b ∈ s, f a = f b ↔ a ≡ b [MOD p]) :
    (∑ r ∈ t, (fiberMass s μ f r) ^ 2) =
      ∑ r ∈ Finset.range p, (residueMass s μ p r) ^ 2 := by
…

Mentions: OAI.Ostmann.fiberMass, OAI.Ostmann.residueMass

theorem OAI.Ostmann.fiber_collision_bound line 142

Source documentation

The weighted pair bound applies on any chosen residue support, including the negative residue support of the second summand.

theorem fiber_collision_bound (P s : Finset ℕ) (μ : ℕ → ℝ)
    (t : ℕ → Finset ℕ) (f : ℕ → ℕ → ℕ) (X : ℕ) (m : ℝ)
    (hX : 1 ≤ X) (hP : ∀ p ∈ P, p.Prime)
    (hs : ∀ a ∈ s, a ≤ X) (hμ : ∀ a ∈ s, 0 ≤ μ a)
    (hmass : ∑ a ∈ s, μ a = 1) (hatom : ∀ a ∈ s, μ a ≤ m)
    (hf : ∀ p ∈ P, ∀ a ∈ s, f p a ∈ t p)
    (hcongr : ∀ p ∈ P, ∀ a ∈ s, ∀ b ∈ s, f p a = f p b ↔ a ≡ b [MOD p]) :
    (∑ p ∈ P, Real.log (p : ℝ) *
      ∑ r ∈ t p, (fiberMass s μ (f p) r) ^ 2) ≤
      Real.log (X : ℝ) + m * ∑ p ∈ P, Real.log (p : ℝ) := by
…

Mentions: OAI.Ostmann.fiberMass