FiniteFourierAssembly.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the finite-group displacement identity

Summing finite cut representations and the Parseval identities for cut indicators gives the finite-group displacement identity.

theorem OAI.TreeEdit.BinaryLower.cut_spectral_weight_nonneg line 22

Source documentation

Summing nonnegative spectral weights with nonnegative cut coefficients preserves nonnegativity.

theorem cut_spectral_weight_nonneg {C K : Type*} [Fintype C]
    (a : C → ℝ) (b : C → K → ℝ)
    (ha : ∀ c, 0 ≤ a c) (hb : ∀ c k, 0 ≤ b c k) (k : K) :
    0 ≤ ∑ c, a c * b c k := by
…

theorem OAI.TreeEdit.BinaryLower.sum_cut_spectral_weights line 29

Source documentation

Interchange a finite cut sum and a finite spectral sum.

theorem sum_cut_spectral_weights {C K : Type*} [Fintype C] [Fintype K]
    (a : C → ℝ) (b : C → K → ℝ) (multiplier : K → ℝ) :
    (∑ c, a c * ∑ k, multiplier k * b c k) =
      ∑ k, multiplier k * ∑ c, a c * b c k := by
…

theorem OAI.TreeEdit.BinaryLower.finite_fourier_of_cut_expansions line 44

Source documentation

A finite cut expansion together with the spectral expansion of each cut implies the averaged displacement representation. Neither injectivity of F nor nontriviality of the individual cuts is needed.

theorem finite_fourier_of_cut_expansions
    {A C E : Type*} [AddCommGroup A] [Fintype A] [Fintype C]
    [NormedAddCommGroup E]
    (F : A → E) (a : C → ℝ) (U : C → A → ℝ)
    (b : C → AddChar A ℂ → ℝ)
    (ha : ∀ c, 0 ≤ a c) (hb : ∀ c χ, 0 ≤ b c χ)
    (hcut : ∀ x y, ‖F x - F y‖ = ∑ c, a c * |U c x - U c y|)
    (hfourier : ∀ c z,
      (𝔼 x, |U c (x + z) - U c x|) =
        ∑ χ : AddChar A ℂ, ‖1 - χ z‖ ^ 2 * b c χ) :
    ∃ H : AddChar A ℂ → ℝ, (∀ χ, 0 ≤ H χ) ∧
      ∀ z, (𝔼 x, ‖F (x + z) - F x‖) =
…

theorem OAI.TreeEdit.BinaryLower.character_displacement_nonneg line 78
Source documentation
Every character displacement multiplier is nonnegative.
```
theorem character_displacement_nonneg {A : Type*} [AddCommGroup A]
    (χ : AddChar A ℂ) (z : A) : 0 ≤ ‖1 - χ z‖ ^ 2 := sq_nonneg _
```

theorem OAI.TreeEdit.BinaryLower.character_displacement_le_four line 82

Source documentation

The multiplier bound used in the finite root-mass estimate.

theorem character_displacement_le_four {A : Type*} [AddCommGroup A] [Finite A]
    (χ : AddChar A ℂ) (z : A) : ‖1 - χ z‖ ^ 2 ≤ 4 := by
…

theorem OAI.TreeEdit.BinaryLower.character_displacement_eq_zero_iff line 92
Source documentation
Root-inactive characters have zero multiplier, and only those characters do.
```
theorem character_displacement_eq_zero_iff {A : Type*} [AddCommGroup A]
    (χ : AddChar A ℂ) (z : A) : ‖1 - χ z‖ ^ 2 = 0 ↔ χ z = 1 := by
…
```