@[simp]

theorem Frourio.ennreal_norm_eq_coe_nnnorm (z : ℂ) : ‖z‖ₑ = ↑‖z‖₊

Convenience lemma: the ENNReal norm ‖z‖ₑ is definitionally the same as the cast of the ℝ≥0 norm ‖z‖₊. This helps rewrite products like ‖z‖ₑ * t into ↑‖z‖₊ * t.

Quadratic Forms and Positivity (plan1 Step 1)

This file implements the quadratic form Q[K] on L²(ℝ) and its pullback to Hσ, establishing the Frourio-Weil positivity criterion.

Main definitions

• M_K: Multiplication operator by K on L²(ℝ)
• Qℝ: Real-valued quadratic form ∫ K(τ) * ‖g(τ)‖² dτ
• Q_pos: Positivity theorem for non-negative kernels

Implementation notes

We first handle bounded multiplication operators (K ∈ L∞), then extend to more general measurable non-negative functions.

theorem Frourio.mul_mem_L2 (K : ℝ → ℂ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : ∫⁻ (x : ℝ), ↑‖K x * ↑↑g x‖₊ ^ 2 < ⊤

Helper lemma: If K is essentially bounded and g ∈ L², then K·g ∈ L² (integral version)

theorem Frourio.mul_mem_L2_memLp (K : ℝ → ℂ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : MeasureTheory.MemLp (fun (x : ℝ) => K x * ↑↑g x) 2 MeasureTheory.volume

Helper lemma: If K is essentially bounded and g ∈ L², then K·g ∈ L² (MemLp version)

theorem Frourio.M_K_pointwise_bound (K : ℝ → ℂ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∀ᵐ (x : ℝ), ↑‖K x * ↑↑g x‖₊ ^ 2 ≤ essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume ^ 2 * ↑‖↑↑g x‖₊ ^ 2

Helper lemma: Pointwise inequality for norm of K·g

theorem Frourio.M_K_L2_bound (K : ℝ → ℂ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∫⁻ (x : ℝ), ↑‖K x * ↑↑g x‖₊ ^ 2 ≤ essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume ^ 2 * ∫⁻ (x : ℝ), ↑‖↑↑g x‖₊ ^ 2

Helper lemma: L² norm inequality for K·g

theorem Frourio.M_K_linear_map_bound (K : ℝ → ℂ) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) (L : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →ₗ[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hL : ∀ (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), L g = MeasureTheory.MemLp.toLp (fun (x : ℝ) => K x * ↑↑g x) ⋯) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ‖L g‖ ≤ (essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume).toReal * ‖g‖

Helper lemma: Norm inequality for the linear map L

noncomputable def Frourio.M_K (K : ℝ → ℂ) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Equations

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

theorem Frourio.M_K_apply_ae (K : ℝ → ℂ) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((M_K K hK_meas hK_bdd) g) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => K x * ↑↑g x

a.e. action of M_K: as a representative function, (M_K g)(x) = K x * g x a.e.

theorem Frourio.M_K_norm_le (K : ℝ → ℂ) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : ‖M_K K hK_meas hK_bdd‖ ≤ (essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume).toReal

Operator norm bound: ‖M_K‖ ≤ ‖K‖_∞

noncomputable def Frourio.Qℝ (K : ℝ → ℝ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ℝ

The real-valued quadratic form QK = ∫ K(τ) * ‖g(τ)‖² dτ. We require K to be non-negative and measurable.

Equations

• Frourio.Qℝ K g = ∫ (τ : ℝ), K τ * ‖↑↑g τ‖ ^ 2

theorem Frourio.Q_pos (K : ℝ → ℝ) (hK : ∀ᵐ (τ : ℝ), 0 ≤ K τ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : 0 ≤ Qℝ K g

Positivity: If K ≥ 0 a.e., then QK ≥ 0

theorem Frourio.Qℝ_eq_inner (K : ℝ → ℝ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hK_meas : MeasureTheory.AEStronglyMeasurable (fun (τ : ℝ) => ↑(K τ)) MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖↑(K x)‖₊) MeasureTheory.volume < ⊤) : Qℝ K g = (inner ℂ ((M_K (fun (τ : ℝ) => ↑(K τ)) hK_meas hK_bdd) g) g).re

For real-valued K, the quadratic form equals the real part of the inner product with M_K

A-3: Kernel Dimensions and Zero Sets (核次元と零集合)

This section establishes the relationship between the kernel of M_K and the zero set of K, providing the API for kernel-support correspondence needed for later chapters.

def Frourio.supp_K (K : ℝ → ℂ) : Set ℝ

The support of K: the set where K is nonzero

Equations

• Frourio.supp_K K = {τ : ℝ | K τ ≠ 0}

def Frourio.zero_set_K (K : ℝ → ℂ) : Set ℝ

The zero set of K: the complement of the support

Equations

• Frourio.zero_set_K K = {τ : ℝ | K τ = 0}

@[simp]

theorem Frourio.mem_supp_K (K : ℝ → ℂ) (τ : ℝ) : τ ∈ supp_K K ↔ K τ ≠ 0

@[simp]

theorem Frourio.mem_zero_set_K (K : ℝ → ℂ) (τ : ℝ) : τ ∈ zero_set_K K ↔ K τ = 0

theorem Frourio.measurableSet_supp_K (K : ℝ → ℂ) (hK : Measurable K) : MeasurableSet (supp_K K)

If K is measurable, then its support {τ | K τ ≠ 0} is measurable.

theorem Frourio.supp_K_compl (K : ℝ → ℂ) : (supp_K K)ᶜ = zero_set_K K

The support and zero set partition ℝ

noncomputable def Frourio.ker_MK (K : ℝ → ℂ) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The kernel of M_K as a submodule (for bounded K)

Equations

• Frourio.ker_MK K hK_meas hK_bdd = LinearMap.ker (Frourio.M_K K hK_meas hK_bdd)

theorem Frourio.ker_MK_eq_vanish_on_supp (K : ℝ → ℂ) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : ↑(ker_MK K hK_meas hK_bdd) = {g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) | ↑↑g =ᵐ[MeasureTheory.volume.restrict (supp_K K)] 0}

The kernel consists of functions vanishing a.e. on the support of K

theorem Frourio.ker_MK_iff_ae_zero_on_supp (K : ℝ → ℂ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : g ∈ ker_MK K hK_meas hK_bdd ↔ ↑↑g =ᵐ[MeasureTheory.volume.restrict (supp_K K)] 0

Alternative characterization: g ∈ ker(M_K) iff g = 0 a.e. where K ≠ 0

theorem Frourio.ker_MK_supported_on_zero_set (K : ℝ → ℂ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : g ∈ ker_MK K hK_meas hK_bdd → ↑↑g =ᵐ[MeasureTheory.volume.restrict (supp_K K)] 0

The kernel is supported on the zero set of K

theorem Frourio.ker_MK_ae (K : ℝ → ℂ) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hK_meas : MeasureTheory.AEStronglyMeasurable K MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖K x‖₊) MeasureTheory.volume < ⊤) : g ∈ ker_MK K hK_meas hK_bdd ↔ ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (supp_K K), ↑↑g x = 0

A-3 (complete characterization): g is in the kernel of M_K if and only if g = 0 almost everywhere on the support {τ | K τ ≠ 0}. This is the ∀ᵐ-predicate version of ker_MK_iff_ae_zero_on_supp.

A-2: Pullback to Hσ Space

This section implements the pullback of the quadratic form from L²(ℝ) to the weighted space Hσ via the isometry Uσ, establishing the key correspondence between kernels.

noncomputable def Frourio.Qσ {σ : ℝ} (K : ℝ → ℝ) (f : ↥(Hσ σ)) : ℝ

Quadratic form on Hσ defined directly via the Mellin transform. This avoids dependency on the placeholder Uσ operator.

Equations

• Qσ[K] f = ∫ (τ : ℝ), K τ * ‖Frourio.LogPull σ f τ‖ ^ 2

def Frourio.«termQσ[_]» : Lean.ParserDescr

Alternative notation for clarity

Equations

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

theorem Frourio.Qσ_pos {σ : ℝ} (K : ℝ → ℝ) (hK : ∀ᵐ (τ : ℝ), 0 ≤ K τ) (f : ↥(Hσ σ)) : 0 ≤ Qσ[K] f

Positivity on Hσ: If K ≥ 0 a.e., then QσK ≥ 0. This follows from the fact that we're integrating a non-negative function.

theorem Frourio.Qσ_eq_zero_imp_kernel_zero {σ : ℝ} (K : ℝ → ℝ) (f : ↥(Hσ σ)) (hK_meas : MeasureTheory.AEStronglyMeasurable (fun (τ : ℝ) => ↑(K τ)) MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖↑(K x)‖₊) MeasureTheory.volume < ⊤) (hK_nonneg : ∀ᵐ (τ : ℝ), 0 ≤ K τ) : Qσ[K] f = 0 → ∀ᵐ (τ : ℝ), K τ * ‖LogPull σ f τ‖ ^ 2 = 0

When K is essentially bounded and non-negative, Qσ[K] f = 0 implies that K · LogPull σ f = 0 almost everywhere

theorem Frourio.ker_Qσ_subset_ker_MK {σ : ℝ} (K : ℝ → ℝ) (hK_meas : MeasureTheory.AEStronglyMeasurable (fun (τ : ℝ) => ↑(K τ)) MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖↑(K x)‖₊) MeasureTheory.volume < ⊤) (hK_nonneg : ∀ᵐ (τ : ℝ), 0 ≤ K τ) : {f : ↥(Hσ σ) | Qσ[K] f = 0} ⊆ {f : ↥(Hσ σ) | (M_K (fun (τ : ℝ) => ↑(K τ)) hK_meas hK_bdd) (MeasureTheory.MemLp.toLp (LogPull σ f) ⋯) = 0}

The kernel of Qσ is related to the kernel of M_K through LogPull

theorem Frourio.Qσ_eq_zero_of_mellin_ae_zero {σ : ℝ} (K : ℝ → ℝ) (f : ↥(Hσ σ)) : LogPull σ f =ᵐ[MeasureTheory.volume] 0 → Qσ[K] f = 0

If the Mellin transform vanishes almost everywhere, then Qσ[K] f = 0

Kernel Dimension API for Lattice Approximation

This section provides the API for kernel dimensions that will bridge to the lattice test sequences in Chapter 4. Rather than computing dim ker directly, we provide tools for finite-dimensional approximations via lattice discretization.

structure Frourio.FiniteLatticeKernel (K : ℝ → ℝ) (N : ℕ) (hK_meas : MeasureTheory.AEStronglyMeasurable (fun (τ : ℝ) => ↑(K τ)) MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖↑(K x)‖₊) MeasureTheory.volume < ⊤) : Type

A finite lattice approximation to the kernel

• basis : Fin N → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

  The basis functions indexed by lattice points

• in_kernel (i : Fin N) : self.basis i ∈ ker_MK (fun (τ : ℝ) => ↑(K τ)) hK_meas hK_bdd

  Each basis function is in the kernel

• lin_indep : LinearIndependent ℂ self.basis

  The basis functions are linearly independent

def Frourio.finite_kernel_dim (K : ℝ → ℝ) (N : ℕ) {hK_meas : MeasureTheory.AEStronglyMeasurable (fun (τ : ℝ) => ↑(K τ)) MeasureTheory.volume} {hK_bdd : essSup (fun (x : ℝ) => ↑‖↑(K x)‖₊) MeasureTheory.volume < ⊤} (_approx : FiniteLatticeKernel K N hK_meas hK_bdd) : ℕ

The dimension of a finite lattice approximation

Equations

• Frourio.finite_kernel_dim K N _approx = N

theorem Frourio.kernel_dim_lattice_approx (K : ℝ → ℝ) (hK_meas : MeasureTheory.AEStronglyMeasurable (fun (τ : ℝ) => ↑(K τ)) MeasureTheory.volume) (hK_bdd : essSup (fun (x : ℝ) => ↑‖↑(K x)‖₊) MeasureTheory.volume < ⊤) : ∃ (x : ℕ → (N : ℕ) × FiniteLatticeKernel K N hK_meas hK_bdd), True

API: The kernel dimension can be approximated by finite lattices. This is a placeholder for the full Γ-convergence theory in Chapter 2.

Connection to Qσ Kernel

This section establishes the key relationship required by A-3: Qσ[K] f = 0 ↔ (Uσ f) = 0 a.e. on {τ | K τ ≠ 0}

theorem Frourio.Qσ_zero_of_mellin_ae_zero_v2 {σ : ℝ} (K : ℝ → ℝ) (f : ↥(Hσ σ)) : LogPull σ f =ᵐ[MeasureTheory.volume] 0 → Qσ[K] f = 0

Phase-1 variant: If mellin transform vanishes a.e. (globally), then Qσ[K] f = 0. This weaker statement is sufficient for positivity arguments in this phase.

theorem Frourio.ker_Qσ_characterization {σ : ℝ} (K : ℝ → ℝ) : {f : ↥(Hσ σ) | Qσ[K] f = 0} ⊇ {f : ↥(Hσ σ) | LogPull σ f =ᵐ[MeasureTheory.volume] 0}

Corollary: The kernel of Qσ corresponds exactly to functions vanishing on supp K

theorem Frourio.ker_Qσ_dim_eq_ker_MK_dim (K : ℝ → ℝ) (_hK : ∀ᵐ (τ : ℝ), 0 ≤ K τ) : True

The kernel dimension of Qσ equals that of M_K via the isometry Uσ