GraphRestrictionInfluence.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.restrictionWeight_eq_graphWeight line 16
Source documentation
The generic restriction weight agrees with the qualified graph weight.
```
theorem restrictionWeight_eq_graphWeight {n : ℕ} (p : ℝ) (x : GraphConfig n) :
    RestrictionInfluence.weight p x = graphWeight p x := rfl
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.RestrictionInfluence.weight, OAI.Problem313.graphWeight
theorem OAI.Problem313.restrictionInfluence_eq_edgeInfluence line 20
Source documentation
The generic restriction influence agrees with the qualified graph influence.
```
theorem restrictionInfluence_eq_edgeInfluence {n : ℕ} (p : ℝ)
    (f : GraphConfig n → Bool) (e : GraphEdge n) :
    RestrictionInfluence.influence p f e = edgeInfluence p f e := rfl
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.GraphEdge, OAI.Problem313.RestrictionInfluence.influence, OAI.Problem313.edgeInfluence
theorem OAI.Problem313.restrictionWeight_eq_reindexWeight line 25
Source documentation
The two generic influence interfaces have definitionally identical weights.
```
theorem restrictionWeight_eq_reindexWeight {ι : Type u} [Fintype ι] [DecidableEq ι]
    (p : ℝ) (x : ι → Bool) :
    RestrictionInfluence.weight p x = Reindex.weight p x := rfl
```
Mentions: OAI.Problem313.RestrictionInfluence.weight, OAI.Problem313.Reindex.weight
theorem OAI.Problem313.restrictionInfluence_eq_reindexInfluence line 30
Source documentation
The two generic influence interfaces have equal influences after identifying their decidable-equality instances.
```
theorem restrictionInfluence_eq_reindexInfluence {ι : Type u} [Fintype ι] [d : DecidableEq ι]
    (p : ℝ) (f : (ι → Bool) → Bool) (i : ι) :
    RestrictionInfluence.influence p f i = Reindex.influence p f i := by
…
```
Mentions: OAI.Problem313.RestrictionInfluence.influence, OAI.Problem313.Reindex.influence

theorem OAI.Problem313.block_average_edgeInfluence line 37

Source documentation

Averaging a conditional free-edge influence recovers its original graph influence.

theorem block_average_edgeInfluence {n : ℕ} (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)] (p : ℝ)
    (f : GraphConfig n → Bool) (e : {e : GraphEdge n // EdgeTouches B e}) :
    (∑ y : {e : GraphEdge n // ¬ EdgeTouches B e} → Bool,
      Reindex.weight p y * Reindex.influence p (restrictCube (EdgeTouches B) f y) e) =
      edgeInfluence p f e.val := by
…

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

theorem OAI.Problem313.block_average_totalInfluence line 51

Source documentation

Averaging conditional total influence gives precisely the original influences of edges touching the block; no invariance or monotonicity is needed.

theorem block_average_totalInfluence {n : ℕ} (B : Finset (Fin n)) [DecidablePred (EdgeTouches B)] (p : ℝ)
    (f : GraphConfig n → Bool) :
    (∑ y : {e : GraphEdge n // ¬ EdgeTouches B e} → Bool,
      Reindex.weight p y * ∑ e : {e : GraphEdge n // EdgeTouches B e},
        Reindex.influence p (restrictCube (EdgeTouches B) f y) e) =
      ∑ e : {e : GraphEdge n // EdgeTouches B e}, edgeInfluence p f e.val := by
…

theorem OAI.Problem313.block_average_totalInfluence_filter line 65

Source documentation

The conditional total-influence identity, with a filtered finite edge sum.

theorem block_average_totalInfluence_filter {n : ℕ} (B : Finset (Fin n))
    [DecidablePred (EdgeTouches B)] (p : ℝ) (f : GraphConfig n → Bool) :
    (∑ y : {e : GraphEdge n // ¬ EdgeTouches B e} → Bool,
      Reindex.weight p y * ∑ e : {e : GraphEdge n // EdgeTouches B e},
        Reindex.influence p (restrictCube (EdgeTouches B) f y) e) =
      ∑ e ∈ Finset.univ.filter (EdgeTouches B), edgeInfluence p f e := by
…