FourierReindex.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem313.BiasedFourier.weight_reindex line 18
Source documentation
Product Bernoulli weight is unchanged by renaming its coordinates.
```
theorem weight_reindex (e : ι ≃ κ) (p : ℝ) (x : ι → Bool) :
    weight p (Reindex.config e x) = weight p x := by
…
```
Mentions: OAI.Problem313.BiasedFourier.weight, OAI.Problem313.Reindex.config
theorem OAI.Problem313.BiasedFourier.char_reindex line 25
Source documentation
Fourier characters are natural under a bijection of coordinate sets.
```
theorem char_reindex (e : ι ≃ κ) (p : ℝ) (S : Finset ι) (x : ι → Bool) :
    char p (S.map e.toEmbedding) (Reindex.config e x) = char p S x := by
…
```
Mentions: OAI.Problem313.BiasedFourier.char, OAI.Problem313.Reindex.config

theorem OAI.Problem313.BiasedFourier.expectation_reindex line 30

Source documentation

Every weighted finite expectation is unchanged by coordinate transport.

theorem expectation_reindex (e : ι ≃ κ) (p : ℝ)
    (f : (ι → Bool) → ℝ) (g : (κ → Bool) → ℝ)
    (hfg : ∀ x, g (Reindex.config e x) = f x) :
    (∑ y, weight p y * g y) = ∑ x, weight p x * f x := by
…

Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.BiasedFourier.weight

theorem OAI.Problem313.BiasedFourier.coeff_reindex line 42

Source documentation

Transport of Fourier coefficients, with the support transported by Finset.map.

theorem coeff_reindex (e : ι ≃ κ) (p : ℝ)
    (f : (ι → Bool) → ℝ) (g : (κ → Bool) → ℝ)
    (hfg : ∀ x, g (Reindex.config e x) = f x) (S : Finset ι) :
    coeff p g (S.map e.toEmbedding) = coeff p f S := by
…

Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.BiasedFourier.coeff

theorem OAI.Problem313.BiasedFourier.spectral_sum_reindex line 55

Source documentation

Coordinate transport of spectral synthesis, including a degree-dependent multiplier.

theorem spectral_sum_reindex (e : ι ≃ κ) (p : ℝ) (M : ℕ → ℝ)
    (c : Finset ι → ℝ) (d : Finset κ → ℝ)
    (hcd : ∀ S, d (S.map e.toEmbedding) = c S) (x : ι → Bool) :
    (∑ T : Finset κ, M T.card * d T * char p T (Reindex.config e x)) =
      ∑ S : Finset ι, M S.card * c S * char p S x := by
…

Mentions: OAI.Problem313.BiasedFourier.char, OAI.Problem313.Reindex.config

theorem OAI.Problem313.BiasedFourier.noise_sum_reindex line 68

Source documentation

Spectral noise is natural under arbitrary finite-coordinate equivalences.

theorem noise_sum_reindex (e : ι ≃ κ) (p ρ : ℝ)
    (f : (ι → Bool) → ℝ) (g : (κ → Bool) → ℝ)
    (hfg : ∀ x, g (Reindex.config e x) = f x) (x : ι → Bool) :
    (∑ T : Finset κ, ρ ^ T.card * coeff p g T * char p T (Reindex.config e x)) =
      ∑ S : Finset ι, ρ ^ S.card * coeff p f S * char p S x := by
…

Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.char

theorem OAI.Problem313.BiasedFourier.noise_fourth_moment_reindex line 77

Source documentation

The fourth-moment hypercontractive statement transports along coordinate equivalences.

theorem noise_fourth_moment_reindex (e : ι ≃ κ) (p ρ : ℝ)
    (f : (ι → Bool) → ℝ) (g : (κ → Bool) → ℝ)
    (hfg : ∀ x, g (Reindex.config e x) = f x)
    (hf : (∑ x, weight p x *
        (∑ S : Finset ι, ρ ^ S.card * coeff p f S * char p S x) ^ 4) ≤
        (∑ x, weight p x * (f x) ^ 2) ^ 2) :
    (∑ y, weight p y *
        (∑ T : Finset κ, ρ ^ T.card * coeff p g T * char p T y) ^ 4) ≤
        (∑ y, weight p y * (g y) ^ 2) ^ 2 := by
…

Mentions: OAI.Problem313.Reindex.config, OAI.Problem313.BiasedFourier.weight, OAI.Problem313.BiasedFourier.coeff, OAI.Problem313.BiasedFourier.char

theorem OAI.Problem313.BiasedFourier.noise_fourth_moment_of_fin line 97

Source documentation

A proof of spectral hypercontractivity on every Fin n cube suffices for every finite coordinate type. This isolates the reindexing burden from the product induction.

theorem noise_fourth_moment_of_fin (p ρ : ℝ)
    (hfin : ∀ (n : ℕ) (f : (Fin n → Bool) → ℝ),
      (∑ x, weight p x *
        (∑ S : Finset (Fin n), ρ ^ S.card * coeff p f S * char p S x) ^ 4) ≤
        (∑ x, weight p x * (f x) ^ 2) ^ 2)
    (g : (ι → Bool) → ℝ) :
    (∑ x, weight p x *
        (∑ S : Finset ι, ρ ^ S.card * coeff p g S * char p S x) ^ 4) ≤
        (∑ x, weight p x * (g x) ^ 2) ^ 2 := by
…

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

theorem OAI.Problem313.BiasedFourier.coefficient_energy_reindex line 112

Source documentation

Every degree-weighted squared coefficient sum is invariant under coordinate transport.

theorem coefficient_energy_reindex (e : ι ≃ κ) (M : ℕ → ℝ)
    (c : Finset ι → ℝ) (d : Finset κ → ℝ)
    (hcd : ∀ S, d (S.map e.toEmbedding) = c S) :
    (∑ T : Finset κ, M T.card * (d T) ^ 2) =
      ∑ S : Finset ι, M S.card * (c S) ^ 2 := by
…

theorem OAI.Problem313.BiasedFourier.synthesis_contraction_reindex line 125

Source documentation

The universal coefficient form of hypercontractivity transports along coordinate bijections. It is the equivalence branch of finite-type induction.

theorem synthesis_contraction_reindex (e : ι ≃ κ) (p ρ : ℝ)
    (hι : ∀ c : Finset ι → ℝ,
      (∑ x, weight p x *
        (∑ S : Finset ι, ρ ^ S.card * c S * char p S x) ^ 4) ≤
        (∑ S : Finset ι, (c S) ^ 2) ^ 2)
    (d : Finset κ → ℝ) :
    (∑ y, weight p y *
        (∑ T : Finset κ, ρ ^ T.card * d T * char p T y) ^ 4) ≤
        (∑ T : Finset κ, (d T) ^ 2) ^ 2 := by
…

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