FourierDerivative.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem313.BiasedFourier.delta line 15
Source documentation
The discrete derivative, retained as a function on the full cube.
```
def delta (i : ι) (g : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ :=
…
```
theorem OAI.Problem313.BiasedFourier.delta_update line 18
theorem OAI.Problem313.BiasedFourier.delta_delta_fun line 23
theorem OAI.Problem313.BiasedFourier.delta_delta line 28
theorem OAI.Problem313.BiasedFourier.char_update_aux line 31
theorem OAI.Problem313.BiasedFourier.char_update_of_not_mem line 38
theorem OAI.Problem313.BiasedFourier.integral_chi_eq_sqrt_mul_delta line 46
Source documentation
Integration by parts against one normalized biased character.
```
theorem integral_chi_eq_sqrt_mul_delta {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (i : ι) (g : (ι → Bool) → ℝ) :
    (∑ x, weight p x * g x * chi p (x i)) =
      Real.sqrt (p * (1-p)) * ∑ x, weight p x * delta i g x := by
…
```
Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.chi, OAI.Problem313.BiasedFourier.delta
theorem OAI.Problem313.BiasedFourier.coeff_insert_eq_sqrt_mul_delta line 68
Source documentation
Fourier coefficients of a coordinate derivative, with the same full cube on both sides.
```
theorem coeff_insert_eq_sqrt_mul_delta {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : (ι → Bool) → ℝ) (i : ι) (A : Finset ι) (hi : i ∉ A) :
    coeff p g (insert i A) =
      Real.sqrt (p * (1-p)) * coeff p (delta i g) A := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.delta
theorem OAI.Problem313.BiasedFourier.coeff_eq_sqrt_mul_delta_erase line 111
Source documentation
Erasing a coordinate from a nonzero-degree coefficient gives the derivative coefficient.
```
theorem coeff_eq_sqrt_mul_delta_erase {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : (ι → Bool) → ℝ) (i : ι) (S : Finset ι) (hi : i ∈ S) :
    coeff p g S = Real.sqrt (p * (1-p)) * coeff p (delta i g) (S.erase i) := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.delta
theorem OAI.Problem313.BiasedFourier.coeff_sq_eq_variance_mul_delta_erase_sq line 118
Source documentation
Squared Fourier derivative identity, in the normalization used by Dirichlet energy.
```
theorem coeff_sq_eq_variance_mul_delta_erase_sq {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : (ι → Bool) → ℝ) (i : ι) (S : Finset ι) (hi : i ∈ S) :
    coeff p g S ^ 2 = p * (1-p) * coeff p (delta i g) (S.erase i) ^ 2 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.delta
theorem OAI.Problem313.BiasedFourier.coeff_delta_eq_zero_of_mem line 125
Source documentation
A coordinate derivative has no Fourier support containing that coordinate.
```
theorem coeff_delta_eq_zero_of_mem {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : (ι → Bool) → ℝ) (i : ι) (S : Finset ι) (hi : i ∈ S) :
    coeff p (delta i g) S = 0 := by
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.delta
theorem OAI.Problem313.BiasedFourier.coeff_insert_eq_sqrt_mul_coeff_delta line 135
Source documentation
The Fourier derivative identity with coordinate-first parameter order.
```
theorem coeff_insert_eq_sqrt_mul_coeff_delta {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (i : ι) (g : (ι → Bool) → ℝ) (A : Finset ι) (hi : i ∉ A) :
    coeff p g (insert i A) = Real.sqrt (p * (1-p)) * coeff p (delta i g) A :=
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.delta
theorem OAI.Problem313.BiasedFourier.coeff_delta_eq_zero line 141
Source documentation
The Fourier derivative identity with coordinate-first parameter order.
```
theorem coeff_delta_eq_zero {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (i : ι) (g : (ι → Bool) → ℝ) (S : Finset ι) (hi : i ∈ S) :
    coeff p (delta i g) S = 0 :=
…
```
Mentions: OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.delta