TreeProductDisintegration.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Disintegrating the original independent leaf law by its total product

theorem OAI.Ostmann.sum_treeLeafTuple_dependent line 11
theorem OAI.Ostmann.treeLeaf_average_by_product line 23

theorem OAI.Ostmann.treeLeaf_average_le line 37

Source documentation

A bound uniform in the exposed product is also a bound for the original independent leaf samples.

theorem treeLeaf_average_le {G : Type} [CommGroup G] [Fintype G]
    (n : ℕ) (F : (P : G) → TreeLeafFiber G n P → ℝ) (B : ℝ)
    (hF : ∀ P, (Fintype.card (TreeLeafFiber G n P) : ℝ)⁻¹ * ∑ x, F P x ≤ B) :
    (Fintype.card (TreeLeafTuple G n) : ℝ)⁻¹ *
        (∑ x : TreeLeafTuple G n, F (treeLeafProduct n x) ⟨x, rfl⟩) ≤ B := by
…

Mentions: OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.treeLeafProduct