OAI/Combinatorics/SharpThreshold/ProjectionIdentities.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem313.WeightedProjection.coefficient line 15
2. def OAI.Problem313.WeightedProjection.synthesis line 18
3. theorem OAI.Problem313.WeightedProjection.inner_synthesis line 22

   Source documentation

   Pairing a function with a finite spectral expansion pairs its coefficients.

   theorem inner_synthesis (w : X → ℝ) (basis : ι → X → ℝ)
       (f : X → ℝ) (L : Finset ι) (c : ι → ℝ) :
       (∑ x, w x * f x * synthesis basis L c x) =
         ∑ i ∈ L, c i * coefficient w basis f i := by
   …

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

4. theorem OAI.Problem313.WeightedProjection.coefficient_synthesis line 35

   Source documentation

   Orthonormality computes the coefficient of a finite spectral expansion.

   theorem coefficient_synthesis [DecidableEq ι]
       (w : X → ℝ) (basis : ι → X → ℝ)
       (horth : ∀ i j, (∑ x, w x * basis i x * basis j x) = if i = j then 1 else 0)
       (L : Finset ι) (c : ι → ℝ) (i : ι) :
       coefficient w basis (synthesis basis L c) i = if i ∈ L then c i else 0 := by
   …

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

5. theorem OAI.Problem313.WeightedProjection.second_moment_synthesis line 54

   Source documentation

   The squared norm of a finite orthonormal expansion is its coefficient energy.

   theorem second_moment_synthesis [DecidableEq ι]
       (w : X → ℝ) (basis : ι → X → ℝ)
       (horth : ∀ i j, (∑ x, w x * basis i x * basis j x) = if i = j then 1 else 0)
       (L : Finset ι) (c : ι → ℝ) :
       (∑ x, w x * (synthesis basis L c x) ^ 2) = ∑ i ∈ L, (c i) ^ 2 := by
   …

   Mentions: OAI.Problem313.WeightedProjection.synthesis

6. theorem OAI.Problem313.WeightedProjection.inner_projection line 75

   Source documentation

   A spectral projection has the same inner product with the original function as its squared norm.

   theorem inner_projection (w : X → ℝ) (basis : ι → X → ℝ)
       (f : X → ℝ) (L : Finset ι) :
       (∑ x, w x * f x * synthesis basis L (coefficient w basis f) x) =
         ∑ i ∈ L, (coefficient w basis f i) ^ 2 := by
   …

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