RegularInitialAmplitude.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The original initial Fourier amplitude and repeated-prime error

def OAI.Ostmann.primeTupleFourierCoefficient line 12
def OAI.Ostmann.regularInitialAmplitude line 20

theorem OAI.Ostmann.initial_physical_fourier_decomposition line 29

Source documentation

Before estimating anything, the retained Fourier amplitude and the discarded repeated tuples sum to the original physical statistic exactly.

theorem initial_physical_fourier_decomposition {n : ℕ}
    (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime)
    (μ : Fin n → P → ℝ) (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
    (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X) (N : ℕ)
    (w : (Fin n → P) → ℂ)
    (hcut : ∀ x, w x ≠ 0 → H * (∏ i, (x i : ℕ)) ≤ N * X)
    (hsupp : ∀ t : ℝ, H < |t| → 𝓕 ψ t = 0) :
    (∑ x : Fin n → P, (productPrior μ x : ℂ) * w x * physicalTupleSum P x F ψ X) =
      (Real.sqrt X : ℂ) * regularInitialAmplitude P μ F ψ X N w +
        ∑ x ∈ Finset.univ.filter (fun x : Fin n → P => ¬ Function.Injective x),
          (productPrior μ x : ℂ) * w x * physicalTupleSum P x F ψ X := by
…

Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.physicalTupleSum, OAI.Ostmann.regularInitialAmplitude

theorem OAI.Ostmann.regularInitialAmplitude_lower line 66

Source documentation

The positive statistic lower bound survives repeated-prime removal and becomes the lower bound on the actual finite initial Fourier amplitude.

theorem regularInitialAmplitude_lower {n : ℕ}
    (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime)
    (μ : Fin n → P → ℝ) (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
    (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X) (N : ℕ)
    (w : (Fin n → P) → ℂ)
    (hcut : ∀ x, w x ≠ 0 → H * (∏ i, (x i : ℕ)) ≤ N * X)
    (hsupp : ∀ t : ℝ, H < |t| → 𝓕 ψ t = 0)
    (δ ε : ℝ)
    (hpositive : Real.sqrt X * (δ + ε) ≤
      ‖∑ x : Fin n → P, (productPrior μ x : ℂ) * w x * physicalTupleSum P x F ψ X‖)
    (herror : ‖∑ x ∈ Finset.univ.filter (fun x : Fin n → P => ¬ Function.Injective x),
      (productPrior μ x : ℂ) * w x * physicalTupleSum P x F ψ X‖ ≤ Real.sqrt X * ε) :
…

Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.physicalTupleSum

theorem OAI.Ostmann.regularInitialAmplitude_lower_of_energy line 90

Source documentation

Normalized local energies suffice for the full repeated-prime removal. This form also applies directly to the two cons/append half-list families.

theorem regularInitialAmplitude_lower_of_energy {n : ℕ}
    (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime)
    (μ : Fin n → P → ℝ) (C : Fin n → ℝ)
    (hμ : ∀ i p, 0 ≤ μ i p) (hC : ∀ i, 0 ≤ C i)
    (hbound : ∀ i (p : P), (p : ℝ) * μ i p ≤ C i)
    (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
    (hzero : ∀ i q, (∑ a, F i q a) = 0)
    (henergy : ∀ i q, (∑ a, ‖F i q a‖ ^ 2) ≤ q)
    (ψ : 𝓢(ℝ, ℂ)) (X H R Δ δ : ℝ) (hX : 0 < X) (hR : 0 < R) (N : ℕ)
    (w : (Fin n → P) → ℂ) (hw : ∀ x, ‖w x‖ ≤ 1)
    (hcut : ∀ x, w x ≠ 0 → H * (∏ i, (x i : ℕ)) ≤ N * X)
    (hsupp : ∀ t : ℝ, H < |t| → 𝓕 ψ t = 0)
…

theorem OAI.Ostmann.regularInitialAmplitude_lower_of_prime_tests line 132

Source documentation

For the actual residue and phase tests, the repeated-prime error is derived from their energies and the original marginal bounds. The only statistic lower bound here is the one supplied by the endpoint construction.

theorem regularInitialAmplitude_lower_of_prime_tests {n : ℕ}
    (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime)
    (μ : Fin n → P → ℝ) (C : Fin n → ℝ)
    (hμ : ∀ i p, 0 ≤ μ i p) (hC : ∀ i, 0 ≤ C i)
    (hbound : ∀ i (p : P), (p : ℝ) * μ i p ≤ C i)
    (S : (q : P) → Finset (ZMod (q : ℕ))) (giant : Fin n → Bool) (favorable : P → Bool)
    (ψ : 𝓢(ℝ, ℂ)) (X H R Δ δ : ℝ) (hX : 0 < X) (hR : 0 < R) (N : ℕ)
    (w : (Fin n → P) → ℂ) (hw : ∀ x, ‖w x‖ ≤ 1)
    (hcut : ∀ x, w x ≠ 0 → H * (∏ i, (x i : ℕ)) ≤ N * X)
    (hsupp : ∀ t : ℝ, H < |t| → 𝓕 ψ t = 0)
    (hsmall : ∀ p : P, H * R < (p : ℝ))
    (hlower : ∀ x, w x ≠ 0 → X * Real.exp Δ ≤ ∏ i, (x i : ℝ))
…