FiniteFourier.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Fourier identities for the finite-tree obstruction

The scalar Fourier identities establish lem:finite-fourier.

def OAI.TreeEdit.BinaryLower.FiniteFourier.coefficient line 21
Source documentation
The normalized Fourier coefficient, with conjugation on the character.
```
def coefficient (f : A → ℂ) (χ : AddChar A ℂ) : ℂ :=
…
```
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.wInner_sum_left line 25
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.wInner_sum_right line 35
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.coefficient_eq_repr line 44
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.expansion line 52
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.parseval_complex line 57
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.parseval line 64
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.coefficient_sum line 73
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.coefficient_smul line 78
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.coefficient_char line 82
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.displacement_expansion line 86
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.coefficient_displacement line 99
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.displacement_parseval line 107
Source documentation
Parseval for the displacement by a fixed group element.
```
lemma displacement_parseval (f : A → ℂ) (z : A) :
    (∑ x : A, ‖f (x + z) - f x‖ ^ 2) / Fintype.card A =
      ∑ χ : AddChar A ℂ, ‖1 - χ z‖ ^ 2 * ‖coefficient f χ‖ ^ 2 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteFourier.coefficient
lemma OAI.TreeEdit.BinaryLower.FiniteFourier.indicator_difference line 116
Source documentation
Indicator differences have equal absolute value and squared complex norm.
```
lemma indicator_difference (u v : ℝ) (hu : u = 0 ∨ u = 1) (hv : v = 0 ∨ v = 1) :
    |u - v| = ‖(u : ℂ) - (v : ℂ)‖ ^ 2 := by
…
```

lemma OAI.TreeEdit.BinaryLower.FiniteFourier.indicator_displacement line 121

Source documentation

The identity for one zero-one valued cut.

lemma indicator_displacement (U : A → ℝ) (hU : ∀ x, U x = 0 ∨ U x = 1) (z : A) :
    (∑ x : A, |U (x + z) - U x|) / Fintype.card A =
      ∑ χ : AddChar A ℂ,
        ‖1 - χ z‖ ^ 2 * ‖coefficient (fun x => (U x : ℂ)) χ‖ ^ 2 := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteFourier.coefficient

theorem OAI.TreeEdit.BinaryLower.FiniteFourier.exists_weights_of_cutRepresentation line 129

Source documentation

Finite nonnegative cut combinations have a nonnegative Fourier representation.

theorem exists_weights_of_cutRepresentation {ι : Type*} [Fintype ι]
    (ρ : A → A → ℝ) (a : ι → ℝ) (ha : ∀ i, 0 ≤ a i)
    (U : ι → A → ℝ) (hU : ∀ i x, U i x = 0 ∨ U i x = 1)
    (hρ : ∀ x y, ρ x y = ∑ i : ι, a i * |U i x - U i y|) :
    ∃ H : AddChar A ℂ → ℝ, (∀ χ, 0 ≤ H χ) ∧
      ∀ z : A, (∑ x : A, ρ x (x + z)) / Fintype.card A =
        ∑ χ : AddChar A ℂ, ‖1 - χ z‖ ^ 2 * H χ := by
…