FiniteParseval.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem313.FiniteParseval.coefficient line 16
Source documentation
Fourier coefficient for an arbitrary finite weighted system.
```
def coefficient (w : Ω → ℝ) (χ : α → Ω → ℝ) (f : Ω → ℝ) (a : α) : ℝ :=
…
```

theorem OAI.Problem313.FiniteParseval.expansion line 21

Source documentation

A square weighted orthonormal system is complete. No positivity is needed for this algebraic statement.

theorem expansion (w : Ω → ℝ) (χ : α → Ω → ℝ)
    (hcard : Fintype.card α = Fintype.card Ω)
    (horth : ∀ a b, (∑ x, w x * χ a x * χ b x) = if a = b then 1 else 0)
    (f : Ω → ℝ) (x : Ω) :
    (∑ a, coefficient w χ f a * χ a x) = f x := by
…

Mentions: OAI.Problem313.FiniteParseval.coefficient

theorem OAI.Problem313.FiniteParseval.parseval_bilinear line 49

Source documentation

Parseval's bilinear identity for a finite weighted orthonormal system.

theorem parseval_bilinear (w : Ω → ℝ) (χ : α → Ω → ℝ)
    (hcard : Fintype.card α = Fintype.card Ω)
    (horth : ∀ a b, (∑ x, w x * χ a x * χ b x) = if a = b then 1 else 0)
    (f g : Ω → ℝ) :
    (∑ a, coefficient w χ f a * coefficient w χ g a) = ∑ x, w x * f x * g x := by
…

Mentions: OAI.Problem313.FiniteParseval.coefficient

theorem OAI.Problem313.FiniteParseval.parseval line 68

Source documentation

The usual sum-of-squares Parseval identity.

theorem parseval (w : Ω → ℝ) (χ : α → Ω → ℝ)
    (hcard : Fintype.card α = Fintype.card Ω)
    (horth : ∀ a b, (∑ x, w x * χ a x * χ b x) = if a = b then 1 else 0)
    (f : Ω → ℝ) :
    (∑ a, (coefficient w χ f a)^2) = ∑ x, w x * (f x)^2 := by
…

Mentions: OAI.Problem313.FiniteParseval.coefficient

def OAI.Problem313.FiniteParseval.synthesis line 76
Source documentation
Synthesis using only a selected finite set of spectral coordinates.
```
def synthesis (χ : α → Ω → ℝ) (c : α → ℝ) (s : Finset α) (x : Ω) : ℝ :=
…
```
theorem OAI.Problem313.FiniteParseval.coefficient_synthesis line 80
theorem OAI.Problem313.FiniteParseval.inner_synthesis line 99
theorem OAI.Problem313.FiniteParseval.synthesis_sq line 113

theorem OAI.Problem313.FiniteParseval.projection_inner_eq_sq line 131

Source documentation

The algebraic orthogonal-projection identity used by the low-degree Hölder estimate.

theorem projection_inner_eq_sq (w : Ω → ℝ) (χ : α → Ω → ℝ)
    (horth : ∀ a b, (∑ x, w x * χ a x * χ b x) = if a = b then 1 else 0)
    (f : Ω → ℝ) (s : Finset α) :
    (∑ x, w x * f x * synthesis χ (coefficient w χ f) s x) =
      ∑ x, w x * (synthesis χ (coefficient w χ f) s x)^2 := by
…

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