FourierRestrictionMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.BiasedFourier.restricted_mass_average line 17

Source documentation

Exact averaging of any selected family of conditional Fourier levels.

theorem restricted_mass_average {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : (ι ⊕ κ → Bool) → ℝ) (L : Finset (Finset ι)) :
    (∑ y : κ → Bool, weight p y *
      ∑ A ∈ L, (coeff p (fun x => f (Sum.elim x y)) A) ^ 2) =
      ∑ A ∈ L, ∑ D : Finset κ, (coeff p f (A.disjSum D)) ^ 2 := by
…

Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff

theorem OAI.Problem313.BiasedFourier.restricted_mass_condition line 31

Source documentation

The restriction identity reindexed by full supports. The condition is placed only on the free-coordinate part, never on exterior Fourier degree.

theorem restricted_mass_condition {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : (ι ⊕ κ → Bool) → ℝ) (P : Finset ι → Prop) [DecidablePred P] :
    (∑ y : κ → Bool, weight p y *
      ∑ A : Finset ι, if P A then
        (coeff p (fun x => f (Sum.elim x y)) A) ^ 2 else 0) =
      ∑ S : Finset (ι ⊕ κ), if P S.toLeft then (coeff p f S) ^ 2 else 0 := by
…

Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff

theorem OAI.Problem313.BiasedFourier.restricted_low_degree_mass_average line 46

Source documentation

Literal real-valued conditional degree cutoff, including the case k < 1.

theorem restricted_low_degree_mass_average {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (f : (ι ⊕ κ → Bool) → ℝ) (k : ℝ) :
    (∑ y : κ → Bool, weight p y *
      ∑ A : Finset ι, if 1 ≤ A.card ∧ (A.card : ℝ) ≤ k then
        (coeff p (fun x => f (Sum.elim x y)) A) ^ 2 else 0) =
      ∑ S : Finset (ι ⊕ κ), if 1 ≤ S.toLeft.card ∧ (S.toLeft.card : ℝ) ≤ k then
        (coeff p f S) ^ 2 else 0 := by
…

Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff