FourierVariance.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.BiasedFourier.coeff_empty line 16

theorem OAI.Problem313.BiasedFourier.weighted_variance_eq_second_moment line 22

Source documentation

Algebraic expansion of finite weighted variance. Positivity is not needed.

theorem weighted_variance_eq_second_moment {α : Type v} [Fintype α]
    (w g : α → ℝ) (hw : ∑ x, w x = 1) :
    (∑ x, w x * (g x - ∑ y, w y * g y) ^ 2) =
      (∑ x, w x * g x ^ 2) - (∑ x, w x * g x) ^ 2 := by
…

theorem OAI.Problem313.BiasedFourier.weight_mass_one line 44
Source documentation
The total mass of the finite Bernoulli product is one, algebraically for every bias.
```
theorem weight_mass_one (p : ℝ) : ∑ x : ι → Bool, weight p x = 1 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.weight

theorem OAI.Problem313.BiasedFourier.variance_eq_nonempty_of_parseval line 50

Source documentation

Parseval implies that the variance is exactly the nonconstant spectral mass.

theorem variance_eq_nonempty_of_parseval (p : ℝ) (g : (ι → Bool) → ℝ)
    (hparseval : (∑ x, weight p x * g x ^ 2) = ∑ S : Finset ι, coeff p g S ^ 2) :
    (∑ x, weight p x * (g x - coeff p g ∅) ^ 2) =
      ∑ S ∈ (Finset.univ : Finset (Finset ι)).erase ∅, coeff p g S ^ 2 := by
…

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

theorem OAI.Problem313.BiasedFourier.variance_eq_nonempty_filter_of_parseval line 58

Source documentation

The same identity with a nonempty filter, convenient for degree cutoffs.

theorem variance_eq_nonempty_filter_of_parseval (p : ℝ) (g : (ι → Bool) → ℝ)
    (hparseval : (∑ x, weight p x * g x ^ 2) = ∑ S : Finset ι, coeff p g S ^ 2) :
    (∑ x, weight p x * (g x - coeff p g ∅) ^ 2) =
      ∑ S ∈ (Finset.univ : Finset (Finset ι)).filter (fun S => S ≠ ∅), coeff p g S ^ 2 := by
…

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

theorem OAI.Problem313.BiasedFourier.variance_eq_nonempty line 65
theorem OAI.Problem313.BiasedFourier.weight_nonneg line 71
theorem OAI.Problem313.BiasedFourier.boolean_spectral_mass_le_one line 79
Source documentation
A Boolean function has total Fourier mass at most one.
```
theorem boolean_spectral_mass_le_one {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : (ι → Bool) → Bool) :
    (∑ S : Finset ι, coeff p (fun x => boolReal (f x)) S ^ 2) ≤ 1 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.boolReal
theorem OAI.Problem313.fourier_weight_eq_graphWeight line 97
theorem OAI.Problem313.fourier_coeff_empty_eq_graphMean line 100
theorem OAI.Problem313.graph_second_moment_eq_mean line 109

theorem OAI.Problem313.graphVariance_eq_fourier_nonempty_of_parseval line 118

Source documentation

The graph variance bridge needs only Parseval on the real-valued Boolean encoding.

theorem graphVariance_eq_fourier_nonempty_of_parseval {n : ℕ} (p : ℝ)
    (f : GraphConfig n → Bool)
    (hparseval : (∑ x, BiasedFourier.weight p x * boolReal (f x) ^ 2) =
      ∑ S : Finset (GraphEdge n), coeff p (fun x => boolReal (f x)) S ^ 2) :
    graphVariance p f =
      ∑ S ∈ (Finset.univ : Finset (Finset (GraphEdge n))).erase ∅,
        coeff p (fun x => boolReal (f x)) S ^ 2 := by
…

Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.BiasedFourier.weight, OAI.Problem313.boolReal, OAI.Problem313.GraphEdge, OAI.Problem313.graphVariance

theorem OAI.Problem313.graphVariance_eq_fourier_nonempty line 130
theorem OAI.Problem313.graphVariance_eq_fourier_nonempty_filter line 138
theorem OAI.Problem313.graph_fourier_mass_eq_mean line 146
theorem OAI.Problem313.graphVariance_eq_fourier_sum_nonempty line 154
Source documentation
The variance identity as a sum over nonempty Fourier supports.
```
theorem graphVariance_eq_fourier_sum_nonempty {n : ℕ} {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) (f : GraphConfig n → Bool) :
    graphVariance p f =
      ∑ S : Finset (GraphEdge n) with S.Nonempty,
        coeff p (fun x => boolReal (f x)) S ^ 2 := by
…
```
Mentions: OAI.Problem313.GraphConfig, OAI.Problem313.graphVariance, OAI.Problem313.GraphEdge, OAI.Problem313.boolReal