SparsePairEnergyBudget.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Combining the actual sparse pair kernel with its two energy budgets

theorem OAI.Ostmann.complementary_field_card_ratio line 12
theorem OAI.Ostmann.weighted_pair_square_bound line 33

theorem OAI.Ostmann.sparse_pair_average_energy_budget line 49

Source documentation

A single finite bound for the concrete sparse weight. The two energy bounds here are the quantities proved by restricted_lowMode_energy_budget. No norm of an untruncated tensor and no dimension factor appears.

theorem sparse_pair_average_energy_budget {n : ℕ}
    (p : Fin n → ℕ) [∀ i, Fact (p i).Prime]
    (S : ∀ i, Finset (ZMod (p i)))
    (hS : ∀ i, (S i).Nonempty) (hSp : ∀ i, (S i).card < p i)
    (hp : ∀ i, (100 : ℝ) ≤ p i)
    (hlo : ∀ i, (1 / 3 : ℝ) ≤ residueDensity (S i))
    (hhi : ∀ i, residueDensity (S i) ≤ 2 / 3)
    (ε : ℝ) (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 1000000)
    (hL1 : ∀ i, (p i : ℝ)⁻¹ * ∑ b, ‖normalizedResidueTransform (S i) b‖ ≤ ε ^ 2)
    (L : ℝ) (hL : 1 ≤ L) (hH : (∑ i, (p i : ℝ)⁻¹) ≤ L)
    (K : ℕ) (hK : 1000 * L ≤ K)
    {ι κ : Type*} (A : Finset ι) (B : Finset κ)
…

Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueTransform