HarmonicPriorCost.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The precise cost of replacing original bulk primes by unit residues

theorem OAI.Ostmann.harmonic_prior_product_cost line 11

theorem OAI.Ostmann.harmonic_prior_product_cost_linear line 35

Source documentation

Once L is at least one, the prior loss has an absolute coefficient per leaf, independent of the transfer depth.

theorem harmonic_prior_product_cost_linear (n : ℕ) (S : TreeLeafIndex n → Finset ℕ)
    (J : TreeLeafIndex n → ℕ) (a C L : ℝ) (ha : 0 < a) (hL : 1 ≤ L)
    (hmass : ∀ i, a ≤ ∑ p ∈ S i, (p : ℝ)⁻¹)
    (hJ : ∀ i, (J i : ℝ) ≤ Real.exp (C * L)) :
    (∏ i, (∑ p ∈ S i, (p : ℝ)⁻¹)⁻¹ * (3 * J i)) ≤
      Real.exp ((C + max (Real.log (3 / a)) 0) * (2 ^ n : ℕ) * L) := by
…

Mentions: OAI.Ostmann.TreeLeafIndex