OAI/Combinatorics/SharpThreshold/RestrictionMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem313.RestrictionMass.weighted_sum_sq_expansion line 14

   Source documentation

   Parseval for a finite orthonormal family, with an explicit real weight.

   theorem weighted_sum_sq_expansion
       {B : Type u} {Y : Type v} [Fintype B] [DecidableEq B] [Fintype Y]
       (w : Y → ℝ) (χ : B → Y → ℝ)
       (horth : ∀ b d, (∑ y, w y * χ b y * χ d y) = if b = d then 1 else 0)
       (c : B → ℝ) :
       (∑ y, w y * (∑ b, c b * χ b y) ^ 2) = ∑ b, c b ^ 2 := by
   …

2. theorem OAI.Problem313.RestrictionMass.average_restriction_mass line 43

   Source documentation

   Averaging the squared restricted coefficients eliminates exterior Fourier cross terms. No sign or normalization assumption on w is needed here.

   theorem average_restriction_mass
       {A : Type w} {B : Type u} {Y : Type v} [Fintype B] [DecidableEq B] [Fintype Y]
       (w : Y → ℝ) (χ : B → Y → ℝ)
       (horth : ∀ b d, (∑ y, w y * χ b y * χ d y) = if b = d then 1 else 0)
       (c : A → B → ℝ) (L : Finset A) :
       (∑ y, w y * ∑ a ∈ L, (∑ b, c a b * χ b y) ^ 2) =
         ∑ a ∈ L, ∑ b, c a b ^ 2 := by
   …

3. theorem OAI.Problem313.RestrictionMass.average_restriction_mass_of_expansion line 58

   Source documentation

   The same identity with restricted coefficients supplied as a separate function.

   theorem average_restriction_mass_of_expansion
       {A : Type w} {B : Type u} {Y : Type v} [Fintype B] [DecidableEq B] [Fintype Y]
       (w : Y → ℝ) (χ : B → Y → ℝ)
       (horth : ∀ b d, (∑ y, w y * χ b y * χ d y) = if b = d then 1 else 0)
       (c : A → B → ℝ) (r : A → Y → ℝ)
       (hr : ∀ a y, r a y = ∑ b, c a b * χ b y) (L : Finset A) :
       (∑ y, w y * ∑ a ∈ L, r a y ^ 2) = ∑ a ∈ L, ∑ b, c a b ^ 2 := by
   …