OAI/Combinatorics/SharpThreshold/BlockInfluence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.restrictCube_influence_reindex line 17

   Source documentation

   Pivotal influences of a conditioned function are invariant under every coordinate permutation that preserves the free set and fixes its complement.

   theorem restrictCube_influence_reindex {α : Type u} [Fintype α]
       (P : α → Prop) [DecidablePred P]
       (π : Equiv.Perm α) (hP : ∀ i, P i ↔ P (π i))
       (hfix : ∀ i, ¬ P i → π i = i) (f : (α → Bool) → Bool)
       (hf : ∀ z, f (fun i => z (π.symm i)) = f z)
       (p : ℝ) (y : {i // ¬ P i} → Bool) (i : {i // P i}) :
       Reindex.influence p (restrictCube P f y) ((π.subtypeEquiv hP) i) =
         Reindex.influence p (restrictCube P f y) i := by
   …

   Mentions: OAI.Problem313.Reindex.influence, OAI.Problem313.restrictCube

2. theorem OAI.Problem313.restrictCube_influence_permEdge line 30

   Source documentation

   Conditional edge influences respect vertex permutations supported on the block.

   theorem restrictCube_influence_permEdge {n : ℕ}
       (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)]
       (π : Equiv.Perm (Fin n)) (hπ : SupportedOnBlock B π)
       (f : GraphConfig n → Bool) (hf : VertexInvariant f)
       (p : ℝ) (y : {e : GraphEdge n // ¬ EdgeTouches B e} → Bool)
       (e : {e : GraphEdge n // EdgeTouches B e}) :
       Reindex.influence p (restrictCube (EdgeTouches B) f y)
           ⟨permEdge π e.val, (edgeTouches_permEdge_iff hπ e.val).mpr e.property⟩ =
         Reindex.influence p (restrictCube (EdgeTouches B) f y) e := by
   …

   Mentions: OAI.Problem313.EdgeTouches, OAI.Problem313.SupportedOnBlock, OAI.Problem313.GraphConfig, OAI.Problem313.VertexInvariant, OAI.Problem313.GraphEdge, OAI.Problem313.Reindex.influence, OAI.Problem313.restrictCube, OAI.Problem313.permEdge, OAI.Problem313.edgeTouches_permEdge_iff

3. theorem OAI.Problem313.restrictCube_influence_le_of_orbit line 46

   Source documentation

   Quantitative conditional influence bound from a finite collection of edges in one block orbit. The collection may be supplied on the original edge type.

   theorem restrictCube_influence_le_of_orbit {n : ℕ}
       (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)]
       (f : GraphConfig n → Bool) (hf : VertexInvariant f)
       {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
       (y : {e : GraphEdge n // ¬ EdgeTouches B e} → Bool)
       (e : {e : GraphEdge n // EdgeTouches B e}) (S : Finset (GraphEdge n))
       {m : ℝ} (hm : 0 < m) (hcard : m ≤ (S.card : ℝ))
       (horbit : ∀ d ∈ S, ∃ π : Equiv.Perm (Fin n),
         SupportedOnBlock B π ∧ permEdge π e.val = d) :
       Reindex.influence p (restrictCube (EdgeTouches B) f y) e ≤
         (∑ d, Reindex.influence p (restrictCube (EdgeTouches B) f y) d) / m := by
   …

   Mentions: OAI.Problem313.EdgeTouches, OAI.Problem313.GraphConfig, OAI.Problem313.VertexInvariant, OAI.Problem313.GraphEdge, OAI.Problem313.SupportedOnBlock, OAI.Problem313.permEdge, OAI.Problem313.Reindex.influence, OAI.Problem313.restrictCube

4. theorem OAI.Problem313.block_restricted_influence_le line 73

   Source documentation

   Every conditional influence on edges touching a block is at most the total conditional influence divided by the number of block vertices.

   theorem block_restricted_influence_le {n : ℕ}
       (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)] (hB : 3 ≤ B.card)
       (f : GraphConfig n → Bool) (hf : VertexInvariant f)
       {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
       (y : {e : GraphEdge n // ¬ EdgeTouches B e} → Bool)
       (e : {e : GraphEdge n // EdgeTouches B e}) :
       Reindex.influence p (restrictCube (EdgeTouches B) f y) e ≤
         (∑ d, Reindex.influence p (restrictCube (EdgeTouches B) f y) d) /
           (B.card : ℝ) := by
   …

   Mentions: OAI.Problem313.EdgeTouches, OAI.Problem313.GraphConfig, OAI.Problem313.VertexInvariant, OAI.Problem313.GraphEdge, OAI.Problem313.Reindex.influence, OAI.Problem313.restrictCube