HarmonicProductDomination.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Original independent harmonic priors on the leaves of a transfer tree

theorem OAI.Ostmann.product_cellPrior_indexed line 12
theorem OAI.Ostmann.indexed_cell_expectation_eq line 33

theorem OAI.Ostmann.indexed_cell_expectation_le line 46

Source documentation

A pointwise upper bound for each residue class yields the product of exactly one loss for each independently sampled leaf.

theorem indexed_cell_expectation_le {I A B : Type*}
    [Fintype I] [DecidableEq I] [Fintype A] [Fintype B]
    (μ : I → A → ℝ) (cell : I → A → B) (C : I → ℝ)
    (hμ : ∀ i a, 0 ≤ μ i a)
    (hcell : ∀ i b, cellPrior (μ i) (cell i) b ≤ C i * (Fintype.card B : ℝ)⁻¹)
    (F : (I → B) → ℝ) (hF : ∀ y, 0 ≤ F y) :
    (∑ x : I → A, (∏ i, μ i (x i)) * F (fun i => cell i (x i))) ≤
      (∏ i, C i) * ((Fintype.card (I → B) : ℝ)⁻¹ * ∑ y : I → B, F y) := by
…

Mentions: OAI.Ostmann.cellPrior

theorem OAI.Ostmann.harmonic_leaf_residue_domination line 72

Source documentation

This uses each leaf's actual harmonic subset, with all boundary primes retained, and produces the original uniform-unit tree average.

theorem harmonic_leaf_residue_domination (P : Finset ℕ) (q n : ℕ) [NeZero q]
    (S : TreeLeafIndex n → Finset ℕ) (h J : TreeLeafIndex n → ℕ)
    (hunit : ∀ p : P, (p : ℕ).Coprime q)
    (hsmall : ∀ i, q ≤ 2 ^ h i)
    (hrange : ∀ i p, p ∈ S i → 2 ^ h i ≤ p ∧ p < 2 ^ (h i + J i))
    (F : TreeLeafTuple (ZMod q)ˣ n → ℝ) (hF : ∀ x, 0 ≤ F x) :
    (∑ x : TreeLeafIndex n → P, (∏ i, primeSubsetPrior P (S i) (x i)) *
      F ((treeLeafTupleEquiv (ZMod q)ˣ n).symm
        (fun i => ZMod.unitOfCoprime (x i : ℕ) (hunit (x i))))) ≤
      (∏ i, (∑ p ∈ S i, (p : ℝ)⁻¹)⁻¹ * (3 * J i)) *
        ((Fintype.card (TreeLeafTuple (ZMod q)ˣ n) : ℝ)⁻¹ * ∑ y, F y) := by
…

Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.primeSubsetPrior, OAI.Ostmann.treeLeafTupleEquiv