FiniteMaximumTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transferring a finite inner sum to its largest covered term

theorem OAI.Ostmann.finite_inner_sum_mean_le line 13

Source documentation

The index type need not be inhabited: if it has no covered term, every inner sum is empty. The bound is uniform over adaptive choices of indices.

theorem finite_inner_sum_mean_le {α β ι : Type*} [DecidableEq β]
    (A : Finset α) (D : α → Finset β) (f : α → β → ℝ) (g : α → ι → ℝ)
    (C δ B : ℝ) (hC : 0 ≤ C) (hδ : 0 ≤ δ) (hB : 0 ≤ B)
    (hf : ∀ a ∈ A, ∀ b ∈ D a, 0 ≤ f a b)
    (hg : ∀ a ∈ A, ∀ i, 0 ≤ g a i)
    (hcard : ∀ a ∈ A, ((D a).card : ℝ) ≤ C)
    (hcover : ∀ a ∈ A, ∀ b ∈ D a, ∃ i, f a b ≤ g a i + δ)
    (hmean : ∀ pick : α → ι,
      (A.card : ℝ)⁻¹ * (∑ a ∈ A, g a (pick a)) ≤ B) :
    (A.card : ℝ)⁻¹ * (∑ a ∈ A, ∑ b ∈ D a, f a b) ≤ C * (B + δ) := by
…