HarmonicBlockRecombination.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Recombining the dyadic pieces of an original harmonic prime prior

theorem OAI.Ostmann.harmonic_raw_of_mean_bound line 12

theorem OAI.Ostmann.harmonic_partition_bound line 29

Source documentation

The cost is the number of dyadic pieces, while the normalizer is the original total harmonic mass. No lower bound for an individual piece is used.

theorem harmonic_partition_bound {I : Type*} [Fintype I]
    (P : Finset ℕ) (key : ℕ → I) (F : ℕ → ℂ) (C : ℝ)
    (hm : 0 < ∑ p ∈ P, (p : ℝ)⁻¹)
    (hlocal : ∀ i, ‖∑ p ∈ P.filter (fun p => key p = i), ((p : ℝ)⁻¹ : ℂ) * F p‖ ^ 2 ≤
      (∑ p ∈ P.filter (fun p => key p = i), (p : ℝ)⁻¹) * C) :
    ‖∑ p : P, (primeSubsetPrior P P p : ℂ) * F p‖ ^ 2 ≤
      (Fintype.card I : ℝ) * (∑ p ∈ P, (p : ℝ)⁻¹)⁻¹ * C := by
…

Mentions: OAI.Ostmann.primeSubsetPrior