8.4. Manuscript Section 4
8.4.1. Definition 4.1 — Regularity along rays (def:ray-regular)
Blueprint node: Definition 3.1.2. Status: verified (its Lean theorem is verified).
Formalization note. The compact symmetric set I ⊆ ℝ∖{0} containing supp ρ̂ fixed before the definition is the predicate IsFrequencyWindow ρ I; the ray-derivative bound max_{k≤m} sup_{ω∈I} |∂^k_ω G(ωa)| and the moment M_m(G) are taken in ℝ≥0∞ so that 'M_m(G) < ∞' is literally rayMoment ν I G m < ⊤; IsRegularAlongRays bundles boundedness, Borel measurability (StronglyMeasurable), smoothness of ω ↦ G(ωa) on an open neighbourhood of I, and finiteness of every M_m(G); it is polymorphic in the target space (the Y-valued version with ‖·‖_Y is the same predicate). The target g_G with spectral density G is spectralTarget ν G (stated for the abstract direction measure ν), and the coefficient γ_G is coefficientFormula ρ G of Section 3. The remark after the definition (regular along rays ⇒ G ∈ L¹(ν_α) ∩ L²(ν_α)) is def_ray_regular.
OperatorRidgelet.IsFrequencyWindow: definition in the library (structure in OperatorRidgelet/Reconstruction/Defs.lean); see the Lean panel of the Blueprint node above.
OperatorRidgelet.rayDerivBound: definition in the library (def in OperatorRidgelet/Reconstruction/Defs.lean); see the Lean panel of the Blueprint node above.
OperatorRidgelet.rayMoment: definition in the library (def in OperatorRidgelet/Reconstruction/Defs.lean); see the Lean panel of the Blueprint node above.
OperatorRidgelet.IsRegularAlongRays: definition in the library (structure in OperatorRidgelet/Reconstruction/Defs.lean); see the Lean panel of the Blueprint node above.
OperatorRidgelet.spectralTarget: definition in the library (def in OperatorRidgelet/Reconstruction/Defs.lean); see the Lean panel of the Blueprint node above.
OperatorRidgelet.Paper.def_ray_regular, theorem in Challenge/Reconstruction.lean:
/-- **Definition [def:ray-regular]** Regularity along rays. A density that is regular along
rays belongs to `L¹(ν_α) ∩ L²(ν_α)` (homogeneity with a fixed `ω ∈ I`). -/
theorem def_ray_regular (ν : Measure H) [SigmaFinite ν] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ)
(hI : IsFrequencyWindow ρ I) (G : H → ℂ) (hG : IsRegularAlongRays ν I G) :
Integrable G ν ∧ MemLp G 2 ν := by
Status: verified by comparator.
8.4.2. Theorem 4.2 — Integral representation of targets with a spectral density (thm:A)
Blueprint node: Theorem 3.1.5. Status: verified (all 11 Lean theorems verified).
Formalization note. Stated for the abstract direction measure ν (σ-finite, full support, homogeneous of degree α), as the manuscript notes after the proof; the Gaussian case is ν = gaussianMixture N α. Part i (bound, continuity, uniqueness) involves neither ρ nor homogeneity and is stated for G ∈ L¹(ν) alone. Part ii: absolute convergence is the a.e. integrability of the inner integrand plus the ν-integrability of the inner integral (ii_a), the identity with C^{(α)}_ρ (ii_b), and the integral-network form integralNetworkDensity when γ_G ∈ L¹(λ_α) (ii_c); it is stated with the band-pass hypothesis of the theorem although, as the manuscript remarks, only admissibility is used. Part iii: a tempered β that is a continuous function of polynomial growth is the pair (β : TemperedDistribution ℝ ℂ, b : ℝ → ℝ) with IsTemperedFunction β b (b continuous, |b| ≤ C(1+|t|)^p, β = integration against b); 'not a polynomial' is ¬ IsPolynomialFun b; the constant is temperedAdmissibilityConst α β ρ of Tempered/Const; iii_a, iii_b are the two absolute convergences, iii_c the identity, iii_d the existence of a band-pass ρ with C^{(α)}_{β,ρ} ≠ 0 for every such non-polynomial β. The remark that the constant is a pairing with a test function supported in -supp ρ̂ is the definition of temperedTestFilter and is not restated.
OperatorRidgelet.Paper.thm_A_i_a, theorem in Challenge/Reconstruction.lean:
set_option linter.unusedVariables false in
omit [CompleteSpace H] [SecondCountableTopology H] [BorelSpace H] in
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For
`G ∈ L¹(ν_α)` the target `g_G` is bounded by `‖G‖_{L¹(ν_α)}`. -/
theorem thm_A_i_a (ν : Measure H) (G : H → ℂ) (hG : Measurable G) (hG₁ : Integrable G ν) :
∀ x : H, ‖spectralTarget ν G x‖ ≤ ∫ ξ, ‖G ξ‖ ∂ν := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_i_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For
`G ∈ L¹(ν_α)` the target `g_G` is continuous. -/
theorem thm_A_i_b (ν : Measure H) (G : H → ℂ) (hG : Measurable G) (hG₁ : Integrable G ν) :
Continuous (spectralTarget ν G) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_i_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For
`G ∈ L¹(ν_α)`, `g_G = 0` only if `G = 0` `ν_α`-almost everywhere. -/
theorem thm_A_i_c (ν : Measure H) (G : H → ℂ) (hG : Measurable G) (hG₁ : Integrable G ν)
(h : spectralTarget ν G = 0) :
G =ᵐ[ν] 0 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_ii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For
`G ∈ L¹(ν_α) ∩ L²(ν_α)` and every `x`, the iterated integral
`∫ [∫ γ_G(a,c) ρ(⟨a,x⟩+c) dc] ν_α(da)` converges absolutely: the inner integral converges
absolutely for `ν_α`-almost every `a`, and the outer integrand is `ν_α`-integrable. -/
theorem thm_A_ii_a (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → ℂ)
(hG : Measurable G) (hG₁ : Integrable G ν) (hG₂ : MemLp G 2 ν) :
∀ x : H,
(∀ᵐ a ∂ν, Integrable fun c : ℝ => coefficientFormula ρ G (a, c) * (ρ (⟪a, x⟫ + c) : ℂ)) ∧
Integrable
(fun a : H => ∫ c : ℝ, coefficientFormula ρ G (a, c) * (ρ (⟪a, x⟫ + c) : ℂ)) ν := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_ii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For
`G ∈ L¹(ν_α) ∩ L²(ν_α)` the spectral synthesis identity
`∫ [∫ γ_G(a,c) ρ(⟨a,x⟩+c) dc] ν_α(da) = C^{(α)}_ρ g_G(x)` holds for every `x`. -/
theorem thm_A_ii_b (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → ℂ)
(hG : Measurable G) (hG₁ : Integrable G ν) (hG₂ : MemLp G 2 ν) :
∀ x : H,
∫ a, (∫ c : ℝ, coefficientFormula ρ G (a, c) * (ρ (⟪a, x⟫ + c) : ℂ)) ∂ν =
admissibilityConst α ρ * spectralTarget ν G x := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_ii_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. If moreover
`γ_G ∈ L¹(λ_α)`, the left side of the spectral synthesis identity is the integral network
`S_ρ[γ_G λ_α](x)`. -/
theorem thm_A_ii_c (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → ℂ)
(hG : Measurable G) (hG₁ : Integrable G ν) (hG₂ : MemLp G 2 ν)
(hγ : Integrable (coefficientFormula ρ G) (parameterMeasure ν)) :
∀ x : H,
∫ a, (∫ c : ℝ, coefficientFormula ρ G (a, c) * (ρ (⟪a, x⟫ + c) : ℂ)) ∂ν =
integralNetworkDensity (fun t => (ρ t : ℂ)) (parameterMeasure ν)
(coefficientFormula ρ G) x := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_iii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For a
tempered `β` that is a continuous function `b` of polynomial growth, and
`G` regular along rays, the inner integral `∫ γ_G(a,c) β(⟨a,x⟩+c) dc` converges absolutely for
`ν_α`-almost every `a`. -/
theorem thm_A_iii_a (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ)
(hI : IsFrequencyWindow ρ I) (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
(hβ : IsTemperedFunction β b) (G : H → ℂ)
(hG : IsRegularAlongRays ν I G) :
∀ x : H, ∀ᵐ a ∂ν,
Integrable fun c : ℝ => coefficientFormula ρ G (a, c) * (b (⟪a, x⟫ + c) : ℂ) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_iii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For a
tempered `β` that is a continuous function `b` of polynomial growth, and
`G` regular along rays, the `ν_α`-integral of the inner integral converges absolutely. -/
theorem thm_A_iii_b (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ)
(hI : IsFrequencyWindow ρ I) (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
(hβ : IsTemperedFunction β b) (G : H → ℂ)
(hG : IsRegularAlongRays ν I G) :
∀ x : H,
Integrable
(fun a : H => ∫ c : ℝ, coefficientFormula ρ G (a, c) * (b (⟪a, x⟫ + c) : ℂ)) ν := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_iii_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For a
tempered `β` that is a continuous function `b` of polynomial growth, and
`G` regular along rays, the tempered spectral synthesis identity
`∫ [∫ γ_G(a,c) β(⟨a,x⟩+c) dc] ν_α(da) = C^{(α)}_{β,ρ} g_G(x)` holds. -/
theorem thm_A_iii_c (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ)
(hI : IsFrequencyWindow ρ I) (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
(hβ : IsTemperedFunction β b) (G : H → ℂ)
(hG : IsRegularAlongRays ν I G) :
∀ x : H,
∫ a, (∫ c : ℝ, coefficientFormula ρ G (a, c) * (b (⟪a, x⟫ + c) : ℂ)) ∂ν =
temperedAdmissibilityConst α β ρ * spectralTarget ν G x := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_iii_d, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:A]** Integral representation of targets with a spectral density. For every
tempered `β` that is a continuous function of polynomial growth and not a polynomial, there is a
band-pass filter `ρ` with `C^{(α)}_{β,ρ} ≠ 0`. -/
theorem thm_A_iii_d {α : ℝ} (hα : 0 < α) (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
(hβ : IsTemperedFunction β b) (hb : ¬ IsPolynomialFun b) :
∃ ρ : SchwartzMap ℝ ℝ, IsBandPass ρ ∧ temperedAdmissibilityConst α β ρ ≠ 0 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_A_iii_e, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Theorem [thm:A]** Tempered synthesis is jointly absolutely integrable. -/
theorem thm_A_iii_e (ν : Measure H) [SigmaFinite ν] (ρ : SchwartzMap ℝ ℝ)
(hρ : IsBandPass ρ) (I : Set ℝ) (hI : IsFrequencyWindow ρ I)
(β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ) (hβ : IsTemperedFunction β b)
(G : H → ℂ) (hG : IsRegularAlongRays ν I G) (x : H) :
Integrable (fun θ : H × ℝ => coefficientFormula ρ G θ *
(b (⟪θ.1, x⟫ + θ.2) : ℂ)) (parameterMeasure ν) := by
Status: verified by comparator.
8.4.3. Theorem 4.3 — Reconstruction and the frame operator (thm:C)
Blueprint node: Theorem 3.2.7. Status: verified (all 18 Lean theorems verified).
Formalization note. Stated for the abstract pair (μ, ν) (Theorem thm:general-weights asserts parts i–iii for it); the Hermite parts iv_d–iv_f add μ = 𝒩(0,Q). 𝓔_α is represented by 𝒦_α = spectralRange μ ν with U_α the inclusion; the continuous anti-dual 𝓔_α' is taken literally as SpectralAntiDual μ ν = (spectralRange μ ν →L⋆[ℂ] ℂ), so that J_α = rieszMap = innerSLFlip ℂ, U_α' = transposeEmbed, T_α = frameOperator = U_α' U_α, S_ρ = synthesis (the anti-dual transpose of the extended transform, eq:weak-synthesis) have exactly the manuscript's values; R_ρ on 𝓔_α is ridgeletExtension, the bounded extension of Theorem thm:B(ii) chosen when it exists; T_α⁻¹ is rieszInv = J_α⁻¹ (part i_a says T_α = J_α, proved by rfl; i_b/i_c: J_α is an isometry and a bijection, proved from the Riesz representation theorem). Part iii: iii_a is the representation of T_α f by g_{𝒢f}, iii_b the converse identity R_ρ T_α⁻¹ U_α' G = W_ρ G, iii_c the representation of U_α' G by g_G for G ∈ L¹, iii_d the second reconstruction formula for U_α' G, and iii_e its concrete form (U_α' G paired with g ∈ 𝒟_α equals C⁻¹ ∫ S_ρ[γ_G λ_α] conj g dμ, the spectral synthesis identity) when γ_G ∈ L¹(λ_α). Part iv: Λ_ρ = backprojection (computed from a jointly measurable bias-Fourier representative; backprojectionOf is the ray average of a given representative); boundedness iv_a is square integrability with a norm bound (linearity of Λ_ρ on L²(λ_α) is a consequence of prop_coefficient_projection_iv); iv_b is Λ_ρ W_ρ = C Id; iv_c is the pointwise identity Λ_ρ R_ρ f = C 𝒢f using the continuous Fourier-slice representative biasFourier (ridgelet μ ρ f); iv_d is the Hermite inversion formula with Mathlib's probabilists' Polynomial.hermite, τ(ξ) = √⟨Qξ,ξ⟩, and the real-variable iterated derivative of hermiteExtension (the analytic continuation e^{t²τ²/2} 𝒢f(tξ)); iv_e is totality on 𝒟_α; iv_f is f = Δ_Q[C⁻¹ Λ_ρ R_ρ f] with Δ_Q = gaussFourierInv the inverse of 𝒢 on its range on 𝒟_α (chosen by uniqueness).
OperatorRidgelet.Paper.thm_C_i_a, theorem in Challenge/Reconstruction.lean:
set_option linter.unusedVariables false in
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The frame operator
`T_α = U_α' U_α` equals the Riesz map `J_α`. -/
theorem thm_C_i_a (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ f : spectralRange μ ν, frameOperator μ ν f = rieszMap μ ν f := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_i_b, theorem in Challenge/Reconstruction.lean:
set_option linter.unusedVariables false in
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The Riesz map `J_α` (hence the
frame operator) is an isometry `𝓔_α → 𝓔_α'`. -/
theorem thm_C_i_b (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
Isometry (rieszMap μ ν) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_i_c, theorem in Challenge/Reconstruction.lean:
set_option linter.unusedVariables false in
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The Riesz map `J_α` (hence the
frame operator) is a bijection `𝓔_α → 𝓔_α'`. -/
theorem thm_C_i_c (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
Function.Bijective (rieszMap μ ν) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_i_d, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The frame identity
`S_ρ R_ρ f = C^{(α)}_ρ T_α f` for `f ∈ 𝓔_α`. -/
theorem thm_C_i_d (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ f : spectralRange μ ν,
synthesis μ ν ρ (ridgeletExtension μ ν ρ f) =
(admissibilityConst α ρ : ℂ) • frameOperator μ ν f := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_ii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The first reconstruction
formula `f = (C^{(α)}_ρ)⁻¹ T_α⁻¹ S_ρ R_ρ f` for `f ∈ 𝓔_α` (`T_α⁻¹ = J_α⁻¹` by part (i)). -/
theorem thm_C_ii_a (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ f : spectralRange μ ν,
f = (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) •
rieszInv μ ν (synthesis μ ν ρ (ridgeletExtension μ ν ρ f)) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_ii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The second reconstruction
formula `g = (C^{(α)}_ρ)⁻¹ S_ρ (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α'`. -/
theorem thm_C_ii_b (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ g : SpectralAntiDual μ ν,
g = (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) •
synthesis μ ν ρ (ridgeletExtension μ ν ρ (rieszInv μ ν g)) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. If `f ∈ 𝒟_α` and
`𝒢_Q f ∈ L¹(ν_α)`, then `T_α f` is represented by the bounded continuous function
`g_{𝒢_Q f}`: `T_α f [g] = ∫ g_{𝒢_Q f}(x) conj(g(x)) μ_Q(dx)` for `g ∈ 𝒟_α`. -/
theorem thm_C_iii_a (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : spectralCore μ ν) (hG : Integrable (gaussFourier μ f) ν) :
∀ g : spectralCore μ ν,
frameOperator μ ν (spectralEmbed μ ν f) (spectralEmbed μ ν g) =
∫ x, spectralTarget ν (gaussFourier μ f) x * (starRingEnd ℂ) ((g : Lp ℂ 2 μ) x) ∂μ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. Conversely, for `G ∈ 𝒦_α` the
functional `U_α' G ∈ 𝓔_α'` satisfies `R_ρ T_α⁻¹ U_α' G = W_ρ G`. -/
theorem thm_C_iii_b (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRange μ ν,
ridgeletExtension μ ν ρ (rieszInv μ ν (transposeEmbed μ ν G)) =
spectralCoefficient ν ρ ((G : Lp ℂ 2 ν) : H → ℂ) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iii_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. When `G ∈ 𝒦_α ∩ L¹(ν_α)`, the
functional `U_α' G` is represented by `g_G`: `U_α' G [g] = ∫ g_G(x) conj(g(x)) μ_Q(dx)` for
`g ∈ 𝒟_α`. -/
theorem thm_C_iii_c (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRange μ ν, Integrable ((G : Lp ℂ 2 ν) : H → ℂ) ν →
∀ g : spectralCore μ ν,
transposeEmbed μ ν G (spectralEmbed μ ν g) =
∫ x, spectralTarget ν ((G : Lp ℂ 2 ν) : H → ℂ) x * (starRingEnd ℂ) ((g : Lp ℂ 2 μ) x)
∂μ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iii_d, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. For `G ∈ 𝒦_α` the second
reconstruction formula applied to `U_α' G` reads `U_α' G = (C^{(α)}_ρ)⁻¹ S_ρ W_ρ G`. -/
theorem thm_C_iii_d (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRange μ ν,
transposeEmbed μ ν G = (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) •
synthesis μ ν ρ (spectralCoefficient ν ρ ((G : Lp ℂ 2 ν) : H → ℂ)) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iii_e, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. When `G ∈ 𝒦_α ∩ L¹(ν_α)` and
`γ_G ∈ L¹(λ_α)`, the second reconstruction formula for `U_α' G` is the spectral synthesis
identity: paired with `g ∈ 𝒟_α`, `U_α' G [g] = (C^{(α)}_ρ)⁻¹ ∫ S_ρ[γ_G λ_α](x) conj(g(x)) μ_Q(dx)`
(Lemma `lem:weak-equals-strong`). -/
theorem thm_C_iii_e (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRange μ ν, Integrable ((G : Lp ℂ 2 ν) : H → ℂ) ν →
Integrable (coefficientFormula ρ ((G : Lp ℂ 2 ν) : H → ℂ)) (parameterMeasure ν) →
∀ g : spectralCore μ ν,
transposeEmbed μ ν G (spectralEmbed μ ν g) =
(((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) *
∫ x, integralNetworkDensity (fun t => (ρ t : ℂ)) (parameterMeasure ν)
(coefficientFormula ρ ((G : Lp ℂ 2 ν) : H → ℂ)) x *
(starRingEnd ℂ) ((g : Lp ℂ 2 μ) x) ∂μ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iv_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The backprojection `Λ_ρ` is a
bounded operator `L²(λ_α) → L²(ν_α)`: `Λ_ρ γ` is square integrable with
`‖Λ_ρ γ‖²_{L²(ν_α)} ≤ M ‖γ‖²_{L²(λ_α)}` for a constant `M`. -/
theorem thm_C_iv_a (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) :
∃ M : ℝ, ∀ γ : Lp ℂ 2 (parameterMeasure ν),
MemLp (backprojection α ν ρ γ) 2 ν ∧
∫ ξ, ‖backprojection α ν ρ γ ξ‖ ^ 2 ∂ν ≤ M * ‖γ‖ ^ 2 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iv_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. `Λ_ρ W_ρ = C^{(α)}_ρ Id` on
`L²(ν_α)`. -/
theorem thm_C_iv_b (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
(hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) :
∀ F : H → ℂ, Measurable F → MemLp F 2 ν →
backprojection α ν ρ (spectralCoefficient ν ρ F) =ᵐ[ν]
fun ξ => admissibilityConst α ρ * F ξ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iv_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. For `f ∈ 𝒟_α` the identity
`Λ_ρ R_ρ f = C^{(α)}_ρ 𝒢_Q f` holds pointwise in `ξ`, with `Λ_ρ` computed from the continuous
Fourier-slice representative `(a,ω) ↦ \widehat{R_ρ f}(a,ω)` of the transform. -/
theorem thm_C_iv_c (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : spectralCore μ ν) :
∀ ξ : H,
backprojectionOf α ρ (biasFourier (ridgelet μ ρ f)) ξ =
admissibilityConst α ρ * gaussFourier μ f ξ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iv_d, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The Hermite inversion formula
`E_{μ_Q}[f He_n(⟨x,ξ⟩/τ(ξ))] = i^n τ(ξ)^{-n} (d/dt)^n (e^{t²τ(ξ)²/2} 𝒢_Q f(tξ))|_{t=0}`,
`τ(ξ) = ⟨Qξ,ξ⟩^{1/2}`, for `f ∈ 𝒟_α` and `ξ ≠ 0`. -/
theorem thm_C_iv_d (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q)
(hμ : IsCenteredGaussian Q μ) (f : spectralCore μ ν) :
∀ ξ : H, ξ ≠ 0 → ∀ n : ℕ,
hermiteCoefficient μ Q f ξ n =
Complex.I ^ n / ((Real.sqrt ⟪Q ξ, ξ⟫ : ℝ) : ℂ) ^ n *
iteratedDeriv n (fun t : ℝ => hermiteExtension μ Q f ξ t) 0 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iv_e, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. The Hermite coefficients over all
`ξ ≠ 0` and `n` determine `f ∈ 𝒟_α` in `L²(μ_Q)`. -/
theorem thm_C_iv_e (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q)
(hμ : IsCenteredGaussian Q μ) :
∀ f g : spectralCore μ ν,
(∀ ξ : H, ξ ≠ 0 → ∀ n : ℕ, hermiteCoefficient μ Q f ξ n = hermiteCoefficient μ Q g ξ n) →
f = g := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iv_f, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:C]** Reconstruction and the frame operator. Reconstruction by
backprojection: `f = Δ_Q[(C^{(α)}_ρ)⁻¹ Λ_ρ R_ρ f]` for `f ∈ 𝒟_α`, with `Δ_Q` the inverse of
`𝒢_Q` on its range on `𝒟_α`. -/
theorem thm_C_iv_f (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q)
(hμ : IsCenteredGaussian Q μ) (f : spectralCore μ ν) :
gaussFourierInv μ ν
(fun ξ => (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) *
backprojectionOf α ρ (biasFourier (ridgelet μ ρ f)) ξ) =
(f : Lp ℂ 2 μ) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_C_iv_completion, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Theorem [thm:C]** Backprojection after analysis recovers the completed spectral density. -/
theorem thm_C_iv_completion (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
{α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : spectralRange μ ν) :
backprojection α ν ρ (ridgeletExtension μ ν ρ f) =ᵐ[ν]
fun ξ => admissibilityConst α ρ * (f : Lp ℂ 2 ν) ξ := by
Status: verified by comparator.
8.4.4. Corollary 4.4 — Stability under coefficient perturbations (cor:coefficient-stability)
Blueprint node: Corollary 3.2.8. Status: verified (all 4 Lean theorems verified).
OperatorRidgelet.Paper.cor_coefficient_stability_i, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Corollary [cor:coefficient-stability]** The decoder is C⁻¹ T⁻¹ S. -/
theorem cor_coefficient_stability_i (α : ℝ) (μ ν : Measure H) [IsProbabilityMeasure μ]
(ρ : ℝ → ℝ) (γ : Lp ℂ 2 (parameterMeasure ν)) :
coefficientDecoder α μ ν ρ γ =
((admissibilityConst α ρ : ℂ)⁻¹) • rieszInv μ ν (synthesis μ ν ρ γ) := by
Status: verified by comparator.
OperatorRidgelet.Paper.cor_coefficient_stability_ii, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Corollary [cor:coefficient-stability]** The bounded decoder is a left inverse. -/
theorem cor_coefficient_stability_ii (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] {α : ℝ} (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : spectralRange μ ν) :
coefficientDecoder α μ ν ρ (ridgeletExtension μ ν ρ f) = f := by
Status: verified by comparator.
OperatorRidgelet.Paper.cor_coefficient_stability_iii, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Corollary [cor:coefficient-stability]** The decoder norm is at most 1/√C. -/
theorem cor_coefficient_stability_iii (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] {α : ℝ} (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
‖coefficientDecoder α μ ν ρ‖ ≤ (Real.sqrt (admissibilityConst α ρ))⁻¹ := by
Status: verified by comparator.
OperatorRidgelet.Paper.cor_coefficient_stability_iv, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Corollary [cor:coefficient-stability]** Coefficient error δ gives spectral error δ/√C. -/
theorem cor_coefficient_stability_iv (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] {α : ℝ} (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : spectralRange μ ν) (γ : Lp ℂ 2 (parameterMeasure ν))
{δ : ℝ} (hδ : ‖γ - ridgeletExtension μ ν ρ f‖ ≤ δ) :
‖coefficientDecoder α μ ν ρ γ - f‖ ≤ δ / Real.sqrt (admissibilityConst α ρ) := by
Status: verified by comparator.
8.4.5. Theorem 4.6 — Vector-valued extension (thm:vector-valued)
Blueprint node: Theorem 3.3.2. Status: verified (all 35 Lean theorems verified).
Formalization note. One theorem per part of thm:A, thm:B, thm:C, mirroring the scalar statements (thm:B in the abstract-pair form of thm:general-weights) for a separable complex Hilbert space Y ([InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]) and targets f : H → Y; scalar integrals are Bochner integrals, products f(x)φ(x) are φ(x) • f(x), absolute values are norms in Y, Borel measurability is StronglyMeasurable, and inner products ⟨u,v⟩_Y (linear in u) are Mathlib's inner ℂ v u. The Y-valued objects are the Vec-suffixed definitions of Reconstruction/Defs (gaussFourierVec, ridgeletVec, coefficientFormulaVec, biasFourierVec, spectralCoefficientVec, spectralInnerVec, spectralCoreVec, spectralRangeVec, spectralEmbedVec, ridgeletExtensionVec, SpectralAntiDualVec, rieszMapVec, rieszInvVec, transposeEmbedVec, frameOperatorVec, synthesisVec, backprojectionOfVec, backprojectionVec, hermiteExtensionVec, hermiteCoefficientVec, gaussFourierInvVec); spectralTarget, IsRegularAlongRays, and integralNetworkDensity are polymorphic in the target. The existence claim thm:A(iii)(d) is scalar and is not repeated; thm:B(ii)(b)–(d) are stated for the chosen extension ridgeletExtensionVec, which (ii)(a) makes unique.
OperatorRidgelet.Paper.thm_vector_valued_A_i_a, theorem in Challenge/Reconstruction.lean:
set_option linter.unusedVariables false in
omit [CompleteSpace H] [SecondCountableTopology H] [BorelSpace H] [CompleteSpace Y]
[SecondCountableTopology Y] in
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(i) for `Y`-valued
densities: `‖g_G(x)‖_Y ≤ ‖G‖_{L¹(ν_α;Y)}`. -/
theorem thm_vector_valued_A_i_a (ν : Measure H) (G : H → Y) (hG : StronglyMeasurable G)
(hG₁ : Integrable G ν) :
∀ x : H, ‖spectralTarget ν G x‖ ≤ ∫ ξ, ‖G ξ‖ ∂ν := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_i_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(i) for `Y`-valued
densities: `g_G` is continuous. -/
theorem thm_vector_valued_A_i_b (ν : Measure H) (G : H → Y) (hG : StronglyMeasurable G)
(hG₁ : Integrable G ν) :
Continuous (spectralTarget ν G) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_i_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(i) for `Y`-valued
densities: `g_G = 0` only if `G = 0` `ν_α`-almost everywhere. -/
theorem thm_vector_valued_A_i_c (ν : Measure H) (G : H → Y) (hG : StronglyMeasurable G)
(hG₁ : Integrable G ν) (h : spectralTarget ν G = 0) :
G =ᵐ[ν] 0 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_ii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(ii) for `Y`-valued
densities: the iterated integral `∫ [∫ ρ(⟨a,x⟩+c) γ_G(a,c) dc] ν_α(da)` converges absolutely. -/
theorem thm_vector_valued_A_ii_a (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
(hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → Y)
(hG : StronglyMeasurable G) (hG₁ : Integrable G ν) (hG₂ : MemLp G 2 ν) :
∀ x : H,
(∀ᵐ a ∂ν, Integrable fun c : ℝ =>
(ρ (⟪a, x⟫ + c) : ℂ) • coefficientFormulaVec ρ G (a, c)) ∧
Integrable
(fun a : H => ∫ c : ℝ, (ρ (⟪a, x⟫ + c) : ℂ) • coefficientFormulaVec ρ G (a, c)) ν := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_ii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(ii) for `Y`-valued
densities: the spectral synthesis identity with the same constant `C^{(α)}_ρ`. -/
theorem thm_vector_valued_A_ii_b (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
(hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → Y)
(hG : StronglyMeasurable G) (hG₁ : Integrable G ν) (hG₂ : MemLp G 2 ν) :
∀ x : H,
∫ a, (∫ c : ℝ, (ρ (⟪a, x⟫ + c) : ℂ) • coefficientFormulaVec ρ G (a, c)) ∂ν =
(admissibilityConst α ρ : ℂ) • spectralTarget ν G x := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_ii_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(ii) for `Y`-valued
densities: if `γ_G ∈ L¹(λ_α; Y)`, the left side is the `Y`-valued integral network
`S_ρ[γ_G λ_α](x)`. -/
theorem thm_vector_valued_A_ii_c (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
(hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → Y)
(hG : StronglyMeasurable G) (hG₁ : Integrable G ν) (hG₂ : MemLp G 2 ν)
(hγ : Integrable (coefficientFormulaVec ρ G) (parameterMeasure ν)) :
∀ x : H,
∫ a, (∫ c : ℝ, (ρ (⟪a, x⟫ + c) : ℂ) • coefficientFormulaVec ρ G (a, c)) ∂ν =
integralNetworkDensity (fun t => (ρ t : ℂ)) (parameterMeasure ν)
(coefficientFormulaVec ρ G) x := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_iii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(iii) for
`Y`-valued densities regular along rays (with `‖·‖_Y` in place of the absolute value): the
inner integral converges absolutely for `ν_α`-almost every `a`. -/
theorem thm_vector_valued_A_iii_a (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
(hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ)
(hI : IsFrequencyWindow ρ I) (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
(hβ : IsTemperedFunction β b) (G : H → Y)
(hG : IsRegularAlongRays ν I G) :
∀ x : H, ∀ᵐ a ∂ν,
Integrable fun c : ℝ => (b (⟪a, x⟫ + c) : ℂ) • coefficientFormulaVec ρ G (a, c) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_iii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(iii) for
`Y`-valued densities regular along rays: the outer integral converges absolutely. -/
theorem thm_vector_valued_A_iii_b (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
(hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ)
(hI : IsFrequencyWindow ρ I) (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
(hβ : IsTemperedFunction β b) (G : H → Y)
(hG : IsRegularAlongRays ν I G) :
∀ x : H,
Integrable
(fun a : H => ∫ c : ℝ, (b (⟪a, x⟫ + c) : ℂ) • coefficientFormulaVec ρ G (a, c)) ν := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_iii_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:A`(iii) for
`Y`-valued densities regular along rays: the tempered spectral synthesis identity with the
same constant `C^{(α)}_{β,ρ}`. -/
theorem thm_vector_valued_A_iii_c (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
(hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ)
(hI : IsFrequencyWindow ρ I) (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
(hβ : IsTemperedFunction β b) (G : H → Y)
(hG : IsRegularAlongRays ν I G) :
∀ x : H,
∫ a, (∫ c : ℝ, (b (⟪a, x⟫ + c) : ℂ) • coefficientFormulaVec ρ G (a, c)) ∂ν =
temperedAdmissibilityConst α β ρ • spectralTarget ν G x := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_B_i_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:B`(i) for `Y`-valued
targets: `R_ρ f ∈ L²(λ_α; Y)` for `f ∈ 𝒟_α(Y)` and `α`-admissible `ρ`. -/
theorem thm_vector_valued_B_i_a (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : Lp Y 2 μ) (hf : f ∈ spectralCoreVec Y μ ν) :
MemLp (ridgeletVec μ ρ f) 2 (parameterMeasure ν) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_B_i_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:B`(i) for `Y`-valued
targets: the Plancherel identity
`⟨R_{ρ₁} f, R_{ρ₂} g⟩_{L²(λ_α;Y)} = C^{(α)}_{ρ₁,ρ₂} ⟨f,g⟩_{𝓔_α(Y)}`. -/
theorem thm_vector_valued_B_i_b (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ₁ ρ₂ : SchwartzMap ℝ ℝ) (hρ₁ : IsAdmissible α ρ₁) (hρ₂ : IsAdmissible α ρ₂)
(f g : Lp Y 2 μ) (hf : f ∈ spectralCoreVec Y μ ν) (hg : g ∈ spectralCoreVec Y μ ν) :
∫ p, inner ℂ (ridgeletVec μ ρ₂ g p) (ridgeletVec μ ρ₁ f p) ∂parameterMeasure ν =
crossAdmissibilityConst α ρ₁ ρ₂ * spectralInnerVec μ ν f g := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_B_ii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:B`(ii) for
`Y`-valued targets: an `α`-admissible `ρ` determines a unique bounded extension
`R_ρ : 𝓔_α(Y) → L²(λ_α; Y)`. -/
theorem thm_vector_valued_B_ii_a (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∃! R : spectralRangeVec Y μ ν →L[ℂ] Lp Y 2 (parameterMeasure ν),
∀ f : spectralCoreVec Y μ ν,
(R (spectralEmbedVec μ ν f) : H × ℝ → Y) =ᵐ[parameterMeasure ν] ridgeletVec μ ρ f := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_B_ii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:B`(ii) for
`Y`-valued targets: `‖R_ρ f‖² = C^{(α)}_ρ ‖f‖²_{𝓔_α(Y)}`. -/
theorem thm_vector_valued_B_ii_b (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRangeVec Y μ ν,
‖ridgeletExtensionVec Y μ ν ρ G‖ ^ 2 = admissibilityConst α ρ * ‖G‖ ^ 2 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_B_ii_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:B`(ii) for
`Y`-valued targets: the range of `R_ρ` is closed. -/
theorem thm_vector_valued_B_ii_c (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
IsClosed (Set.range (ridgeletExtensionVec Y μ ν ρ)) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_B_ii_d, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:B`(ii) for
`Y`-valued targets: `R_ρ = W_ρ U_α`. -/
theorem thm_vector_valued_B_ii_d (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRangeVec Y μ ν,
ridgeletExtensionVec Y μ ν ρ G = spectralCoefficientVec ν ρ ((G : Lp Y 2 ν) : H → Y) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_B_iii, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:B`(iii) for
`Y`-valued targets: `R_ρ f = 0` `λ_α`-a.e. implies `f = 0` `μ_Q`-a.e. for `f ∈ L¹(μ_Q; Y)`. -/
theorem thm_vector_valued_B_iii (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : H → Y) (hf : Integrable f μ)
(h : ridgeletVec μ ρ f =ᵐ[parameterMeasure ν] 0) :
f =ᵐ[μ] 0 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_i_a, theorem in Challenge/Reconstruction.lean:
set_option linter.unusedVariables false in
omit [CompleteSpace H] [SecondCountableTopology H] [CompleteSpace Y] [SecondCountableTopology Y]
in
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(i) for `Y`-valued
targets: the frame operator `T_α = U_α' U_α` equals the Riesz map `J_α` of `𝓔_α(Y)`. -/
theorem thm_vector_valued_C_i_a (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ f : spectralRangeVec Y μ ν, frameOperatorVec μ ν f = rieszMapVec Y μ ν f := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_i_b, theorem in Challenge/Reconstruction.lean:
set_option linter.unusedVariables false in
omit [CompleteSpace H] [SecondCountableTopology H] [CompleteSpace Y] [SecondCountableTopology Y]
in
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(i) for `Y`-valued
targets: the Riesz map of `𝓔_α(Y)` is an isometry. -/
theorem thm_vector_valued_C_i_b (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
Isometry (rieszMapVec Y μ ν) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_i_c, theorem in Challenge/Reconstruction.lean:
set_option linter.unusedVariables false in
omit [CompleteSpace H] [SecondCountableTopology H] [SecondCountableTopology Y] in
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(i) for `Y`-valued
targets: the Riesz map of `𝓔_α(Y)` is a bijection onto `𝓔_α(Y)'`. -/
theorem thm_vector_valued_C_i_c (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
Function.Bijective (rieszMapVec Y μ ν) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_i_d, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(i) for `Y`-valued
targets: the frame identity `S_ρ R_ρ f = C^{(α)}_ρ T_α f`. -/
theorem thm_vector_valued_C_i_d (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ f : spectralRangeVec Y μ ν,
synthesisVec μ ν ρ (ridgeletExtensionVec Y μ ν ρ f) =
(admissibilityConst α ρ : ℂ) • frameOperatorVec μ ν f := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_ii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(ii) for
`Y`-valued targets: `f = (C^{(α)}_ρ)⁻¹ T_α⁻¹ S_ρ R_ρ f`. -/
theorem thm_vector_valued_C_ii_a (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ f : spectralRangeVec Y μ ν,
f = (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) •
rieszInvVec μ ν (synthesisVec μ ν ρ (ridgeletExtensionVec Y μ ν ρ f)) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_ii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(ii) for
`Y`-valued targets: `g = (C^{(α)}_ρ)⁻¹ S_ρ (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α(Y)'`. -/
theorem thm_vector_valued_C_ii_b (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ g : SpectralAntiDualVec Y μ ν,
g = (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) •
synthesisVec μ ν ρ (ridgeletExtensionVec Y μ ν ρ (rieszInvVec μ ν g)) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iii_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iii) for
`Y`-valued targets: for `f ∈ 𝒟_α(Y)` with `𝒢_Q f ∈ L¹(ν_α; Y)`, `T_α f` is represented by
`g_{𝒢_Q f}`: `T_α f [g] = ∫ ⟨g_{𝒢_Q f}(x), g(x)⟩_Y μ_Q(dx)`. -/
theorem thm_vector_valued_C_iii_a (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : spectralCoreVec Y μ ν)
(hG : Integrable (gaussFourierVec μ ((f : Lp Y 2 μ) : H → Y)) ν) :
∀ g : spectralCoreVec Y μ ν,
frameOperatorVec μ ν (spectralEmbedVec μ ν f) (spectralEmbedVec μ ν g) =
∫ x, inner ℂ ((g : Lp Y 2 μ) x)
(spectralTarget ν (gaussFourierVec μ ((f : Lp Y 2 μ) : H → Y)) x) ∂μ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iii_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iii) for
`Y`-valued targets: `R_ρ T_α⁻¹ U_α' G = W_ρ G` for `G ∈ 𝒦_α(Y)`. -/
theorem thm_vector_valued_C_iii_b (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRangeVec Y μ ν,
ridgeletExtensionVec Y μ ν ρ (rieszInvVec μ ν (transposeEmbedVec μ ν G)) =
spectralCoefficientVec ν ρ ((G : Lp Y 2 ν) : H → Y) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iii_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iii) for
`Y`-valued targets: when `G ∈ 𝒦_α(Y) ∩ L¹(ν_α; Y)`, `U_α' G` is represented by `g_G`. -/
theorem thm_vector_valued_C_iii_c (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRangeVec Y μ ν, Integrable ((G : Lp Y 2 ν) : H → Y) ν →
∀ g : spectralCoreVec Y μ ν,
transposeEmbedVec μ ν G (spectralEmbedVec μ ν g) =
∫ x, inner ℂ ((g : Lp Y 2 μ) x) (spectralTarget ν ((G : Lp Y 2 ν) : H → Y) x) ∂μ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iii_d, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iii) for
`Y`-valued targets: `U_α' G = (C^{(α)}_ρ)⁻¹ S_ρ W_ρ G` for `G ∈ 𝒦_α(Y)`. -/
theorem thm_vector_valued_C_iii_d (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRangeVec Y μ ν,
transposeEmbedVec μ ν G = (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) •
synthesisVec μ ν ρ (spectralCoefficientVec ν ρ ((G : Lp Y 2 ν) : H → Y)) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iii_e, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iii) for
`Y`-valued targets: when `G ∈ 𝒦_α(Y) ∩ L¹(ν_α; Y)` and `γ_G ∈ L¹(λ_α; Y)`, the second
reconstruction formula for `U_α' G` is the spectral synthesis identity paired with
`g ∈ 𝒟_α(Y)`. -/
theorem thm_vector_valued_C_iii_e (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) :
∀ G : spectralRangeVec Y μ ν, Integrable ((G : Lp Y 2 ν) : H → Y) ν →
Integrable (coefficientFormulaVec ρ ((G : Lp Y 2 ν) : H → Y)) (parameterMeasure ν) →
∀ g : spectralCoreVec Y μ ν,
transposeEmbedVec μ ν G (spectralEmbedVec μ ν g) =
(((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) *
∫ x, inner ℂ ((g : Lp Y 2 μ) x)
(integralNetworkDensity (fun t => (ρ t : ℂ)) (parameterMeasure ν)
(coefficientFormulaVec ρ ((G : Lp Y 2 ν) : H → Y)) x) ∂μ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iv_a, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iv) for
`Y`-valued targets: the backprojection `Λ_ρ` is a bounded operator
`L²(λ_α; Y) → L²(ν_α; Y)`. -/
theorem thm_vector_valued_C_iv_a (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
(hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) :
∃ M : ℝ, ∀ γ : Lp Y 2 (parameterMeasure ν),
MemLp (backprojectionVec α ν ρ γ) 2 ν ∧
∫ ξ, ‖backprojectionVec α ν ρ γ ξ‖ ^ 2 ∂ν ≤ M * ‖γ‖ ^ 2 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iv_b, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iv) for
`Y`-valued targets: `Λ_ρ W_ρ = C^{(α)}_ρ Id` on `L²(ν_α; Y)`. -/
theorem thm_vector_valued_C_iv_b (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
(hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) :
∀ F : H → Y, StronglyMeasurable F → MemLp F 2 ν →
backprojectionVec α ν ρ (spectralCoefficientVec ν ρ F) =ᵐ[ν]
fun ξ => (admissibilityConst α ρ : ℂ) • F ξ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iv_c, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iv) for
`Y`-valued targets: `Λ_ρ R_ρ f = C^{(α)}_ρ 𝒢_Q f` pointwise for `f ∈ 𝒟_α(Y)`, with `Λ_ρ`
computed from the Fourier-slice representative of `R_ρ f`. -/
theorem thm_vector_valued_C_iv_c (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) (f : spectralCoreVec Y μ ν) :
∀ ξ : H,
backprojectionOfVec α ρ (biasFourierVec (ridgeletVec μ ρ ((f : Lp Y 2 μ) : H → Y))) ξ =
(admissibilityConst α ρ : ℂ) • gaussFourierVec μ ((f : Lp Y 2 μ) : H → Y) ξ := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iv_d, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iv) for
`Y`-valued targets: the Hermite inversion formula, applied componentwise, for `f ∈ 𝒟_α(Y)` and
`ξ ≠ 0`. -/
theorem thm_vector_valued_C_iv_d (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q)
(hμ : IsCenteredGaussian Q μ) (f : spectralCoreVec Y μ ν) :
∀ ξ : H, ξ ≠ 0 → ∀ n : ℕ,
hermiteCoefficientVec μ Q ((f : Lp Y 2 μ) : H → Y) ξ n =
(Complex.I ^ n / ((Real.sqrt ⟪Q ξ, ξ⟫ : ℝ) : ℂ) ^ n) •
iteratedDeriv n
(fun t : ℝ => hermiteExtensionVec μ Q ((f : Lp Y 2 μ) : H → Y) ξ t) 0 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iv_e, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iv) for
`Y`-valued targets: the Hermite coefficients over all `ξ ≠ 0` and `n` determine
`f ∈ 𝒟_α(Y)` in `L²(μ_Q; Y)`. -/
theorem thm_vector_valued_C_iv_e (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q)
(hμ : IsCenteredGaussian Q μ) :
∀ f g : spectralCoreVec Y μ ν,
(∀ ξ : H, ξ ≠ 0 → ∀ n : ℕ,
hermiteCoefficientVec μ Q ((f : Lp Y 2 μ) : H → Y) ξ n =
hermiteCoefficientVec μ Q ((g : Lp Y 2 μ) : H → Y) ξ n) →
f = g := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iv_f, theorem in Challenge/Reconstruction.lean:
/-- **Theorem [thm:vector-valued]** Vector-valued extension. Theorem `thm:C`(iv) for
`Y`-valued targets: `f = Δ_Q[(C^{(α)}_ρ)⁻¹ Λ_ρ R_ρ f]` for `f ∈ 𝒟_α(Y)`. -/
theorem thm_vector_valued_C_iv_f (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
[ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsAdmissible α ρ) {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q)
(hμ : IsCenteredGaussian Q μ) (f : spectralCoreVec Y μ ν) :
gaussFourierInvVec μ ν
(fun ξ => (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) •
backprojectionOfVec α ρ (biasFourierVec (ridgeletVec μ ρ ((f : Lp Y 2 μ) : H → Y))) ξ) =
(f : Lp Y 2 μ) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_A_iii_e, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] [CompleteSpace Y]
[SecondCountableTopology Y] in
/-- **Theorem [thm:vector-valued]** Tempered synthesis is Bochner integrable on the product. -/
theorem thm_vector_valued_A_iii_e (ν : Measure H) [SigmaFinite ν] (ρ : SchwartzMap ℝ ℝ)
(hρ : IsBandPass ρ) (I : Set ℝ) (hI : IsFrequencyWindow ρ I)
(β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ) (hβ : IsTemperedFunction β b)
(G : H → Y) (hG : IsRegularAlongRays ν I G) (x : H) :
Integrable (fun θ : H × ℝ => (b (⟪θ.1, x⟫ + θ.2) : ℂ) •
coefficientFormulaVec ρ G θ) (parameterMeasure ν) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_vector_valued_C_iv_completion, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Theorem [thm:vector-valued]** The completed vector spectral density is recovered in L². -/
theorem thm_vector_valued_C_iv_completion (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (f : spectralRangeVec Y μ ν) :
backprojectionVec α ν ρ (ridgeletExtensionVec Y μ ν ρ f) =ᵐ[ν]
fun ξ => (admissibilityConst α ρ : ℂ) • (f : Lp Y 2 ν) ξ := by
Status: verified by comparator.