8.14.1. Corollary G.2 — The frame operator in finite dimension (cor:finite-backprojection)🔗

Blueprint node: Corollary 2.5.2. Status: verified (all 6 Lean theorems verified).

Formalization note. On EuclideanSpace ℝ (Fin m) with ν_α = c_{m,α}‖a‖^{α-m} da (directionMeasure); the nondegenerate Gaussian density p is IsCenteredGaussian Q (p dx) with Q a trace-class covariance and p continuous, positive; (-Δ)^s is the Fourier multiplier ‖ξ‖^{2s} (fracLaplacian); S_ρ R_ρ f is encoded through its defining pairing h ↦ ⟨R_ρ f, R_ρ h⟩_{L²(λ)} on 𝒟_α (the synthesis operator itself belongs to the reconstruction work package); the distributional formula is tested against Schwartz functions.

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

/-- **Corollary [cor:finite-backprojection]** The frame operator in finite dimension.  If
`f ∈ L²(p dx)` with `g = f p ∈ 𝒮(ℝ^m)`, then `f ∈ 𝒟_α`. -/
theorem cor_finite_backprojection_i {m : ℕ} {α : ℝ} (hα : 0 < α) (hαm : α < m)
    (p : Euclid m → ℝ) (hp : ∀ x, 0 < p x) (hpc : Continuous p) {Q : Euclid m →L[ℝ] Euclid m}
    (hQ : IsTraceClassCovariance Q) [IsProbabilityMeasure (densityMeasure p)]
    (hpQ : IsCenteredGaussian Q (densityMeasure p)) (f : Euclid m → ℂ)
    (hf : MemLp f 2 (densityMeasure p)) (g : SchwartzMap (Euclid m) ℂ)
    (hg : ∀ x, g x = f x * p x) :
    hf.toLp f ∈ spectralCore (densityMeasure p) (directionMeasure m α) := by

Status: verified by comparator.

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

/-- **Corollary [cor:finite-backprojection]** The frame operator in finite dimension.  The
representative of the frame operator against the pivot measure is the Riesz potential
`t_f = ∫ e^{i⟨x,ξ⟩} ĝ(ξ) ν_α(dξ) = k_{m,α} (-Δ)^{-(m-α)/2} g`. -/
theorem cor_finite_backprojection_ii {m : ℕ} {α : ℝ} (hα : 0 < α) (hαm : α < m)
    (p : Euclid m → ℝ) (hp : ∀ x, 0 < p x) (hpc : Continuous p) {Q : Euclid m →L[ℝ] Euclid m}
    (hQ : IsTraceClassCovariance Q) [IsProbabilityMeasure (densityMeasure p)]
    (hpQ : IsCenteredGaussian Q (densityMeasure p)) (f : Euclid m → ℂ)
    (hf : MemLp f 2 (densityMeasure p)) (g : SchwartzMap (Euclid m) ℂ)
    (hg : ∀ x, g x = f x * p x) :
    ∀ x, frameRepresentative (directionMeasure m α) g x =
      frameConst m α * fracLaplacian (-((m - α) / 2)) g x := by

Status: verified by comparator.

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

/-- **Corollary [cor:finite-backprojection]** The frame operator in finite dimension.  For a
band-pass `ρ`, the synthesis `S_ρ R_ρ f`, i.e. the functional `h ↦ ⟨R_ρ f, R_ρ h⟩_{L²(λ_α)}` on
`𝒟_α`, is represented against the pivot measure by `C^{(α)}_ρ t_f`. -/
theorem cor_finite_backprojection_iii {m : ℕ} {α : ℝ} (hα : 0 < α) (hαm : α < m)
    (p : Euclid m → ℝ) (hp : ∀ x, 0 < p x) (hpc : Continuous p) {Q : Euclid m →L[ℝ] Euclid m}
    (hQ : IsTraceClassCovariance Q) [IsProbabilityMeasure (densityMeasure p)]
    (hpQ : IsCenteredGaussian Q (densityMeasure p)) (f : Euclid m → ℂ)
    (hf : MemLp f 2 (densityMeasure p)) (g : SchwartzMap (Euclid m) ℂ)
    (hg : ∀ x, g x = f x * p x) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) :
    ∀ h : Lp ℂ 2 (densityMeasure p), h ∈ spectralCore (densityMeasure p) (directionMeasure m α) →
      ∫ q, ridgelet (densityMeasure p) ρ f q * (starRingEnd ℂ) (ridgelet (densityMeasure p) ρ h q)
          ∂parameterMeasure (directionMeasure m α) =
        admissibilityConst α ρ *
          ∫ x, frameRepresentative (directionMeasure m α) g x * (starRingEnd ℂ) (h x)
            ∂densityMeasure p := by

Status: verified by comparator.

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

/-- **Corollary [cor:finite-backprojection]** The frame operator in finite dimension.  The
distributional reconstruction `f = p^{-1} (k_{m,α} C^{(α)}_ρ)^{-1} (-Δ)^{(m-α)/2} S_ρ R_ρ f`,
with `S_ρ R_ρ f` represented by `C^{(α)}_ρ t_f`: tested against Schwartz functions `φ`,
`∫ f φ p dx = (k C)^{-1} ∫ (C t_f) (-Δ)^{(m-α)/2} φ dx`. -/
theorem cor_finite_backprojection_iv {m : ℕ} {α : ℝ} (hα : 0 < α) (hαm : α < m)
    (p : Euclid m → ℝ) (hp : ∀ x, 0 < p x) (hpc : Continuous p) {Q : Euclid m →L[ℝ] Euclid m}
    (hQ : IsTraceClassCovariance Q) [IsProbabilityMeasure (densityMeasure p)]
    (hpQ : IsCenteredGaussian Q (densityMeasure p)) (f : Euclid m → ℂ)
    (hf : MemLp f 2 (densityMeasure p)) (g : SchwartzMap (Euclid m) ℂ)
    (hg : ∀ x, g x = f x * p x) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) :
    ∀ φ : SchwartzMap (Euclid m) ℂ,
      ∫ x, f x * φ x ∂densityMeasure p =
        ((frameConst m α * admissibilityConst α ρ)⁻¹ : ℝ) *
          ∫ x, (admissibilityConst α ρ * frameRepresentative (directionMeasure m α) g x) *
            fracLaplacian ((m - α) / 2) φ x := by

Status: verified by comparator.

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

/-- **Corollary [cor:finite-backprojection]** The frame operator in finite dimension.  With
Lebesgue direction measure and `α = m`, the multiplier is one and `k = (2π)^m`:
`t_f = (2π)^m g`. -/
theorem cor_finite_backprojection_v {m : ℕ} (p : Euclid m → ℝ) (hp : ∀ x, 0 < p x)
    (hpc : Continuous p) {Q : Euclid m →L[ℝ] Euclid m} (hQ : IsTraceClassCovariance Q)
    [IsProbabilityMeasure (densityMeasure p)] (hpQ : IsCenteredGaussian Q (densityMeasure p))
    (f : Euclid m → ℂ) (hf : MemLp f 2 (densityMeasure p)) (g : SchwartzMap (Euclid m) ℂ)
    (hg : ∀ x, g x = f x * p x) :
    ∀ x, frameRepresentative volume g x = ((2 * Real.pi) ^ m : ℝ) * (f x * p x) := by

Status: verified by comparator.

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

/-- **Corollary [cor:finite-backprojection]** The frame operator in finite dimension.  With
Lebesgue direction measure and `α = m`, `S_ρ R_ρ f` is represented against the pivot measure by
`(2π)^m C^{(m)}_ρ f p`, that is `f = (2π)^{-m} (C^{(m)}_ρ)^{-1} p^{-1} S_ρ R_ρ f`. -/
theorem cor_finite_backprojection_vi {m : ℕ} (p : Euclid m → ℝ) (hp : ∀ x, 0 < p x)
    (hpc : Continuous p) {Q : Euclid m →L[ℝ] Euclid m} (hQ : IsTraceClassCovariance Q)
    [IsProbabilityMeasure (densityMeasure p)] (hpQ : IsCenteredGaussian Q (densityMeasure p))
    (f : Euclid m → ℂ) (hf : MemLp f 2 (densityMeasure p)) (g : SchwartzMap (Euclid m) ℂ)
    (hg : ∀ x, g x = f x * p x) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) :
    ∀ h : Lp ℂ 2 (densityMeasure p), h ∈ spectralCore (densityMeasure p) volume →
      ∫ q, ridgelet (densityMeasure p) ρ f q * (starRingEnd ℂ) (ridgelet (densityMeasure p) ρ h q)
          ∂parameterMeasure (volume : Measure (Euclid m)) =
        ∫ x, (((2 * Real.pi) ^ m * admissibilityConst m ρ : ℝ) : ℂ) * (f x * p x) *
          (starRingEnd ℂ) (h x) ∂densityMeasure p := by

Status: verified by comparator.

8.14.2. Proposition G.3 — Dilation obstruction (prop:dilation-obstruction)🔗

Blueprint node: Proposition 2.5.3. Status: verified (all 5 Lean theorems verified).

Formalization note. The eigen-decomposition of W is a hypothesis (HilbertBasis ℕ ℝ H of eigenvectors with eigenvalues w_j > 0); 𝒩(0,tW) is a family γ t with IsCenteredGaussian (t • W); a finite complex Borel measure Γ is represented as h · m with m finite and h integrable. Part i_c is Mathlib's strong law of large numbers (ProbabilityTheory.strong_law_ae) for the coordinates ⟨x,e_j⟩²/w_j, which are i.i.d. with mean t under γ t: the law of ⟨x,e_j⟩/√w_j is 𝒩(0,t) and distinct coordinates are independent, both read off the characteristic functional (IsCenteredGaussian.map_inner_eq_gaussianReal, IsCenteredGaussian.indepFun_inner); part i_d combines i_a–i_c with the fact that a σ-finite measure charges at most countably many pairwise disjoint sets (Measure.countable_meas_pos_of_disjoint_iUnion).

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

/-- **Proposition [prop:dilation-obstruction]** Dilation obstruction.  The sets `E_t` are Borel. -/
theorem prop_dilation_obstruction_i_a (hH : ¬ FiniteDimensional ℝ H) {W : H →L[ℝ] H}
    (hW : IsTraceClassCovariance W) (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ j, 0 < w j)
    (hWe : ∀ j, W (e j) = w j • e j) :
    ∀ t : ℝ, MeasurableSet (strongLawSet e w t) := by

Status: verified by comparator.

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

set_option linter.unusedVariables false in
omit [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H] in
/-- **Proposition [prop:dilation-obstruction]** Dilation obstruction.  The sets `E_t` are pairwise
disjoint. -/
theorem prop_dilation_obstruction_i_b (hH : ¬ FiniteDimensional ℝ H) {W : H →L[ℝ] H}
    (hW : IsTraceClassCovariance W) (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ j, 0 < w j)
    (hWe : ∀ j, W (e j) = w j • e j) :
    ∀ t t' : ℝ, t ≠ t' → Disjoint (strongLawSet e w t) (strongLawSet e w t') := by

Status: verified by comparator.

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

/-- **Proposition [prop:dilation-obstruction]** Dilation obstruction.  For `t > 0`,
`𝒩(0,tW)(E_t) = 1`. -/
theorem prop_dilation_obstruction_i_c (hH : ¬ FiniteDimensional ℝ H) {W : H →L[ℝ] H}
    (hW : IsTraceClassCovariance W) (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ j, 0 < w j)
    (hWe : ∀ j, W (e j) = w j • e j) (γ : ℝ → Measure H)
    (hγ : ∀ t : ℝ, 0 < t → IsCenteredGaussian (t • W) (γ t)) :
    ∀ t : ℝ, 0 < t → γ t (strongLawSet e w t) = 1 := by

Status: verified by comparator.

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

/-- **Proposition [prop:dilation-obstruction]** Dilation obstruction.  Consequently a σ-finite
measure dominates `𝒩(0,tW)` for at most countably many `t > 0`. -/
theorem prop_dilation_obstruction_i_d (hH : ¬ FiniteDimensional ℝ H) {W : H →L[ℝ] H}
    (hW : IsTraceClassCovariance W) (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ j, 0 < w j)
    (hWe : ∀ j, W (e j) = w j • e j) (γ : ℝ → Measure H)
    (hγ : ∀ t : ℝ, 0 < t → IsCenteredGaussian (t • W) (γ t)) :
    ∀ ν : Measure H, SigmaFinite ν → Set.Countable {t : ℝ | 0 < t ∧ γ t ≪ ν} := by

Status: verified by comparator.

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

/-- **Proposition [prop:dilation-obstruction]** Dilation obstruction.  For a bounded Borel `r`
with `{r ≠ 0}` of positive Lebesgue measure, no finite complex Borel measure `Γ = h m` on
`H × ℝ` (a finite measure `m` with an integrable density `h`) has bias slices
`Γ⁺_ω(E) = ∫_{E×ℝ} e^{iωc} Γ(da,dc) = r(ω) (D_{1/ω})_# 𝒩(0,W)(E)` for almost every `ω ≠ 0`. -/
theorem prop_dilation_obstruction_ii (hH : ¬ FiniteDimensional ℝ H) {W : H →L[ℝ] H}
    (hW : IsTraceClassCovariance W) (e : HilbertBasis ℕ ℝ H) (w : ℕ → ℝ) (hw : ∀ j, 0 < w j)
    (hWe : ∀ j, W (e j) = w j • e j) (γW : Measure H) (hγW : IsCenteredGaussian W γW)
    (r : ℝ → ℝ) (hr : Measurable r) (hrb : ∃ M : ℝ, ∀ ω, |r ω| ≤ M)
    (hr0 : 0 < volume {ω : ℝ | r ω ≠ 0}) :
    ¬ ∃ m : Measure (H × ℝ), IsFiniteMeasure m ∧ ∃ h : H × ℝ → ℂ, Integrable h m ∧
      ∀ᵐ ω ∂(volume : Measure ℝ), ω ≠ 0 → ∀ E : Set H, MeasurableSet E →
        ∫ q in E ×ˢ Set.univ, Complex.exp ((ω * q.2 : ℝ) * Complex.I) * h q ∂m =
          (r ω : ℂ) * (((γW.map fun a => ω⁻¹ • a) E).toReal : ℂ) := by

Status: verified by comparator.