SquarefreeMajorant.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The squarefree majorant in corrected dispersion

Only the positive variance term is majorized. The mixed and model terms retain their actual Möbius-square weights.

def OAI.CubicFirstMoment.truncatedSquareDivisorSum line 18
lemma OAI.CubicFirstMoment.truncatedSquareDivisorSum_eq_one line 21
theorem OAI.CubicFirstMoment.squarefree_le_truncated_majorant line 38
Source documentation
This majorizes the true squarefree indicator and is exactly one on squarefree elements. It applies to every truncation containing one.
```
theorem squarefree_le_truncated_majorant (C : Finset Eisenstein)
    (hC : ∀ c ∈ C, primary c) (h1 : 1 ∈ C) (a : Eisenstein) :
    (idealMoebius a : ℝ)^2 ≤ (truncatedSquareDivisorSum C a)^2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealMoebius, OAI.CubicFirstMoment.truncatedSquareDivisorSum
theorem OAI.CubicFirstMoment.truncatedSquareDivisorSum_sq line 49
Source documentation
Expansion before collecting pairs by their least common multiple.
```
theorem truncatedSquareDivisorSum_sq (C : Finset Eisenstein) (a : Eisenstein) :
    (truncatedSquareDivisorSum C a)^2 =
      ∑ c ∈ C, ∑ d ∈ C, (idealMoebius c : ℝ)*(idealMoebius d : ℝ)*
        (if c^2 ∣ a ∧ d^2 ∣ a then (1 : ℝ) else 0) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.truncatedSquareDivisorSum, OAI.CubicFirstMoment.idealMoebius
def OAI.CubicFirstMoment.squareDivisorTruncation line 62
Source documentation
The concrete norm truncation used by corrected dispersion.
```
def squareDivisorTruncation (D : ℝ) : Finset Eisenstein :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.squareDivisorTruncation_primary line 65
lemma OAI.CubicFirstMoment.one_mem_squareDivisorTruncation line 68

theorem OAI.CubicFirstMoment.corrected_squarefree_majorant line 75

Source documentation

The positive term alone is enlarged in the corrected square. The two remaining terms keep their original squarefree weights.

theorem corrected_squarefree_majorant (A C : Finset Eisenstein)
    (hC : ∀ c ∈ C, primary c) (h1 : 1 ∈ C)
    (W : Eisenstein → ℝ) (hW : ∀ a ∈ A, 0 ≤ W a)
    (F M : Eisenstein → ℂ) :
    (∑ a ∈ A, (idealMoebius a : ℝ)^2*W a*‖F a-M a‖^2) ≤
      (∑ a ∈ A, (truncatedSquareDivisorSum C a)^2*W a*‖F a‖^2) -
        2*(∑ a ∈ A, (idealMoebius a : ℝ)^2*W a*(star (F a)*M a).re) +
        ∑ a ∈ A, (idealMoebius a : ℝ)^2*W a*‖M a‖^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealMoebius, OAI.CubicFirstMoment.truncatedSquareDivisorSum