OAI/NumberTheory/Ostmann/Construction/RepeatedPhysicalTests.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.localTest_bound_of_energy line 14

   Source documentation

   The physical giant need not be bounded by one; its normalized energy still gives the exact square-root bound needed for repeated factors.

   theorem localTest_bound_of_energy {q : ℕ} [NeZero q] (F : ZMod q → ℂ)
       (hF : ∑ x, ‖F x‖ ^ 2 ≤ (q : ℝ)) (x : ZMod q) :
       ‖F x‖ ≤ Real.sqrt q := by
   …

2. theorem OAI.Ostmann.sum_norm_product_le_sqrt_pow line 22

   Source documentation

   Two repeated factors use Cauchy; all remaining factors use the square-root bound. The local tests may belong to different roles.

   theorem sum_norm_product_le_sqrt_pow {I : Type*} {q : ℕ} [NeZero q]
       (S : Finset I) (F : I → ZMod q → ℂ) (hS : 2 ≤ S.card)
       (hF : ∀ i ∈ S, ∑ x, ‖F i x‖ ^ 2 ≤ (q : ℝ)) :
       (∑ x : ZMod q, ‖∏ i ∈ S, F i x‖) ≤ (Real.sqrt q) ^ S.card := by
   …

3. theorem OAI.Ostmann.product_complete_mean_norm_le line 62
4. def OAI.Ostmann.groupedPhysicalTest line 73
5. theorem OAI.Ostmann.groupedPhysicalTest_product line 78
6. theorem OAI.Ostmann.groupedPhysicalTest_singleton line 92
7. def OAI.Ostmann.physicalTupleSum line 105

   Source documentation

   Grouping at each distinct prime preserves the original physical product, including when a prime occurs in several different roles.

   noncomputable def physicalTupleSum {I : Type*} [Fintype I]
       (P : Finset ℕ) (p : I → P) (F : I → (q : P) → ZMod (q : ℕ) → ℂ)
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) : ℂ :=
   …

8. theorem OAI.Ostmann.physicalTupleSum_singleton_zero line 112

   Source documentation

   A single occurrence of a mean-zero test annihilates the entire short- period sum, without any character assumption.

   theorem physicalTupleSum_singleton_zero {I : Type*} [Fintype I]
       (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime) (p : I → P)
       (F : I → (q : P) → ZMod (q : ℕ) → ℂ)
       (i : I) (hi : ∀ j, p j = p i → j = i) (hmean : ∑ x, F i (p i) x = 0)
       (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X)
       (hperiod : H < X / (∏ q : P, (q : ℕ)))
       (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) :
       physicalTupleSum P p F ψ X = 0 := by
   …

   Mentions: OAI.Ostmann.physicalTupleSum

9. theorem OAI.Ostmann.groupedPhysicalTest_sqrt_product line 138
10. theorem OAI.Ostmann.physicalTupleSum_multiple_bound line 153

    Source documentation

    The repeated tuple estimate needed in Section 7.3. Its dependence on the product counted with multiplicity is exact.

    theorem physicalTupleSum_multiple_bound {I : Type*} [Fintype I]
        (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime) (p : I → P)
        (F : I → (q : P) → ZMod (q : ℕ) → ℂ)
        (hmultiple : ∀ q : P, 2 ≤ (Finset.univ.filter (fun i => p i = q)).card)
        (henergy : ∀ i, ∑ x, ‖F i (p i) x‖ ^ 2 ≤ (p i : ℝ))
        (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X)
        (hperiod : H < X / (∏ q : P, (q : ℕ)))
        (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) :
        ‖physicalTupleSum P p F ψ X‖ ≤
          X * ‖𝓕 ψ 0‖ * (Real.sqrt (∏ i, (p i : ℝ)) / ∏ q : P, (q : ℝ)) := by
    …

    Mentions: OAI.Ostmann.physicalTupleSum

11. theorem OAI.Ostmann.physicalTupleSum_short_period_bound line 194

    Source documentation

    Either every used prime occurs twice, or a singleton mean-zero test makes the complete residue mean vanish. This is the uniform short-period bound before any summation over repeated tuples.

    theorem physicalTupleSum_short_period_bound {I : Type*} [Fintype I]
        (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)]
        (hP : ∀ q ∈ P, q.Prime) (p : I → P) (hp : Function.Surjective p)
        (F : I → (q : P) → ZMod (q : ℕ) → ℂ)
        (hmean : ∀ i, ∑ x, F i (p i) x = 0)
        (henergy : ∀ i, ∑ x, ‖F i (p i) x‖ ^ 2 ≤ (p i : ℝ))
        (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X)
        (hperiod : H < X / (∏ q : P, (q : ℕ)))
        (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) :
        ‖physicalTupleSum P p F ψ X‖ ≤
          X * ‖𝓕 ψ 0‖ * (Real.sqrt (∏ i, (p i : ℝ)) / ∏ q : P, (q : ℝ)) := by
    …

    Mentions: OAI.Ostmann.physicalTupleSum

12. theorem OAI.Ostmann.physicalTupleSum_repeated_bound line 222

    Source documentation

    Repeating one prime makes the true period short at the initial product scale. The resulting bound uses the actual physical tests throughout.

    theorem physicalTupleSum_repeated_bound {I : Type*} [Fintype I]
        (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)]
        (hP : ∀ q ∈ P, q.Prime) (p : I → P) (hp : Function.Surjective p)
        (F : I → (q : P) → ZMod (q : ℕ) → ℂ)
        (hmean : ∀ i, ∑ x, F i (p i) x = 0)
        (henergy : ∀ i, ∑ x, ‖F i (p i) x‖ ^ 2 ≤ (p i : ℝ))
        (ψ : 𝓢(ℝ, ℂ)) (X H R : ℝ) (hX : 0 < X) (hR : 0 < R)
        (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0)
        (hsmall : ∀ i, H * R < (p i : ℝ)) (hprod : (∏ i, (p i : ℝ)) ≤ X * R)
        (i j : I) (hij : i ≠ j) (heq : p i = p j) :
        ‖physicalTupleSum P p F ψ X‖ ≤
          X * ‖𝓕 ψ 0‖ * (Real.sqrt (∏ i, (p i : ℝ)) / ∏ q : P, (q : ℝ)) := by
    …

    Mentions: OAI.Ostmann.physicalTupleSum

13. theorem OAI.Ostmann.physicalTupleSum_repeated_bound_used line 254

    Source documentation

    The ambient prime set may contain unused values. Restricting to the actual image gives the true squarefree period and leaves every test unchanged.

    theorem physicalTupleSum_repeated_bound_used {I : Type*} [Fintype I]
        (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)]
        (hP : ∀ q ∈ P, q.Prime) (p : I → P)
        (F : I → (q : P) → ZMod (q : ℕ) → ℂ)
        (hmean : ∀ i, ∑ x, F i (p i) x = 0)
        (henergy : ∀ i, ∑ x, ‖F i (p i) x‖ ^ 2 ≤ (p i : ℝ))
        (ψ : 𝓢(ℝ, ℂ)) (X H R : ℝ) (hX : 0 < X) (hR : 0 < R)
        (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0)
        (hsmall : ∀ i, H * R < (p i : ℝ)) (hprod : (∏ i, (p i : ℝ)) ≤ X * R)
        (i j : I) (hij : i ≠ j) (heq : p i = p j) :
        ‖physicalTupleSum P p F ψ X‖ ≤
          X * ‖𝓕 ψ 0‖ * (Real.sqrt (∏ i, (p i : ℝ)) /
    …

    Mentions: OAI.Ostmann.physicalTupleSum