FourierDirichlet.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.BiasedFourier.coordinate_energy_of_coeff_derivative line 18

Source documentation

The coordinate Dirichlet identity, with only the two derivative coefficient identities isolated as hypotheses.

theorem coordinate_energy_of_coeff_derivative {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g dg : (ι → Bool) → ℝ) (i : ι)
    (hzero : ∀ S, i ∈ S → coeff p dg S = 0)
    (hinsert : ∀ S, i ∉ S → coeff p g (insert i S) =
      Real.sqrt (p * (1 - p)) * coeff p dg S) :
    (∑ S : Finset ι, if i ∈ S then (coeff p g S)^2 else 0) =
      p * (1 - p) * ∑ x, weight p x * (dg x)^2 := by
…

Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.weight

theorem OAI.Problem313.BiasedFourier.total_energy_of_coordinate_energy line 30

Source documentation

Summing coordinate Dirichlet identities gives degree-weighted Fourier energy.

theorem total_energy_of_coordinate_energy {p : ℝ}
    (g : (ι → Bool) → ℝ) (E : ι → ℝ)
    (hcoord : ∀ i, (∑ S : Finset ι, if i ∈ S then (coeff p g S)^2 else 0) =
      p * (1 - p) * E i) :
    (∑ S : Finset ι, (S.card : ℝ) * (coeff p g S)^2) =
      p * (1 - p) * ∑ i, E i := by
…

Mentions: OAI.Problem313.BiasedFourier.coeff

theorem OAI.Problem313.BiasedFourier.coordinate_dirichlet line 42
Source documentation
The Fourier mass on supports containing a fixed coordinate equals its weighted squared discrete derivative.
```
theorem coordinate_dirichlet {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : (ι → Bool) → ℝ) (i : ι) :
    (∑ S : Finset ι, if i ∈ S then (coeff p g S)^2 else 0) =
      p * (1 - p) * ∑ x, weight p x * (delta i g x)^2 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.delta
theorem OAI.Problem313.BiasedFourier.dirichlet line 51
Source documentation
The full finite-cube Fourier Dirichlet identity for real observables.
```
theorem dirichlet {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : (ι → Bool) → ℝ) :
    (∑ S : Finset ι, (S.card : ℝ) * (coeff p g S)^2) =
      p * (1 - p) * ∑ i, ∑ x, weight p x * (delta i g x)^2 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.delta
theorem OAI.Problem313.BiasedFourier.boolean_coordinate_dirichlet line 58
Source documentation
For Boolean observables, squared derivative energy is pivotal influence.
```
theorem boolean_coordinate_dirichlet {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : (ι → Bool) → Bool) (i : ι) :
    (∑ S : Finset ι, if i ∈ S then (coeff p (fun x => boolReal (f x)) S)^2 else 0) =
      p * (1 - p) * Reindex.influence p f i := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal, OAI.Problem313.Reindex.influence
theorem OAI.Problem313.BiasedFourier.boolean_dirichlet line 69
Source documentation
The degree-weighted Fourier mass of a Boolean function is its total pivotal influence times the Bernoulli variance.
```
theorem boolean_dirichlet {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : (ι → Bool) → Bool) :
    (∑ S : Finset ι, (S.card : ℝ) * (coeff p (fun x => boolReal (f x)) S)^2) =
      p * (1 - p) * ∑ i, Reindex.influence p f i := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal, OAI.Problem313.Reindex.influence
theorem OAI.Problem313.graph_fourier_dirichlet line 80
Source documentation
The graph Dirichlet identity for pivotal total influence.
```
theorem graph_fourier_dirichlet {n : ℕ} {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : GraphConfig n → Bool) :
    (∑ S : Finset (GraphEdge n), (S.card : ℝ) *
      (BiasedFourier.coeff p (fun x => boolReal (f x)) S)^2) =
      p * (1 - p) * totalInfluence p f := by
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.GraphEdge, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal, OAI.Problem313.totalInfluence