8.8.1. Lemma A.1 — Partial Fourier transform of a square-integrable coefficient (lem:partial-fourier-l2)🔗

Blueprint node: Lemma 2.2.7. Status: verified (all 2 Lean theorems verified).

OperatorRidgelet.Paper.lem_partial_fourier_l2, theorem in Challenge/Revision.lean:

omit [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [BorelSpace H] in
/-- **Lemma [lem:partial-fourier-l2]** Bias Fourier transformation is a genuine unitary
with jointly measurable representatives and the angular normalization. -/
theorem lem_partial_fourier_l2 (ν : Measure H) [SigmaFinite ν] :
    ∃ U : Lp Y 2 (parameterMeasure ν) ≃ₗᵢ[ℂ]
      Lp Y 2 (ν.prod (ENNReal.ofReal (2 * Real.pi)⁻¹ • (volume : Measure ℝ))),
      ∀ γ : Lp Y 2 (parameterMeasure ν),
        ∃ Φ : H → ℝ → Y, StronglyMeasurable (Function.uncurry Φ) ∧
          HasBiasFourierVec ν γ Φ ∧
          Function.uncurry Φ =ᵐ[ν.prod (ENNReal.ofReal (2 * Real.pi)⁻¹ • volume)] ⇑(U γ) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_partial_fourier_l2_uniqueness, theorem in Challenge/Revision.lean:

omit [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [BorelSpace H] in
/-- **Lemma [lem:partial-fourier-l2]** The Fourier representatives agree on almost every section. -/
theorem lem_partial_fourier_l2_uniqueness (ν : Measure H) [SigmaFinite ν]
    (γ : H × ℝ → Y) (Φ Φ' : H → ℝ → Y) (hΦ : HasBiasFourierVec ν γ Φ)
    (hΦ' : HasBiasFourierVec ν γ Φ') :
    ∀ᵐ a ∂ν, Φ a =ᵐ[volume] Φ' a := by

Status: verified by comparator.

8.8.2. Lemma A.2 — Measurability and integration of the mixture (lem:mixture-integration)🔗

Blueprint node: Lemma 2.1.3. Status: verified (all 4 Lean theorems verified).

Formalization note. Measurability on (0,∞), the bind formula on Borel sets, the lintegral formula, and the Bochner-integral formula for integrable complex F.

OperatorRidgelet.Paper.lem_mixture_integration_i, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:mixture-integration]** Measurability and integration of the mixture.  For every
Borel set `E`, the map `s ↦ 𝒩(0,2sP)(E)` is Borel measurable on `(0,∞)`. -/
theorem lem_mixture_integration_i {P : H →L[ℝ] H} (hP : IsTraceClassCovariance P)
    {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) :
    ∀ E : Set H, MeasurableSet E → Measurable fun s : Set.Ioi (0 : ℝ) => N s E := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_mixture_integration_ii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:mixture-integration]** Measurability and integration of the mixture.  The
mixture is a countably additive Borel measure given on Borel sets by
`ν_α(E) = ∫₀^∞ 𝒩(0,2sP)(E) s^{α/2-1} ds`. -/
theorem lem_mixture_integration_ii {P : H →L[ℝ] H} (hP : IsTraceClassCovariance P)
    {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) :
    ∀ E : Set H, MeasurableSet E →
      gaussianMixture N α E =
        ∫⁻ s in Set.Ioi (0 : ℝ), N s E * ENNReal.ofReal (s ^ (α / 2 - 1)) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_mixture_integration_iii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:mixture-integration]** Measurability and integration of the mixture.  For every
nonnegative Borel `F`, `∫ F dν_α = ∫₀^∞ (∫ F d𝒩(0,2sP)) s^{α/2-1} ds`, both sides possibly
infinite. -/
theorem lem_mixture_integration_iii {P : H →L[ℝ] H} (hP : IsTraceClassCovariance P)
    {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) :
    ∀ F : H → ℝ≥0∞, Measurable F →
      ∫⁻ ξ, F ξ ∂gaussianMixture N α =
        ∫⁻ s in Set.Ioi (0 : ℝ), (∫⁻ ξ, F ξ ∂N s) * ENNReal.ofReal (s ^ (α / 2 - 1)) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_mixture_integration_iv, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:mixture-integration]** Measurability and integration of the mixture.  For
complex `F` the integration formula holds when `∫ |F| dν_α < ∞`. -/
theorem lem_mixture_integration_iv {P : H →L[ℝ] H} (hP : IsTraceClassCovariance P)
    {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) :
    ∀ F : H → ℂ, Integrable F (gaussianMixture N α) →
      ∫ ξ, F ξ ∂gaussianMixture N α =
        ∫ s in Set.Ioi (0 : ℝ), (∫ ξ, F ξ ∂N s) * ((s ^ (α / 2 - 1) : ℝ) : ℂ) := by

Status: verified by comparator.

8.8.3. Lemma A.3 — Gaussian-layer regularization (lem:mixture-character)🔗

Blueprint node: Lemma 2.1.5. Status: verified (all 4 Lean theorems verified).

Formalization note. The double limit ε ↓ 0, M ↑ ∞ is a Tendsto along (𝓝[>] 0) ×ˢ atTop of the characteristic functionals of the truncated mixtures gaussianMixtureOn N α (Ioo ε M).

OperatorRidgelet.Paper.lem_mixture_character_i, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:mixture-character]** Gaussian-layer regularization.  For `z ≠ 0` the quadratic
form `q = ⟨Pz,z⟩` is positive. -/
theorem lem_mixture_character_i {P : H →L[ℝ] H} (hP : IsTraceClassCovariance P) (z : H)
    (hz : z ≠ 0) :
    0 < ⟪P z, z⟫ := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_mixture_character_ii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:mixture-character]** Gaussian-layer regularization.  The characteristic
functionals of the truncated mixtures `ν_α^{ε,M} = ∫_ε^M 𝒩(0,2sP) s^{α/2-1} ds` converge, as
`ε ↓ 0` and `M ↑ ∞`, to `Γ(α/2) q^{-α/2}`. -/
theorem lem_mixture_character_ii {P : H →L[ℝ] H} (hP : IsTraceClassCovariance P)
    {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N) {α : ℝ} (hα : 0 < α) (z : H)
    (hz : z ≠ 0) :
    Tendsto (fun εM : ℝ × ℝ => charFun (gaussianMixtureOn N α (Set.Ioo εM.1 εM.2)) z)
      ((𝓝[>] (0 : ℝ)) ×ˢ atTop)
      (𝓝 ((Real.Gamma (α / 2) * ⟪P z, z⟫ ^ (-(α / 2)) : ℝ) : ℂ)) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_mixture_character_iii, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:mixture-character]** Gaussian-layer regularization.  The limit is the Gamma
integral `∫₀^∞ e^{-sq} s^{α/2-1} ds = Γ(α/2) q^{-α/2}`. -/
theorem lem_mixture_character_iii {P : H →L[ℝ] H} (hP : IsTraceClassCovariance P) {α : ℝ}
    (hα : 0 < α) (z : H) (hz : z ≠ 0) :
    ∫ s in Set.Ioi (0 : ℝ), Real.exp (-s * ⟪P z, z⟫) * s ^ (α / 2 - 1) =
      Real.Gamma (α / 2) * ⟪P z, z⟫ ^ (-(α / 2)) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_mixture_character_iv, theorem in Challenge/Transform.lean:

/-- **Lemma [lem:mixture-character]** Gaussian-layer regularization.  In contrast, the character
`ξ ↦ e^{i⟨z,ξ⟩}` is not integrable against `ν_α`, so the limit is not a Lebesgue integral. -/
theorem lem_mixture_character_iv (hH : ¬ FiniteDimensional ℝ H) {P : H →L[ℝ] H}
    (hP : IsTraceClassCovariance P) {N : ℝ → Measure H} (hN : IsCenteredGaussianLayers P N)
    {α : ℝ} (hα : 0 < α) (z : H) (hz : z ≠ 0) :
    ¬ Integrable (fun ξ : H => Complex.exp ((⟪z, ξ⟫ : ℝ) * Complex.I)) (gaussianMixture N α) := by

Status: verified by comparator.