RestrictionInfluence.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite-product averaging for pivotal influences under restrictions.

def OAI.Problem313.RestrictionInfluence.weight line 16
Source documentation
Bernoulli weight on an arbitrary finite set of coordinates.
```
def weight (p : ℝ) (x : ι → Bool) : ℝ :=
…
```
def OAI.Problem313.RestrictionInfluence.influence line 20
Source documentation
The pivotal influence, with the redundant pivotal coordinate included in the sum.
```
def influence (p : ℝ) (f : (ι → Bool) → Bool) (i : ι) : ℝ := by
…
```
def OAI.Problem313.RestrictionInfluence.join line 28
Source documentation
Glue a free and an exterior configuration into a full configuration.
```
def join (x : {i // P i} → Bool) (y : {i // ¬ P i} → Bool) : ι → Bool :=
…
```
theorem OAI.Problem313.RestrictionInfluence.join_pos line 32
theorem OAI.Problem313.RestrictionInfluence.join_neg line 37
theorem OAI.Problem313.RestrictionInfluence.weight_join line 43
Source documentation
Product weights factor across any coordinate partition.
```
theorem weight_join (p : ℝ) (x : {i // P i} → Bool)
    (y : {i // ¬ P i} → Bool) :
    weight p (join P x y) = weight p x * weight p y := by
…
```
Mentions: OAI.Problem313.RestrictionInfluence.weight, OAI.Problem313.RestrictionInfluence.join
theorem OAI.Problem313.RestrictionInfluence.sum_weight_join line 51
Source documentation
Fubini for a coordinate restriction, with the exterior sum outermost.
```
theorem sum_weight_join (p : ℝ) (g : (ι → Bool) → ℝ) :
    (∑ z, weight p z * g z) =
      ∑ y : {i // ¬ P i} → Bool, weight p y *
        ∑ x : {i // P i} → Bool, weight p x * g (join P x y) := by
…
```
Mentions: OAI.Problem313.RestrictionInfluence.weight, OAI.Problem313.RestrictionInfluence.join
theorem OAI.Problem313.RestrictionInfluence.join_update line 71
Source documentation
Updating a free coordinate commutes with gluing an exterior configuration.
```
theorem join_update (x : {i // P i} → Bool) (y : {i // ¬ P i} → Bool)
    (i : {i // P i}) (b : Bool) :
    join P (Function.update x i b) y = Function.update (join P x y) i.val b := by
…
```
Mentions: OAI.Problem313.RestrictionInfluence.join
theorem OAI.Problem313.RestrictionInfluence.average_influence line 87
Source documentation
Averaging one pivotal influence over the exterior recovers the full influence.
```
theorem average_influence (p : ℝ) (f : (ι → Bool) → Bool) (i : {i // P i}) :
    (∑ y : {i // ¬ P i} → Bool,
      weight p y * influence p (fun x => f (join P x y)) i) =
        influence p f i.val := by
…
```
Mentions: OAI.Problem313.RestrictionInfluence.weight, OAI.Problem313.RestrictionInfluence.influence, OAI.Problem313.RestrictionInfluence.join
theorem OAI.Problem313.RestrictionInfluence.average_totalInfluence line 106
Source documentation
Averaging total influence on the free coordinates gives the sum of their original influences.
```
theorem average_totalInfluence (p : ℝ) (f : (ι → Bool) → Bool) :
    (∑ y : {i // ¬ P i} → Bool, weight p y *
      ∑ i : {i // P i}, influence p (fun x => f (join P x y)) i) =
        ∑ i : {i // P i}, influence p f i.val := by
…
```
Mentions: OAI.Problem313.RestrictionInfluence.weight, OAI.Problem313.RestrictionInfluence.influence, OAI.Problem313.RestrictionInfluence.join