PageFactors.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Keeping the exceptional-character density in the arithmetic measures

The correction is retained, including when it correlates with the amplitude. Once its conductor is supported on the frequency modulus, CRT places it in that coordinate and the other residue averages factor exactly.

def OAI.Ostmann.pageMultiplier line 18
theorem OAI.Ostmann.pageMultiplier_bounds line 21
theorem OAI.Ostmann.pageMultiplier_zero line 33

theorem OAI.Ostmann.page_prior_mass_le_two line 38

Source documentation

The corrected coordinate prior has mass at most two, even if its exceptional character has nonzero mean under the original prior.

theorem page_prior_mass_le_two {A : Type*} [Fintype A]
    (μ : A → ℝ) (hμ : ∀ a, 0 ≤ μ a) (hmass : ∑ a, μ a ≤ 1)
    (χ : A → ℝ) (β t : ℝ) (hχ : ∀ a, |χ a| ≤ 1) (hβ : β ≤ 1) (ht : 0 ≤ t) :
    (∀ a, 0 ≤ μ a * pageMultiplier χ β t a) ∧
      (∑ a, μ a * pageMultiplier χ β t a) ≤ 2 := by
…

Mentions: OAI.Ostmann.pageMultiplier

theorem OAI.Ostmann.uniform_equiv_product_average line 54

Source documentation

Exact separation of a retained density and all remaining coordinates. This also applies to signed and complex amplitudes.

theorem uniform_equiv_product_average {A B C : Type*}
    [Fintype A] [Fintype B] [Fintype C]
    (e : A ≃ B × C) (f : B → ℂ) (g : C → ℂ) :
    (Fintype.card A : ℂ)⁻¹ * (∑ a, f (e a).1 * g (e a).2) =
      ((Fintype.card B : ℂ)⁻¹ * ∑ b, f b) *
        ((Fintype.card C : ℂ)⁻¹ * ∑ c, g c) := by
…

theorem OAI.Ostmann.retained_page_average line 68

Source documentation

In the finite box decomposition, the Page factor remains inside the frequency-coordinate integral; it is never replaced by its mean.

theorem retained_page_average {A B C : Type*}
    [Fintype A] [Fintype B] [Fintype C]
    (e : A ≃ B × C) (χ : B → ℝ) (β t : ℝ) (f : B → ℂ) (g : C → ℂ) :
    (Fintype.card A : ℂ)⁻¹ *
        (∑ a, (pageMultiplier χ β t (e a).1 : ℂ) * f (e a).1 * g (e a).2) =
      ((Fintype.card B : ℂ)⁻¹ * ∑ b, (pageMultiplier χ β t b : ℂ) * f b) *
        ((Fintype.card C : ℂ)⁻¹ * ∑ c, g c) :=
…

Mentions: OAI.Ostmann.pageMultiplier

def OAI.Ostmann.crtSplitUnitEquiv line 79
Source documentation
The retained frequency block and all other unit residues in the actual modulus.
```
noncomputable def crtSplitUnitEquiv (q r : ℕ) (h : q.Coprime r) :
    (ZMod (q * r))ˣ ≃ (ZMod q)ˣ × (ZMod r)ˣ :=
…
```
theorem OAI.Ostmann.crt_retained_page_average line 84