RegularDiagonalCancellation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact cancellation of the diagonal regular-prime unit loss

The external integer giant is restricted to units. At a regular prime carrying a squared transform, its energy cancels that restriction exactly. At an outer compensation prime the factor left over is 1 - 1/p.

def OAI.Ostmann.externalRegularLocal line 17
theorem OAI.Ostmann.externalRegularLocal_sum_first line 23
theorem OAI.Ostmann.externalRegularLocal_average line 42

theorem OAI.Ostmann.crt_external_regular_cancellation line 62

Source documentation

This is the exact regular-prime integral in the diagonal environment, including the outer compensation slots which carry no transform.

theorem crt_external_regular_cancellation {I : Type*} [Fintype I] [DecidableEq I]
    (p : I → ℕ) [∀ i, Fact (p i).Prime] [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
    (hc : Pairwise (fun i j => (p i).Coprime (p j)))
    (active : I → Bool) (a : ∀ i, (ZMod (p i))ˣ) (g : ∀ i, ZMod (p i) → ℂ)
    (hg : ∀ i, g i 0 = 0) (henergy : ∀ i, (∑ x : ZMod (p i), ‖g i x‖ ^ 2) = p i) :
    (Fintype.card (ZMod (∏ i, p i) × (ZMod (∏ i, p i))ˣ) : ℝ)⁻¹ *
      (∑ z, ∏ i, externalRegularLocal (active i) (a i) (g i) (crtExternalPairEquiv p hc z i)) =
    ∏ i, if active i then 1 else 1 - (p i : ℝ)⁻¹ := by
…

Mentions: OAI.Ostmann.externalRegularLocal, OAI.Ostmann.crtExternalPairEquiv

theorem OAI.Ostmann.external_regular_cancellation_factor_le_one line 75