FourierNoise.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem313.Spectral.coefficient line 13
def OAI.Problem313.Spectral.synthesis line 16
def OAI.Problem313.Spectral.multiplier line 19

theorem OAI.Problem313.Spectral.coefficient_synthesis line 24

Source documentation

Orthogonality diagonalizes every spectral multiplier.

theorem coefficient_synthesis (w : Ω → ℝ) (χ : S → Ω → ℝ)
    (horth : ∀ s t, (∑ x, w x * χ s x * χ t x) = if s = t then 1 else 0)
    (a : S → ℝ) (t : S) :
    coefficient w χ (synthesis χ a) t = a t := by
…

Mentions: OAI.Problem313.Spectral.coefficient, OAI.Problem313.Spectral.synthesis

theorem OAI.Problem313.Spectral.coefficient_multiplier line 45

Source documentation

The Fourier coefficient of a multiplier is multiplied by its symbol.

theorem coefficient_multiplier (w : Ω → ℝ) (χ : S → Ω → ℝ)
    (horth : ∀ s t, (∑ x, w x * χ s x * χ t x) = if s = t then 1 else 0)
    (symbol : S → ℝ) (f : Ω → ℝ) (t : S) :
    coefficient w χ (multiplier w χ symbol f) t = symbol t * coefficient w χ f t :=
…

Mentions: OAI.Problem313.Spectral.coefficient, OAI.Problem313.Spectral.multiplier

theorem OAI.Problem313.Spectral.inner_synthesis line 53
Source documentation
Finite synthesis/analysis duality, without any orthogonality assumption.
```
theorem inner_synthesis (w : Ω → ℝ) (χ : S → Ω → ℝ)
    (a : S → ℝ) (g : Ω → ℝ) :
    (∑ x, w x * synthesis χ a x * g x) =
      ∑ s, a s * coefficient w χ g s := by
…
```
Mentions: OAI.Problem313.Spectral.synthesis, OAI.Problem313.Spectral.coefficient

theorem OAI.Problem313.Spectral.multiplier_self_adjoint line 73

Source documentation

Every real spectral multiplier is self-adjoint.

theorem multiplier_self_adjoint (w : Ω → ℝ) (χ : S → Ω → ℝ)
    (symbol : S → ℝ) (f g : Ω → ℝ) :
    (∑ x, w x * multiplier w χ symbol f x * g x) =
      ∑ x, w x * f x * multiplier w χ symbol g x := by
…

Mentions: OAI.Problem313.Spectral.multiplier

theorem OAI.Problem313.Spectral.synthesis_energy line 92

Source documentation

Parseval for an explicitly synthesized function.

theorem synthesis_energy (w : Ω → ℝ) (χ : S → Ω → ℝ)
    (horth : ∀ s t, (∑ x, w x * χ s x * χ t x) = if s = t then 1 else 0)
    (a : S → ℝ) :
    (∑ x, w x * (synthesis χ a x)^2) = ∑ s, (a s)^2 := by
…

Mentions: OAI.Problem313.Spectral.synthesis

def OAI.Problem313.BiasedFourier.noise line 115
Source documentation
The biased noise operator, defined by its Fourier multiplier.
```
def noise (p ρ : ℝ) (g : (ι → Bool) → ℝ) (x : ι → Bool) : ℝ := by
…
```
theorem OAI.Problem313.BiasedFourier.noise_self_adjoint line 119