OAI/Combinatorics/SharpThreshold/DirichletEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.sum_supports_containing line 13

   Source documentation

   Delete a distinguished coordinate to reindex all supports containing it.

   theorem sum_supports_containing (i : ι) (a : Finset ι → ℝ) :
       (∑ S : Finset ι, if i ∈ S then a S else 0) =
         ∑ S : Finset ι, if i ∉ S then a (insert i S) else 0 := by
   …

2. theorem OAI.Problem313.spectral_coordinate_energy line 31

   Source documentation

   Algebraic coordinate energy identity from the derivative Fourier identities.

   theorem spectral_coordinate_energy (i : ι) (a b : Finset ι → ℝ) (σ : ℝ)
       (hzero : ∀ S, i ∈ S → b S = 0)
       (hinsert : ∀ S, i ∉ S → a (insert i S) = σ * b S) :
       (∑ S : Finset ι, if i ∈ S then (a S)^2 else 0) =
         σ^2 * ∑ S : Finset ι, (b S)^2 := by
   …

3. theorem OAI.Problem313.sum_card_mul_eq_sum_mem line 44

   Source documentation

   Counting each spectral support once for every coordinate it contains.

   theorem sum_card_mul_eq_sum_mem (a : Finset ι → ℝ) :
       (∑ S : Finset ι, (S.card : ℝ) * a S) =
         ∑ i : ι, ∑ S : Finset ι, if i ∈ S then a S else 0 := by
   …

4. theorem OAI.Problem313.spectral_dirichlet line 53

   Source documentation

   Summing coordinate energies gives the finite Dirichlet identity.

   theorem spectral_dirichlet (a : Finset ι → ℝ) (I : ι → ℝ) (σ : ℝ)
       (hcoord : ∀ i, (∑ S : Finset ι, if i ∈ S then (a S)^2 else 0) = σ^2 * I i) :
       (∑ S : Finset ι, (S.card : ℝ) * (a S)^2) = σ^2 * ∑ i, I i := by
   …