RussoReindex.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem313.russoInsert line 14
Source documentation
Reinsert one Boolean coordinate in a function on the remaining coordinates.
```
def russoInsert (i : ι) (b : Bool) (z : {j : ι // j ≠ i} → Bool) : ι → Bool :=
…
```
theorem OAI.Problem313.russoInsert_self line 17
theorem OAI.Problem313.russoInsert_of_ne line 21
theorem OAI.Problem313.update_russoInsert line 26

theorem OAI.Problem313.sum_bool_split line 37

Source documentation

Splitting a finite Boolean cube at one coordinate.

theorem sum_bool_split (i : ι) (g : (ι → Bool) → ℝ) :
    (∑ x, g x) = ∑ z : {j : ι // j ≠ i} → Bool,
      (g (russoInsert i true z) + g (russoInsert i false z)) := by
…

Mentions: OAI.Problem313.russoInsert

theorem OAI.Problem313.prod_erase_russoInsert line 45

Source documentation

The product excluding a coordinate does not depend on that coordinate.

theorem prod_erase_russoInsert (p : ℝ) (i : ι) (b c : Bool)
    (z : {j : ι // j ≠ i} → Bool) :
    (∏ j ∈ Finset.univ.erase i, if russoInsert i b z j = true then p else 1-p) =
    ∏ j ∈ Finset.univ.erase i, if russoInsert i c z j = true then p else 1-p := by
…

Mentions: OAI.Problem313.russoInsert

theorem OAI.Problem313.prod_russoInsert line 55

Source documentation

A Bernoulli weight factors at a chosen coordinate.

theorem prod_russoInsert (p : ℝ) (i : ι) (b : Bool)
    (z : {j : ι // j ≠ i} → Bool) :
    (∏ j, if russoInsert i b z j = true then p else 1-p) =
    (if b = true then p else 1-p) *
      ∏ j ∈ Finset.univ.erase i, if russoInsert i false z j = true then p else 1-p := by
…

Mentions: OAI.Problem313.russoInsert

theorem OAI.Problem313.russo_sum_reindex line 67

Source documentation

Finite reindexing identity behind the Russo--Margulis derivative formula. No positivity assumptions on the bias or the observable are needed.

theorem russo_sum_reindex (p : ℝ) (i : ι) (g : (ι → Bool) → ℝ) :
    (∑ x : ι → Bool, (if x i = true then (1 : ℝ) else -1) *
      (∏ j ∈ Finset.univ.erase i, if x j = true then p else 1-p) * g x) =
    ∑ x : ι → Bool, (∏ j, if x j = true then p else 1-p) *
      (g (Function.update x i true) - g (Function.update x i false)) := by
…

theorem OAI.Problem313.sum_weight_conditioning line 81

Source documentation

Integrating out one coordinate is unchanged by Bernoulli resampling.

theorem sum_weight_conditioning (p : ℝ) (i : ι) (g : (ι → Bool) → ℝ) :
    (∑ x : ι → Bool, (∏ j, if x j = true then p else 1-p) * g x) =
    ∑ x : ι → Bool, (∏ j, if x j = true then p else 1-p) *
      ((1-p) * g (Function.update x i false) + p * g (Function.update x i true)) := by
…

theorem OAI.Problem313.sum_weight_update line 92

Source documentation

A reset observable can be integrated on the cube with that coordinate removed.

theorem sum_weight_update (p : ℝ) (i : ι) (b : Bool) (g : (ι → Bool) → ℝ) :
    (∑ x : ι → Bool, (∏ j, if x j = true then p else 1-p) *
      g (Function.update x i b)) =
    ∑ z : {j : ι // j ≠ i} → Bool,
      (∏ j ∈ Finset.univ.erase i, if russoInsert i false z j = true then p else 1-p) *
      g (russoInsert i b z) := by
…

Mentions: OAI.Problem313.russoInsert

theorem OAI.Problem313.sum_weight_centered_coordinate line 105

Source documentation

Discrete integration by parts for a centered Bernoulli coordinate.

theorem sum_weight_centered_coordinate (p : ℝ) (i : ι) (g : (ι → Bool) → ℝ) :
    (∑ x : ι → Bool, (∏ j, if x j = true then p else 1-p) * g x *
      ((if x i = true then (1 : ℝ) else 0) - p)) =
    p * (1-p) * ∑ x : ι → Bool, (∏ j, if x j = true then p else 1-p) *
      (g (Function.update x i true) - g (Function.update x i false)) := by
…