Russo.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.hasDerivAt_graphWeight line 11

Source documentation

Derivative of the Bernoulli mass of a single graph configuration.

theorem hasDerivAt_graphWeight {n : ℕ} (p : ℝ) (x : GraphConfig n) :
    HasDerivAt (fun q => graphWeight q x)
      (∑ e : GraphEdge n, (if x e = true then (1 : ℝ) else -1) *
        ∏ j ∈ Finset.univ.erase e, if x j = true then p else 1 - p) p := by
…

Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.graphWeight, OAI.Problem313.GraphEdge

theorem OAI.Problem313.hasDerivAt_graphMean_raw line 26

Source documentation

The finite product rule for the graph probability polynomial.

theorem hasDerivAt_graphMean_raw {n : ℕ} (f : GraphConfig n → Bool) (p : ℝ) :
    HasDerivAt (fun q => graphMean q f)
      (∑ e : GraphEdge n, ∑ x : GraphConfig n,
        ((if x e = true then (1 : ℝ) else -1) *
          ∏ j ∈ Finset.univ.erase e, if x j = true then p else 1 - p) *
          boolReal (f x)) p := by
…

Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.graphMean, OAI.Problem313.GraphEdge, OAI.Problem313.boolReal

theorem OAI.Problem313.differentiable_graphMean line 40
Source documentation
The graph probability is a differentiable polynomial, without a monotonicity assumption.
```
theorem differentiable_graphMean {n : ℕ} (f : GraphConfig n → Bool) :
    Differentiable ℝ (fun p => graphMean p f) :=
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.graphMean
theorem OAI.Problem313.continuous_graphMean_russo line 45
Source documentation
Continuity of graph probability as a function of the edge bias.
```
theorem continuous_graphMean_russo {n : ℕ} (f : GraphConfig n → Bool) :
    Continuous (fun p => graphMean p f) :=
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.graphMean
theorem OAI.Problem313.increasing_update_false_true line 50
Source documentation
Every increasing property has nonnegative Boolean coordinate differences.
```
theorem increasing_update_false_true {n : ℕ} {f : GraphConfig n → Bool}
    (hf : IncreasingGraphProperty f) (x : GraphConfig n) (e : GraphEdge n) :
    f (Function.update x e false) = true → f (Function.update x e true) = true := by
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.IncreasingGraphProperty, OAI.Problem313.GraphEdge

theorem OAI.Problem313.boolReal_update_sub_eq_indicator line 62

Source documentation

For an increasing Boolean function the coordinate difference is its pivotal indicator.

theorem boolReal_update_sub_eq_indicator {n : ℕ} {f : GraphConfig n → Bool}
    (hf : IncreasingGraphProperty f) (x : GraphConfig n) (e : GraphEdge n) :
    boolReal (f (Function.update x e true)) - boolReal (f (Function.update x e false)) =
      if f (Function.update x e true) ≠ f (Function.update x e false) then 1 else 0 := by
…

Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.IncreasingGraphProperty, OAI.Problem313.GraphEdge, OAI.Problem313.boolReal

theorem OAI.Problem313.edgeInfluence_eq_sum_boolReal_sub line 73
Source documentation
Monotone pivotal influence is the expectation of the oriented coordinate difference.
```
theorem edgeInfluence_eq_sum_boolReal_sub {n : ℕ} {f : GraphConfig n → Bool}
    (hf : IncreasingGraphProperty f) (p : ℝ) (e : GraphEdge n) :
    edgeInfluence p f e = ∑ x : GraphConfig n, graphWeight p x *
      (boolReal (f (Function.update x e true)) -
        boolReal (f (Function.update x e false))) := by
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.IncreasingGraphProperty, OAI.Problem313.GraphEdge, OAI.Problem313.edgeInfluence, OAI.Problem313.graphWeight, OAI.Problem313.boolReal
theorem OAI.Problem313.hasDerivAt_graphMean line 87
Source documentation
Russo--Margulis formula with pivotal total influence. The identity is polynomial, so no restriction to biases in [0,1] is necessary.
```
theorem hasDerivAt_graphMean {n : ℕ} {f : GraphConfig n → Bool}
    (hf : IncreasingGraphProperty f) (p : ℝ) :
    HasDerivAt (fun q => graphMean q f) (totalInfluence p f) p := by
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.IncreasingGraphProperty, OAI.Problem313.graphMean, OAI.Problem313.totalInfluence
theorem OAI.Problem313.deriv_graphMean line 99
Source documentation
Derivative form of the Russo--Margulis identity.
```
theorem deriv_graphMean {n : ℕ} {f : GraphConfig n → Bool}
    (hf : IncreasingGraphProperty f) (p : ℝ) :
    deriv (fun q => graphMean q f) p = totalInfluence p f :=
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.IncreasingGraphProperty, OAI.Problem313.graphMean, OAI.Problem313.totalInfluence