noncomputable def energy {G : Type u_1} [AddCommGroup G] (n : ℕ) (s : Finset G) (ν : G → ℂ) : ℝ

Equations

• energy n s ν = ∑ γ ∈ Fintype.piFinset fun (x : Fin n) => s, ∑ δ ∈ Fintype.piFinset fun (x : Fin n) => s, ‖ν (∑ i : Fin n, γ i - ∑ i : Fin n, δ i)‖

@[simp]

theorem energy_nonneg {G : Type u_1} [AddCommGroup G] (n : ℕ) (s : Finset G) (ν : G → ℂ) : 0 ≤ energy n s ν

theorem energy_nsmul {G : Type u_1} [AddCommGroup G] (m n : ℕ) (s : Finset G) (ν : G → ℂ) : energy n s (m • ν) = m • energy n s ν

@[simp]

theorem energy_zero {G : Type u_1} [AddCommGroup G] (s : Finset G) (ν : G → ℂ) : energy 0 s ν = ‖ν 0‖

noncomputable def boringEnergy {G : Type u_1} [AddCommGroup G] [DecidableEq G] (n : ℕ) (s : Finset G) : ℝ

Equations

• boringEnergy n s = energy n s trivChar

@[simp]

theorem boringEnergy_zero {G : Type u_1} [AddCommGroup G] [DecidableEq G] (s : Finset G) : boringEnergy 0 s = 1

theorem boringEnergy_eq {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] (n : ℕ) (s : Finset G) : boringEnergy n s = ∑ x : G, (((↑s).indicator fun (x : G) => 1) ∗ᵈ^ n) x ^ 2

@[simp]

theorem boringEnergy_one {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Finite G] (s : Finset G) : boringEnergy 1 s = ↑s.card

theorem cLpNorm_dft_indicator_one_pow {G : Type u_1} [AddCommGroup G] [DecidableEq G] [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (n : ℕ) (s : Finset G) : ‖dft ((↑s).indicator fun (x : G) => 1)‖ₙ_[↑(2 * n)] ^ (2 * n) = boringEnergy n s

theorem cL2Norm_dft_indicator_one {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (s : Finset G) : ‖dft ((↑s).indicator fun (x : G) => 1)‖ₙ_[2] = √↑s.card