PhaseCollision.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EuclideanFiveColor.PhaseCollision.repeatedPairs line 26
Source documentation
Ordered distinct pairs in one assigned bin.
```
def repeatedPairs (s : Finset ι) (f : ι → κ) : Finset (ι × ι) := by
…
```
lemma OAI.EuclideanFiveColor.PhaseCollision.sameBin_card line 31
lemma OAI.EuclideanFiveColor.PhaseCollision.sameBin_card_eq line 48
theorem OAI.EuclideanFiveColor.PhaseCollision.repeated_bin_lower_bound line 68
def OAI.EuclideanFiveColor.PhaseCollision.closePairs line 87
Source documentation
Ordered distinct phase pairs within a fixed distance.
```
def closePairs (v : ι → V) (r : ℝ) : Finset (ι × ι) := by
…
```
theorem OAI.EuclideanFiveColor.PhaseCollision.close_pair_lower_bound line 91

theorem OAI.EuclideanFiveColor.PhaseCollision.normalized_close_pair_lower_bound line 119

Source documentation

The normalized source estimate q² / #bins - 1/#indices.

theorem normalized_close_pair_lower_bound [Nonempty ι] [Nonempty κ]
    (s : Finset ι) (f : ι → κ) (v : ι → V) (w : κ → V) (r : ℝ)
    (h : ∀ i ∈ s, dist (v i) (w (f i)) ≤ r) :
    ((s.card : ℝ) / Fintype.card ι) ^ 2 / Fintype.card κ - 1 / Fintype.card ι ≤
      (closePairs v (2 * r)).card / (Fintype.card ι : ℝ) ^ 2 := by
…

Mentions: OAI.EuclideanFiveColor.PhaseCollision.closePairs

theorem OAI.EuclideanFiveColor.PhaseCollision.average_cover_forces_collision line 142

Source documentation

Larger than 95 percent average phase coverage forces a colliding pair. The bins and assignments may depend on the sampled point; no measurable choice of assignments is required.

theorem average_cover_forces_collision (μ : Measure Ω) [IsProbabilityMeasure μ]
    (s : Ω → Finset ι) (f : Ω → ι → κ) (v : Ω → ι → V) (w : Ω → κ → V)
    (r : ℝ)
    (hcov : ∀ᵐ x ∂μ, ∀ i ∈ s x, dist (v x i) (w x (f x i)) ≤ r)
    (hm : ∀ i j, Measurable (fun x => dist (v x i) (v x j)))
    (hq : Measurable (fun x => ((s x).card : ℝ) / Fintype.card ι))
    (hlarge : 10 * Fintype.card κ < Fintype.card ι)
    (havg : (19/20 : ℝ) < ∫ x, ((s x).card : ℝ) / Fintype.card ι ∂μ) :
    ∃ i j : ι, i ≠ j ∧
      1 / (4 * (Fintype.card κ : ℝ)) ≤ μ.real {x | dist (v x i) (v x j) ≤ 2*r} := by
…

def OAI.EuclideanFiveColor.AverageErrors.goodFraction line 259
Source documentation
The fraction of indices whose nonnegative error is below a threshold.
```
def goodFraction (e : ι → Ω → ℝ) (t : ℝ) (x : Ω) : ℝ := by
…
```
lemma OAI.EuclideanFiveColor.AverageErrors.goodFraction_eq_sum line 264
lemma OAI.EuclideanFiveColor.AverageErrors.measurable_goodFraction line 270
lemma OAI.EuclideanFiveColor.AverageErrors.goodFraction_nonneg line 279
lemma OAI.EuclideanFiveColor.AverageErrors.goodFraction_le_one line 283
lemma OAI.EuclideanFiveColor.AverageErrors.integrable_goodFraction line 289

theorem OAI.EuclideanFiveColor.AverageErrors.average_goodFraction line 298

Source documentation

Less than 5% average error gives more than 95% good indices on average.

theorem average_goodFraction (μ : Measure Ω) [IsProbabilityMeasure μ]
    (e : ι → Ω → ℝ) (t : ℝ) (ht : 0 < t)
    (he : ∀ i, Measurable (e i)) (hi : ∀ i, Integrable (e i) μ)
    (hn : ∀ᵐ x ∂μ, ∀ i, 0 ≤ e i x)
    (havg : ∀ i, ∫ x, e i x ∂μ < t/20) :
    (19/20 : ℝ) < ∫ x, goodFraction e t x ∂μ := by
…

Mentions: OAI.EuclideanFiveColor.AverageErrors.goodFraction

theorem OAI.EuclideanFiveColor.PhaseCollision.average_exists_cover_forces_collision line 352

Source documentation

The assignment itself need not be measurable and may be chosen separately at every sample. Only the phase distances and fraction are measured.

theorem average_exists_cover_forces_collision (μ : Measure Ω) [IsProbabilityMeasure μ]
    (s : Ω → Finset ι) (v : Ω → ι → V) (w : Ω → κ → V) (r : ℝ)
    (hcov : ∀ᵐ x ∂μ, ∀ i ∈ s x, ∃ j, dist (v x i) (w x j) ≤ r)
    (hm : ∀ i j, Measurable (fun x => dist (v x i) (v x j)))
    (hq : Measurable (fun x => ((s x).card : ℝ) / Fintype.card ι))
    (hlarge : 10 * Fintype.card κ < Fintype.card ι)
    (havg : (19/20 : ℝ) < ∫ x, ((s x).card : ℝ) / Fintype.card ι ∂μ) :
    ∃ i j : ι, i ≠ j ∧
      1 / (4 * (Fintype.card κ : ℝ)) ≤ μ.real {x | dist (v x i) (v x j) ≤ 2*r} := by
…

lemma OAI.EuclideanFiveColor.PhaseCollision.circle_product_dist line 373

theorem OAI.EuclideanFiveColor.EncodedCollision.collision_from_close_encodings line 396

Source documentation

This is the source's collision contradiction on one selected predecessor fiber. The lists need not be measurably enumerated. Measurability is required only of their symmetric encodings and the actual sampled phases.

theorem collision_from_close_encodings (μ : Measure Ω) [IsProbabilityMeasure μ]
    (m : ℕ) (hm : 0 < m) (ρ : ℝ) (hρ : 0 < ρ)
    (zp zm : Ω → ι → Fin m → Circle) (ap am : ι → Ω → Circle) (j₀ : ι)
    (hap : ∀ j, Measurable (ap j)) (ham : ∀ j, Measurable (am j))
    (hDp : ∀ j, Measurable (fun x => dist (encoding (zp x j)) (encoding (zp x j₀))))
    (hDm : ∀ j, Measurable (fun x => dist (encoding (zm x j)) (encoding (zm x j₀))))
    (hmem : ∀ᵐ x ∂μ, ∀ j, (∃ r, ap j x = zp x j r) ∧ (∃ r, am j x = zm x j r))
    (hi : ∀ j, Integrable (fun x =>
       dist (encoding (zp x j)) (encoding (zp x j₀))^2 +
       dist (encoding (zm x j)) (encoding (zm x j₀))^2) μ)
    (he : ∀ j, (∫ x,
       dist (encoding (zp x j)) (encoding (zp x j₀))^2 +
…

theorem OAI.EuclideanFiveColor.EncodedCollision.collision_from_measurable_encodings line 463

Source documentation

theorem collision_from_measurable_encodings (μ : Measure Ω) [IsProbabilityMeasure μ]
    (m : ℕ) (hm : 0 < m) (ρ : ℝ) (hρ : 0 < ρ)
    (zp zm : Ω → ι → Fin m → Circle) (ap am : ι → Ω → Circle) (j₀ : ι)
    (Hp Hm : ι → Ω → Fin m → ℂ)
    (henc : ∀ᵐ x ∂μ, ∀ j, encoding (zp x j) = Hp j x ∧ encoding (zm x j) = Hm j x)
    (hap : ∀ j, Measurable (ap j)) (ham : ∀ j, Measurable (am j))
    (hDp : ∀ j, Measurable (fun x => dist (Hp j x) (Hp j₀ x)))
    (hDm : ∀ j, Measurable (fun x => dist (Hm j x) (Hm j₀ x)))
    (hmem : ∀ᵐ x ∂μ, ∀ j, (∃ r, ap j x = zp x j r) ∧ (∃ r, am j x = zm x j r))
    (hi : ∀ j, Integrable (fun x =>
       dist (Hp j x) (Hp j₀ x)^2 +
       dist (Hm j x) (Hm j₀ x)^2) μ)
…