MaskedPhaseGiantMean.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The favorable-prime mask in the initial giant

Nonfavorable primes remain in the prior. Their physical test is exactly zero.

theorem OAI.Ostmann.phaseGiantPhysical_zero line 13
def OAI.Ostmann.favorablePhaseTransform line 17
theorem OAI.Ostmann.favorablePhaseTransform_real line 22

theorem OAI.Ostmann.favorablePhase_uniform_mean_lower line 34

Source documentation

The favorable Fourier L1 mass gives a positive uniform-support mean, while the other primes make zero contribution.

theorem favorablePhase_uniform_mean_lower {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, Fact (p i).Prime] (S : ∀ i, Finset (ZMod (p i)))
    (F : Finset I) (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) (γ : ℝ)
    (hS : ∀ i ∈ F, (S i).Nonempty) (hSp : ∀ i ∈ F, (S i).card < p i)
    (hσ : ∀ i ∈ F, residueDensity (S i) ≤ 2 / 3)
    (hγ : ∀ i ∈ F, γ ≤ (p i : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform (S i) b‖) :
    (γ / 2) * (∑ i ∈ F, w i) ≤
      ∑ i, w i * (((S i).card : ℝ)⁻¹ *
        ∑ x ∈ S i, (phaseGiantPhysical (favorablePhaseTransform p S F i) x).re) := by
…

Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.phaseGiantPhysical, OAI.Ostmann.favorablePhaseTransform

theorem OAI.Ostmann.favorablePhase_empirical_mean_lower line 59

Source documentation

The initial empirical mean, with the genuine Fourier phase mask, pays only the square-root collision loss from Section 7.1.

theorem favorablePhase_empirical_mean_lower {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, Fact (p i).Prime] (S : ∀ i, Finset (ZMod (p i)))
    (F : Finset I) (μ : ∀ i, ZMod (p i) → ℝ)
    (w : I → ℝ) (hw : ∀ i, 0 ≤ w i) (γ B : ℝ)
    (hS : ∀ i ∈ F, (S i).Nonempty) (hSp : ∀ i ∈ F, (S i).card < p i)
    (hσ : ∀ i ∈ F, residueDensity (S i) ≤ 2 / 3)
    (hγ : ∀ i ∈ F, γ ≤ (p i : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform (S i) b‖)
    (hbudget : (∑ i, w i * ((p i : ℝ) *
      ∑ x ∈ S i, (μ i x - 1 / ((S i).card : ℝ)) ^ 2)) ≤ B) :
    (γ / 2) * (∑ i ∈ F, w i) - Real.sqrt (∑ i, w i) * Real.sqrt B ≤
      ∑ i, w i * ∑ x ∈ S i, μ i x *
        (phaseGiantPhysical (favorablePhaseTransform p S F i) x).re := by
…

Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueTransform, OAI.Ostmann.phaseGiantPhysical, OAI.Ostmann.favorablePhaseTransform