@[reducible, inline]

abbrev Frourio.MeasureR : Type

Equations

• Frourio.MeasureR = MeasureTheory.Measure ℝ

noncomputable def Frourio.L2NormR (_f : ℝ → ℂ) : ℝ

Equations

• Frourio.L2NormR _f = 0

noncomputable def Frourio.TVNorm (_ν : MeasureR) : ℝ

Equations

• Frourio.TVNorm _ν = 0

noncomputable def Frourio.L2NormZ (a : ℤ → ℂ) : ℝ

Equations

• Frourio.L2NormZ a = √(∑' (n : ℤ), ‖a n‖ ^ 2)

noncomputable def Frourio.L1NormZ (μ : ℤ → ℂ) : ℝ

Equations

• Frourio.L1NormZ μ = ∑' (n : ℤ), ‖μ n‖

noncomputable def Frourio.convR_measure (_f : ℝ → ℂ) (_ν : MeasureR) : ℝ → ℂ

Equations

• Frourio.convR_measure _f _ν _x = 0

noncomputable def Frourio.convZ (a μ : ℤ → ℂ) : ℤ → ℂ

Equations

• Frourio.convZ a μ n = ∑' (k : ℤ), a k * μ (n - k)

structure Frourio.DiracLike : Type

• phase : ℝ
• s0 : ℝ

noncomputable def Frourio.oneFunc : ℝ → ℂ

A concrete nonzero test function on ℝ → ℂ: the constant-one map.

Equations

• Frourio.oneFunc x✝ = 1

theorem Frourio.oneFunc_ne_zero : oneFunc ≠ fun (x : ℝ) => 0

def Frourio.convR_measure_is_linear (ν : MeasureR) : Prop

Linearity of convR_measure in the function argument (statement-only).

Equations

• One or more equations did not get rendered due to their size.