PhaseGiantCollision.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Collision control for the unbounded physical giant test

theorem OAI.Ostmann.phaseGiantPhysical_empirical_error line 13

Source documentation

The pointwise inverse bound grows with the prime; the empirical error uses its counting energy instead and loses exactly one factor of the modulus.

theorem phaseGiantPhysical_empirical_error {p : ℕ} [NeZero p]
    (S : Finset (ZMod p)) (μ : ZMod p → ℝ) (g : ZMod p → ℂ) :
    ‖(∑ x ∈ S, (μ x : ℂ) * phaseGiantPhysical g x) -
      (S.card : ℂ)⁻¹ * ∑ x ∈ S, phaseGiantPhysical g x‖ ^ 2 ≤
        (p : ℝ) * ∑ x ∈ S, (μ x - 1 / (S.card : ℝ)) ^ 2 := by
…

Mentions: OAI.Ostmann.phaseGiantPhysical

theorem OAI.Ostmann.phaseGiant_weighted_empirical_error line 29

Source documentation

Weighted Cauchy gives the square-root error in Section 7.1 directly from the collision budget. No pointwise bound on the inverse transform is used.

theorem phaseGiant_weighted_empirical_error {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, NeZero (p i)]
    (S : ∀ i, Finset (ZMod (p i))) (μ : ∀ i, ZMod (p i) → ℝ)
    (g : ∀ i, ZMod (p i) → ℂ) (w : I → ℝ) (hw : ∀ i, 0 ≤ w i)
    (B : ℝ)
    (hbudget : (∑ i, w i * ((p i : ℝ) *
      ∑ x ∈ S i, (μ i x - 1 / ((S i).card : ℝ)) ^ 2)) ≤ B) :
    ‖∑ i, (w i : ℂ) * ((∑ x ∈ S i, (μ i x : ℂ) * phaseGiantPhysical (g i) x) -
      ((S i).card : ℂ)⁻¹ * ∑ x ∈ S i, phaseGiantPhysical (g i) x)‖ ≤
      Real.sqrt (∑ i, w i) * Real.sqrt B := by
…

Mentions: OAI.Ostmann.phaseGiantPhysical

theorem OAI.Ostmann.phaseGiant_weighted_empirical_mean_lower line 59

Source documentation

The complex collision estimate implies the required lower bound for the real empirical mean before the soft-cell pigeonhole.

theorem phaseGiant_weighted_empirical_mean_lower {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, NeZero (p i)]
    (S : ∀ i, Finset (ZMod (p i))) (μ : ∀ i, ZMod (p i) → ℝ)
    (g : ∀ i, ZMod (p i) → ℂ) (w : I → ℝ) (hw : ∀ i, 0 ≤ w i)
    (B : ℝ)
    (hbudget : (∑ i, w i * ((p i : ℝ) *
      ∑ x ∈ S i, (μ i x - 1 / ((S i).card : ℝ)) ^ 2)) ≤ B) :
    (∑ i, w i * (((S i).card : ℝ)⁻¹ *
      ∑ x ∈ S i, (phaseGiantPhysical (g i) x).re)) -
        Real.sqrt (∑ i, w i) * Real.sqrt B ≤
      ∑ i, w i * ∑ x ∈ S i, μ i x * (phaseGiantPhysical (g i) x).re := by
…

Mentions: OAI.Ostmann.phaseGiantPhysical