OAI/Combinatorics/SharpThreshold/InfluenceReindex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem313.Reindex.config line 14
  2. def OAI.Problem313.Reindex.configEquiv line 16
  3. theorem OAI.Problem313.Reindex.config_apply line 22
  4. theorem OAI.Problem313.Reindex.configEquiv_apply line 25
  5. theorem OAI.Problem313.Reindex.config_update line 28
  6. def OAI.Problem313.Reindex.weight line 40
  7. def OAI.Problem313.Reindex.influence line 43
  8. theorem OAI.Problem313.Reindex.weight_config line 48
  9. theorem OAI.Problem313.Reindex.influence_config line 53
  10. theorem OAI.Problem313.Reindex.weight_nonneg line 64
  11. theorem OAI.Problem313.Reindex.influence_nonneg line 71
  12. theorem OAI.Problem313.Reindex.influence_le_total_div line 82

    Source documentation

    An orbit of at least m equally influential coordinates bounds each influence.

    theorem influence_le_total_div [Fintype ι] {p : ℝ}
    (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (f : (ι → Bool) → Bool) (i : ι)
    (S : Finset ι) {m : ℝ} (hm : 0 < m) (hcard : m ≤ (S.card : ℝ))
    (heq : ∀ j ∈ S, influence p f j = influence p f i) :
    influence p f i ≤ (∑ j, influence p f j) / m := by
…

    Mentions: OAI.Problem313.Reindex.influence