OrbitInfluence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.weight_le_sum_div_of_constant_on line 13

Source documentation

A nonnegative weight which is constant on a sufficiently large finite set is at most the total weight divided by the size lower bound.

theorem weight_le_sum_div_of_constant_on
    {ι : Type u} [Fintype ι] (w : ι → ℝ) (O : Finset ι) (e : ι) (m : ℝ)
    (hm : 0 < m) (hw : ∀ j, 0 ≤ w j)
    (hcard : m ≤ (O.card : ℝ))
    (hconstant : ∀ j ∈ O, w j = w e) :
    w e ≤ (∑ j, w j) / m := by
…

theorem OAI.Problem313.weight_le_sum_div_of_injective_family line 35

Source documentation

The same bound when each point of a finite injectively indexed family has weight equal to the distinguished point. This form avoids constructing an orbit.

theorem weight_le_sum_div_of_injective_family
    {ι : Type u} {κ : Type v} [Fintype ι] [Fintype κ]
    (w : ι → ℝ) (e : ι) (φ : κ → ι) (hφ : Function.Injective φ)
    (m : ℝ) (hm : 0 < m) (hcard : m ≤ (Fintype.card κ : ℝ))
    (hw : ∀ j, 0 ≤ w j) (hconstant : ∀ j, w (φ j) = w e) :
    w e ≤ (∑ j, w j) / m := by
…