CycleCoefficient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A coefficient bound for a cycle

Once all but one Mellin index are fixed, the cycle relation determines the remaining index. This is the final finite-sum estimate in Section 6.

theorem OAI.Ostmann.cycleCoefficient_sum_le line 20

Source documentation

A cycle relation costs one supremum and the masses of the remaining indices.

theorem cycleCoefficient_sum_le {G I : Type*} [CommGroup G] [Fintype G] [Fintype I]
    [DecidableEq G] [DecidableEq I]
    (b₀ : G → ℝ) (b : I → G → ℝ) (S : ℝ)
    (h₀ : ∀ a, b₀ a ≤ S) (hb : ∀ i a, 0 ≤ b i a) :
    (∑ f : I → G, ∑ a : G,
      if a * (∏ i, f i) = 1 then b₀ a * (∏ i, b i (f i)) else 0) ≤
        S * ∏ i, ∑ a : G, b i a := by
…