8.15. Appendix H
8.15.1. Theorem H.1 — Abstract-weight extension (thm:general-weights)
Blueprint node: Theorem 2.4.1. Status: verified (all 11 Lean theorems verified).
Formalization note. The Fourier-slice identity is already stated for general μ (lem_fourier_slice_v); thm:B for the abstract pair is the eight parts here; the abstract-weight versions of thm:A and thm:C(i)-(iii) belong to the reconstruction work package.
OperatorRidgelet.Paper.thm_general_weights_plancherel_memLp, theorem in Challenge/Transform.lean:
/-- **Theorem [thm:general-weights]** Abstract-weight extension. Theorem `thm:B`(i) for the
abstract pair: `R_ρ f ∈ L²(λ)` for `f ∈ 𝒟_{μ,ν}` and `α`-admissible `ρ`. -/
theorem thm_general_weights_plancherel_memLp (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (f : Lp ℂ 2 μ) (hf : f ∈ spectralCore μ ν) :
MemLp (ridgelet μ ρ f) 2 (parameterMeasure ν) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_plancherel, theorem in Challenge/Transform.lean:
/-- **Theorem [thm:general-weights]** Abstract-weight extension. Theorem `thm:B`(i) for the
abstract pair: the Plancherel identity
`⟨R_{ρ₁} f, R_{ρ₂} g⟩_{L²(λ)} = C^{(α)}_{ρ₁,ρ₂} ⟨f,g⟩_{𝓔_{μ,ν}}`. -/
theorem thm_general_weights_plancherel (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ₁ ρ₂ : SchwartzMap ℝ ℝ) (hρ₁ : IsAdmissible α ρ₁) (hρ₂ : IsAdmissible α ρ₂)
(f g : Lp ℂ 2 μ) (hf : f ∈ spectralCore μ ν) (hg : g ∈ spectralCore μ ν) :
∫ p, ridgelet μ ρ₁ f p * (starRingEnd ℂ) (ridgelet μ ρ₂ g p) ∂parameterMeasure ν =
crossAdmissibilityConst α ρ₁ ρ₂ * spectralInner μ ν f g := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_extension, theorem in Challenge/Transform.lean:
/-- **Theorem [thm:general-weights]** Abstract-weight extension. Theorem `thm:B`(ii) for the
abstract pair: the unique bounded extension `R_ρ : 𝓔_{μ,ν} → L²(λ)`. -/
theorem thm_general_weights_extension (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) :
∃! R : spectralRange μ ν →L[ℂ] Lp ℂ 2 (parameterMeasure ν),
∀ f : spectralCore μ ν,
(R (spectralEmbed μ ν f) : H × ℝ → ℂ) =ᵐ[parameterMeasure ν] ridgelet μ ρ f := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_extension_norm, theorem in Challenge/Transform.lean:
/-- **Theorem [thm:general-weights]** Abstract-weight extension. Theorem `thm:B`(ii) for the
abstract pair: `‖R_ρ f‖² = C^{(α)}_ρ ‖f‖²_{𝓔_{μ,ν}}`. -/
theorem thm_general_weights_extension_norm (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ)
(R : spectralRange μ ν →L[ℂ] Lp ℂ 2 (parameterMeasure ν))
(hR : ∀ f : spectralCore μ ν,
(R (spectralEmbed μ ν f) : H × ℝ → ℂ) =ᵐ[parameterMeasure ν] ridgelet μ ρ f) :
∀ G : spectralRange μ ν, ‖R G‖ ^ 2 = admissibilityConst α ρ * ‖G‖ ^ 2 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_extension_closed_range, theorem in Challenge/Transform.lean:
/-- **Theorem [thm:general-weights]** Abstract-weight extension. Theorem `thm:B`(ii) for the
abstract pair: the extension has closed range. -/
theorem thm_general_weights_extension_closed_range (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ)
(R : spectralRange μ ν →L[ℂ] Lp ℂ 2 (parameterMeasure ν))
(hR : ∀ f : spectralCore μ ν,
(R (spectralEmbed μ ν f) : H × ℝ → ℂ) =ᵐ[parameterMeasure ν] ridgelet μ ρ f) :
IsClosed (Set.range R) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_extension_coefficient, theorem in Challenge/Transform.lean:
/-- **Theorem [thm:general-weights]** Abstract-weight extension. Theorem `thm:B`(ii) for the
abstract pair: `R_ρ = W_ρ U`. -/
theorem thm_general_weights_extension_coefficient (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ)
(R : spectralRange μ ν →L[ℂ] Lp ℂ 2 (parameterMeasure ν))
(hR : ∀ f : spectralCore μ ν,
(R (spectralEmbed μ ν f) : H × ℝ → ℂ) =ᵐ[parameterMeasure ν] ridgelet μ ρ f) :
∀ G : spectralRange μ ν, R G = spectralCoefficient ν ρ ((G : Lp ℂ 2 ν) : H → ℂ) := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_injective, theorem in Challenge/Transform.lean:
/-- **Theorem [thm:general-weights]** Abstract-weight extension. Theorem `thm:B`(iii) for the
abstract pair: `R_ρ f = 0` `λ`-a.e. implies `f = 0` `μ`-a.e. for `f ∈ L²(μ)`. -/
theorem thm_general_weights_injective (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (f : H → ℂ) (hf : MemLp f 2 μ)
(h : ridgelet μ ρ f =ᵐ[parameterMeasure ν] 0) :
f =ᵐ[μ] 0 := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_one_mem_iff, theorem in Challenge/Transform.lean:
/-- **Theorem [thm:general-weights]** Abstract-weight extension. `1 ∈ 𝒟_{μ,ν}` if and only if
`∫ |μ̂(ξ)|² ν(dξ) < ∞`. -/
theorem thm_general_weights_one_mem_iff (μ ν : Measure H) [IsProbabilityMeasure μ]
[SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) :
MemLp.toLp (fun _ : H => (1 : ℂ)) (memLp_const 1) ∈ spectralCore μ ν ↔
Integrable (fun ξ : H => ‖charFun μ ξ‖ ^ 2) ν := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_dense, theorem in Challenge/Revision.lean:
/-- **Theorem [thm:general-weights]** Bounded-set finite direction weights retain universality. -/
theorem thm_general_weights_dense (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure]
{α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
(hfin : ∀ R : ℝ, ν (Metric.closedBall (0 : H) R) < ⊤)
(β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
(hβ : IsTemperedFunction β b) (hpoly : ¬ IsPolynomialFun b) (ρ : SchwartzMap ℝ ℝ)
(hρ : IsBandPass ρ) (hC : temperedAdmissibilityConst α β ρ = 1) (I : Set ℝ)
(hI : IsFrequencyWindow ρ I) {f : H → ℂ} (hf : Continuous f) {K : Set H}
(hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) :
∃ (N : ℕ) (v : Fin N → ℂ) (a : Fin N → H) (c : Fin N → ℝ),
compactSupNorm K (fun x => f x - finiteNetwork (fun t => (b t : ℂ)) v a c x) < ε := by
Status: verified by comparator.
OperatorRidgelet.Paper.thm_general_weights_backprojection, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Theorem [thm:general-weights]** Abstract input weights retain completed backprojection. -/
theorem thm_general_weights_backprojection (μ ν : 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.
OperatorRidgelet.Paper.thm_general_weights_stability, theorem in Challenge/Revision.lean:
omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Theorem [thm:general-weights]** Stability holds for an arbitrary probability input weight. -/
theorem thm_general_weights_stability (μ ν : 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.