8.9.1. Lemma B.1 — The coefficient operator is a scaled isometry (lem:coefficient-isometry)🔗

Blueprint node: Lemma 2.2.6. Status: verified (all 6 Lean theorems verified).

Formalization note. Stated for an abstract σ-finite homogeneous ν; the formula claim is def_spectral_coefficient (shared with def:spectral-coefficient).

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

/-- **Lemma [lem:coefficient-isometry]** The coefficient operator is a scaled isometry.  `W_ρ G`
is well defined: there is exactly one element of `L²(λ)` whose partial Fourier transform in the
bias is `ρ̂(ω) G(-ωa)`. -/
theorem lem_coefficient_isometry_i {α : ℝ} (hα : 0 < α) (ν : Measure H) [SigmaFinite ν]
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → ℂ)
    (hG : Measurable G) (hG₂ : MemLp G 2 ν) :
    ∃! γ : Lp ℂ 2 (parameterMeasure ν),
      HasBiasFourier ν γ (fun a ω => filterFourier ρ ω * G (-(ω • a))) := by

Status: verified by comparator.

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

/-- **Lemma [lem:coefficient-isometry]** The coefficient operator is a scaled isometry.  `W_ρ G`
does not depend on the Borel representative of `G`. -/
theorem lem_coefficient_isometry_ii {α : ℝ} (hα : 0 < α) (ν : Measure H) [SigmaFinite ν]
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G G' : H → ℂ)
    (hG : Measurable G) (hG' : Measurable G') (hG₂ : MemLp G 2 ν) (hGG' : G =ᵐ[ν] G') :
    spectralCoefficient ν ρ G = spectralCoefficient ν ρ G' := by

Status: verified by comparator.

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

/-- **Lemma [lem:coefficient-isometry]** The coefficient operator is a scaled isometry.
`‖W_ρ G‖²_{L²(λ)} = C^{(α)}_ρ ‖G‖²_{L²(ν)}`. -/
theorem lem_coefficient_isometry_iii {α : ℝ} (hα : 0 < α) (ν : Measure H) [SigmaFinite ν]
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → ℂ)
    (hG : Measurable G) (hG₂ : MemLp G 2 ν) :
    ∫ p, ‖(spectralCoefficient ν ρ G : H × ℝ → ℂ) p‖ ^ 2 ∂parameterMeasure ν =
      admissibilityConst α ρ * ∫ ξ, ‖G ξ‖ ^ 2 ∂ν := by

Status: verified by comparator.

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

/-- **Lemma [lem:coefficient-isometry]** The coefficient operator is a scaled isometry.  If
`G ∈ L¹(ν)`, then `ω ↦ G(-ωa)` is integrable on compact subsets of `ℝ ∖ {0}` for `ν`-almost
every `a`. -/
theorem lem_coefficient_isometry_iv {α : ℝ} (hα : 0 < α) (ν : Measure H) [SigmaFinite ν]
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → ℂ)
    (hG : Measurable G) (hG₁ : Integrable G ν) :
    ∀ᵐ a ∂ν, ∀ I : Set ℝ, IsCompact I → (0 : ℝ) ∉ I →
      IntegrableOn (fun ω : ℝ => G (-(ω • a))) I := by

Status: verified by comparator.

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

/-- **Definition [def:spectral-coefficient]** The coefficient operator.  For
`G ∈ L²(ν)` the coefficient `W_ρ G` is given by the explicit formula
`γ_G(a,c) = (2π)⁻¹ ∫ ρ̂(ω) G(-ωa) e^{iωc} dω`, `λ`-almost everywhere. -/
theorem def_spectral_coefficient {α : ℝ} (hα : 0 < α) (ν : Measure H) [SigmaFinite ν]
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) (G : H → ℂ)
    (hG : Measurable G) (hG₂ : MemLp G 2 ν) :
    (spectralCoefficient ν ρ G : H × ℝ → ℂ) =ᵐ[parameterMeasure ν] coefficientFormula ρ G := by

Status: verified by comparator.

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

omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Lemma [lem:coefficient-isometry]** The L² inverse formula is absolutely integrable
on almost every ray, for every bias value. -/
theorem lem_coefficient_isometry_v {α : ℝ} (hα : 0 < α) (ν : Measure H) [SigmaFinite ν]
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ)
    (G : H → ℂ) (hG : Measurable G) (hG₂ : MemLp G 2 ν) :
    ∀ᵐ a ∂ν, ∀ c : ℝ, Integrable (fun ω : ℝ =>
      filterFourier ρ ω * G (-(ω • a)) * Complex.exp ((ω * c : ℝ) * Complex.I)) := by

Status: verified by comparator.

8.9.2. Lemma B.2 — An integrable spectral density defines a unique continuous target (lem:spectral-target-basic)🔗

Blueprint node: Lemma 3.1.1. Status: verified (all 3 Lean theorems verified).

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

omit [CompleteSpace H] [SecondCountableTopology H] [BorelSpace H] [CompleteSpace Y]
  [SecondCountableTopology Y] in
/-- **Lemma [lem:spectral-target-basic]** The spectral target has the uniform L¹ norm bound. -/
theorem lem_spectral_target_basic_i (ν : Measure H) (G : H → Y) (_hG : Integrable G ν) :
    ∀ x : H, ‖spectralTarget ν G x‖ ≤ ∫ ξ, ‖G ξ‖ ∂ν := by

Status: verified by comparator.

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

omit [CompleteSpace H] [SecondCountableTopology H] [CompleteSpace Y]
  [SecondCountableTopology Y] in
/-- **Lemma [lem:spectral-target-basic]** An integrable spectral density has a continuous target. -/
theorem lem_spectral_target_basic_ii (ν : Measure H) (G : H → Y) (hG : Integrable G ν) :
    Continuous (spectralTarget ν G) := by

Status: verified by comparator.

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

/-- **Lemma [lem:spectral-target-basic]** A spectral density is determined by its target. -/
theorem lem_spectral_target_basic_iii (ν : Measure H) (G : H → Y) (hG : Integrable G ν)
    (hzero : spectralTarget ν G = 0) : G =ᵐ[ν] 0 := by

Status: verified by comparator.

8.9.3. Lemma B.3 — Finite-order coefficient decay and moments (lem:coefficient-finite-order)🔗

Blueprint node: Lemma 3.1.3. Status: verified (all 5 Lean theorems verified).

Formalization note. Finite C^(r+2) ray regularity gives A_(r+2,r) moments; decay and moment constants are explicit definitions depending only on the filter and order, independent of the output space.

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

omit [CompleteSpace H] [SecondCountableTopology H] [CompleteSpace Y]
  [SecondCountableTopology Y] in
/-- **Lemma [lem:coefficient-finite-order]** A bounded density with a finite ray moment is L¹∩L². -/
theorem lem_coefficient_finite_order_i (ν : Measure H) {α : ℝ}
    (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ)
    (I : Set ℝ) (hI : IsFrequencyWindow ρ I) (G : H → Y) (hG : StronglyMeasurable G)
    (hbound : ∃ M : ℝ, ∀ ξ, ‖G ξ‖ ≤ M) (r : ℕ)
    (hM : finiteRayMoment ν I G (r + 2) r < ⊤) :
    Integrable G ν ∧ MemLp G 2 ν := by

Status: verified by comparator.

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

omit [CompleteSpace H] [SecondCountableTopology H] in
/-- **Lemma [lem:coefficient-finite-order]** The inverse integral represents the coefficient. -/
theorem lem_coefficient_finite_order_ii (ν : Measure H) [SigmaFinite ν] {α : ℝ}
    (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ)
    (I : Set ℝ) (hI : IsFrequencyWindow ρ I) (G : H → Y) (hG : StronglyMeasurable G)
    (hbound : ∃ M : ℝ, ∀ ξ, ‖G ξ‖ ≤ M) (r : ℕ)
    (hM : finiteRayMoment ν I G (r + 2) r < ⊤) :
    StronglyMeasurable (coefficientFormulaVec ρ G) ∧
      (spectralCoefficientVec ν ρ G : H × ℝ → Y) =ᵐ[parameterMeasure ν]
        coefficientFormulaVec ρ G := by

Status: verified by comparator.

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

omit [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  [CompleteSpace Y] [SecondCountableTopology Y] in
/-- **Lemma [lem:coefficient-finite-order]** Finitely many ray derivatives give pointwise decay. -/
theorem lem_coefficient_finite_order_iii (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ)
    (I : Set ℝ) (hI : IsFrequencyWindow ρ I) (r : ℕ) :
    0 < finiteCoefficientDecayConstant ρ (r + 2) ∧
      finiteCoefficientDecayConstant ρ (r + 2) < ⊤ ∧ ∀ G : H → Y,
      (∀ a : H, ∃ U : Set ℝ, IsOpen U ∧ I ⊆ U ∧
        ContDiffOn ℝ (r + 2 : ℕ) (fun ω : ℝ => G (ω • a)) U) →
      ∀ (a : H) (c : ℝ),
        ENNReal.ofReal ((1 + |c|) ^ (r + 2)) * ‖coefficientFormulaVec ρ G (a, c)‖ₑ ≤
          finiteCoefficientDecayConstant ρ (r + 2) * rayDerivBound I G (r + 2) a := by

Status: verified by comparator.

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

omit [CompleteSpace H] [SecondCountableTopology H] [CompleteSpace Y]
  [SecondCountableTopology Y] in
/-- **Lemma [lem:coefficient-finite-order]** The parameter moment is bounded by A_{r+2,r}. -/
theorem lem_coefficient_finite_order_iv (ν : Measure H) [SigmaFinite ν]
    (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ) (hI : IsFrequencyWindow ρ I)
    (r : ℕ) :
    finiteCoefficientMomentConstant ρ r ≠ ⊤ ∧ ∀ G : H → Y, StronglyMeasurable G →
      (∀ a : H, ∃ U : Set ℝ, IsOpen U ∧ I ⊆ U ∧
        ContDiffOn ℝ (r + 2 : ℕ) (fun ω : ℝ => G (ω • a)) U) →
      ∫⁻ θ : H × ℝ, ENNReal.ofReal ((1 + ‖θ.1‖ + |θ.2|) ^ r) *
          ‖coefficientFormulaVec ρ G θ‖ₑ ∂parameterMeasure ν ≤
        finiteCoefficientMomentConstant ρ r * finiteRayMoment ν I G (r + 2) r := by

Status: verified by comparator.

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

omit [CompleteSpace H] [SecondCountableTopology H] [CompleteSpace Y]
  [SecondCountableTopology Y] in
/-- **Lemma [lem:coefficient-finite-order]** Finite ray data imply a finite parameter moment. -/
theorem lem_coefficient_finite_order_v (ν : Measure H) [SigmaFinite ν]
    (ρ : SchwartzMap ℝ ℝ) (hρ : IsBandPass ρ) (I : Set ℝ) (hI : IsFrequencyWindow ρ I)
    (G : H → Y) (hG : StronglyMeasurable G) (r : ℕ)
    (hGs : ∀ a : H, ∃ U : Set ℝ, IsOpen U ∧ I ⊆ U ∧
      ContDiffOn ℝ (r + 2 : ℕ) (fun ω : ℝ => G (ω • a)) U)
    (hM : finiteRayMoment ν I G (r + 2) r < ⊤) :
    Integrable (fun θ : H × ℝ => (1 + ‖θ.1‖ + |θ.2|) ^ r *
      ‖coefficientFormulaVec ρ G θ‖) (parameterMeasure ν) := by

Status: verified by comparator.

8.9.4. Lemma B.4 — Synthesis of an integrable coefficient is the integral network (lem:weak-equals-strong)🔗

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

Formalization note. γ ∈ L¹(λ_α) ∩ L²(λ_α) is γ : Lp ℂ 2 (parameterMeasure ν) with Integrable γ; S_ρ[γ λ_α] is integralNetworkDensity (fun t => (ρ t : ℂ)) (parameterMeasure ν) γ. Part i: measurable and bounded (ν σ-finite; no μ is involved). Part ii is stated with the defining pairing (S_ρ γ)[g] = ⟨γ, R_ρ g⟩_{L²(λ_α)} written out with the transform ridgelet μ ρ g on 𝒟_α, since the lemma assumes only that ρ is real Schwartz (for admissible ρ this is synthesis μ ν ρ γ (spectralEmbed μ ν g) by Theorem thm:B(ii)).

OperatorRidgelet.Paper.lem_weak_equals_strong_i, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:weak-equals-strong]** Synthesis of an integrable coefficient is the integral
network.  For real Schwartz `ρ` and `γ ∈ L¹(λ_α) ∩ L²(λ_α)`, the integral network
`S_ρ[γ λ_α]` is a bounded Borel function on `H`. -/
theorem lem_weak_equals_strong_i (ν : Measure H) [SigmaFinite ν] (ρ : SchwartzMap ℝ ℝ)
    (γ : Lp ℂ 2 (parameterMeasure ν)) (hγ : Integrable γ (parameterMeasure ν)) :
    Measurable (integralNetworkDensity (fun t => (ρ t : ℂ)) (parameterMeasure ν) γ) ∧
      ∃ M : ℝ, ∀ x : H,
        ‖integralNetworkDensity (fun t => (ρ t : ℂ)) (parameterMeasure ν) γ x‖ ≤ M := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_weak_equals_strong_ii, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:weak-equals-strong]** Synthesis of an integrable coefficient is the integral
network.  For every `g ∈ 𝒟_α`, the synthesis functional `(S_ρ γ)[g] = ⟨γ, R_ρ g⟩_{L²(λ_α)}`
of `eq:weak-synthesis` equals `∫ S_ρ[γ λ_α](x) conj(g(x)) μ_Q(dx)`. -/
theorem lem_weak_equals_strong_ii (μ ν : Measure H) [IsProbabilityMeasure μ] [SigmaFinite ν]
    (ρ : SchwartzMap ℝ ℝ) (γ : Lp ℂ 2 (parameterMeasure ν))
    (hγ : Integrable γ (parameterMeasure ν)) :
    ∀ g : spectralCore μ ν,
      ∫ p, γ p * (starRingEnd ℂ) (ridgelet μ ρ g p) ∂parameterMeasure ν =
        ∫ x, integralNetworkDensity (fun t => (ρ t : ℂ)) (parameterMeasure ν) γ x *
          (starRingEnd ℂ) ((g : Lp ℂ 2 μ) x) ∂μ := by

Status: verified by comparator.

8.9.5. Lemma B.5 — Entire extension and totality of the Hermite coefficients (lem:hermite-totality)🔗

Blueprint node: Lemma 3.2.5. Status: verified (all 6 Lean theorems verified).

Formalization note. 𝒢_Q f(zξ) for complex z is the analytic continuation gaussFourierLine μ f ξ z = ∫ f(x) e^{-iz⟨x,ξ⟩} dμ, and G_f(zξ) = hermiteExtension μ Q f ξ z = e^{z²⟨Qξ,ξ⟩/2} 𝒢_Q f(zξ); He_n is Mathlib's Polynomial.hermite (probabilists' normalization, He_{n+1} = X He_n − He_n'), evaluated at ⟨x,ξ⟩/√⟨Qξ,ξ⟩ through Polynomial.aeval; the coefficients E_{μ_Q}[f He_n(⟨x,ξ⟩/τ)] are hermiteCoefficient μ Q f ξ n. Parts: i entire (Differentiable ℂ), ii the series (HasSum for every z), iii locally uniform convergence of the partial sums (TendstoLocallyUniformly), iv the bound with ‖f‖_{L²} = √∫|f|², v the Hermite inversion formula (real-variable iterated derivative at 0), vi totality (the coefficients over all ξ ≠ 0 and n determine f in L²(μ_Q), as injectivity). μ = 𝒩(0,Q) with Q a trace-class covariance. Part (vi) carries [Nontrivial H]: on a trivial space no ξ ≠ 0 exists, the hypothesis is vacuous and the conclusion fails. The manuscript is unaffected, since H is infinite-dimensional throughout.

OperatorRidgelet.Paper.lem_hermite_totality_i, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
For `f ∈ L²(μ_Q)` and `ξ ≠ 0`, `z ↦ G_f(zξ) = e^{z²τ(ξ)²/2} 𝒢_Q f(zξ)` is entire. -/
theorem lem_hermite_totality_i {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (f : H → ℂ) (hf : MemLp f 2 μ)
    (ξ : H) (hξ : ξ ≠ 0) :
    Differentiable ℂ (hermiteExtension μ Q f ξ) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_hermite_totality_ii, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The Hermite series `G_f(zξ) = ∑ₙ (-izτ(ξ))^n/n! E_{μ_Q}[f He_n(⟨x,ξ⟩/τ(ξ))]` converges for every
`z`. -/
theorem lem_hermite_totality_ii {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (f : H → ℂ) (hf : MemLp f 2 μ)
    (ξ : H) (hξ : ξ ≠ 0) :
    ∀ z : ℂ,
      HasSum
        (fun n : ℕ => (-(Complex.I * z * ((Real.sqrt ⟪Q ξ, ξ⟫ : ℝ) : ℂ))) ^ n / (n.factorial : ℂ) *
          hermiteCoefficient μ Q f ξ n)
        (hermiteExtension μ Q f ξ z) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_hermite_totality_iii, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The Hermite series converges locally uniformly in `z`. -/
theorem lem_hermite_totality_iii {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (f : H → ℂ) (hf : MemLp f 2 μ)
    (ξ : H) (hξ : ξ ≠ 0) :
    TendstoLocallyUniformly
      (fun N : ℕ => fun z : ℂ => ∑ n ∈ Finset.range N,
        (-(Complex.I * z * ((Real.sqrt ⟪Q ξ, ξ⟫ : ℝ) : ℂ))) ^ n / (n.factorial : ℂ) *
          hermiteCoefficient μ Q f ξ n)
      (hermiteExtension μ Q f ξ) atTop := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_hermite_totality_iv, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The bound `|G_f(zξ)| ≤ ‖f‖_{L²(μ_Q)} e^{|z|²τ(ξ)²/2}`. -/
theorem lem_hermite_totality_iv {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (f : H → ℂ) (hf : MemLp f 2 μ)
    (ξ : H) (hξ : ξ ≠ 0) :
    ∀ z : ℂ,
      ‖hermiteExtension μ Q f ξ z‖ ≤
        Real.sqrt (∫ x, ‖f x‖ ^ 2 ∂μ) * Real.exp (‖z‖ ^ 2 * ⟪Q ξ, ξ⟫ / 2) := by

Status: verified by comparator.

OperatorRidgelet.Paper.lem_hermite_totality_v, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The Hermite inversion formula `eq:hermite-inversion` holds for `f ∈ L²(μ_Q)` and `ξ ≠ 0`. -/
theorem lem_hermite_totality_v {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q) (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (f : H → ℂ) (hf : MemLp f 2 μ)
    (ξ : H) (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.lem_hermite_totality_vi, theorem in Challenge/Reconstruction.lean:

/-- **Lemma [lem:hermite-totality]** Entire extension and totality of the Hermite coefficients.
The Hermite coefficients over all `ξ ≠ 0` and `n` determine `f` in `L²(μ_Q)`. -/
theorem lem_hermite_totality_vi [Nontrivial H] {Q : H →L[ℝ] H} (hQ : IsTraceClassCovariance Q)
    (μ : Measure H)
    [IsProbabilityMeasure μ] (hμ : IsCenteredGaussian Q μ) (f : H → ℂ) (hf : MemLp f 2 μ) :
    ∀ g : H → ℂ, MemLp g 2 μ →
      (∀ ξ : H, ξ ≠ 0 → ∀ n : ℕ, hermiteCoefficient μ Q f ξ n = hermiteCoefficient μ Q g ξ n) →
        f =ᵐ[μ] g := by

Status: verified by comparator.

8.9.6. Proposition B.8 — Bounded backprojection and orthogonal range projection (prop:coefficient-projection)🔗

Blueprint node: Proposition 3.2.6. Status: verified (all 8 Lean theorems verified).

Formalization note. 𝒴 = L²(λ_α) with its usual norm (the norm through the partial bias Fourier transform equals the L²(λ_α)-norm by Plancherel). Λ_ρ = backprojection α ν ρ γ is the ray average eq:ray-average of a jointly measurable bias-Fourier representative of γ chosen through HasBiasFourier; backprojectionOf α ρ Φ is the ray average of a given representative Φ. Parts: i absolute convergence ν_α-a.e. for every jointly measurable representative, ii independence of the representative (a.e. equality of the ray averages of two representatives), iii square integrability with ∫|Λ_ρ γ|² ≤ C ‖γ‖² (the bound ‖Λ_ρ γ‖ ≤ √C ‖γ‖_𝒴 squared), iv the Hilbert-adjoint identity ⟨γ, W_ρ F⟩_{L²(λ_α)} = ⟨Λ_ρ γ, F⟩_{L²(ν_α)} in the manuscript's convention (linear in the first argument), v Λ_ρ W_ρ = C Id a.e., vi Π_ρ = coefficientProjection = C⁻¹ W_ρ P_{𝒦_α} Λ_ρ (with Mathlib's starProjection onto spectralRange, which is complete) is the orthogonal projection onto Ran R_ρ = ridgeletRange, encoded as Π_ρ γ ∈ Ran R_ρ and γ − Π_ρ γ ∈ (Ran R_ρ)ᗮ, vii the minimum-norm solution C⁻¹ R_ρ J_α⁻¹ F of S_ρ γ = F (it solves the equation and has the least norm among solutions), viii the solution set is the minimum-norm solution plus (Ran R_ρ)ᗮ. ρ is α-admissible as in the manuscript; parts vi–viii involve μ through 𝒦_α and R_ρ.

OperatorRidgelet.Paper.prop_coefficient_projection_i, theorem in Challenge/Reconstruction.lean:

/-- **Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  For `γ ∈ L²(λ_α)` and a jointly measurable partial bias-Fourier representative
`Φ` of `γ`, the ray-average integral `eq:ray-average` converges absolutely for `ν_α`-almost
every `ξ`. -/
theorem prop_coefficient_projection_i (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure]
    {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ)
    (γ : Lp ℂ 2 (parameterMeasure ν)) (Φ : H → ℝ → ℂ) (hΦ : Measurable (Function.uncurry Φ))
    (hγΦ : HasBiasFourier ν γ Φ) :
    ∀ᵐ ξ ∂ν,
      Integrable fun ω : ℝ =>
        (starRingEnd ℂ) (filterFourier ρ ω) * ((|ω| ^ (-α) : ℝ) : ℂ) * Φ (-(ω⁻¹ • ξ)) ω := by

Status: verified by comparator.

OperatorRidgelet.Paper.prop_coefficient_projection_ii, theorem in Challenge/Reconstruction.lean:

/-- **Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  As an `L²(ν_α)` class, `Λ_ρ γ` does not depend on the jointly measurable
Fourier representative of `γ`. -/
theorem prop_coefficient_projection_ii (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure]
    {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ)
    (γ : Lp ℂ 2 (parameterMeasure ν)) (Φ Φ' : H → ℝ → ℂ) (hΦ : Measurable (Function.uncurry Φ))
    (hΦ' : Measurable (Function.uncurry Φ')) (hγΦ : HasBiasFourier ν γ Φ)
    (hγΦ' : HasBiasFourier ν γ Φ') :
    backprojectionOf α ρ Φ =ᵐ[ν] backprojectionOf α ρ Φ' := by

Status: verified by comparator.

OperatorRidgelet.Paper.prop_coefficient_projection_iii, theorem in Challenge/Reconstruction.lean:

/-- **Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  `Λ_ρ γ ∈ L²(ν_α)` with `‖Λ_ρ γ‖_{L²(ν_α)} ≤ √C ‖γ‖_𝒴`, `C = C^{(α)}_ρ`. -/
theorem prop_coefficient_projection_iii (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure]
    {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ) :
    ∀ γ : Lp ℂ 2 (parameterMeasure ν),
      MemLp (backprojection α ν ρ γ) 2 ν ∧
        ∫ ξ, ‖backprojection α ν ρ γ ξ‖ ^ 2 ∂ν ≤ admissibilityConst α ρ * ‖γ‖ ^ 2 := by

Status: verified by comparator.

OperatorRidgelet.Paper.prop_coefficient_projection_iv, theorem in Challenge/Reconstruction.lean:

/-- **Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  `Λ_ρ` is the Hilbert adjoint of `W_ρ : L²(ν_α) → 𝒴`:
`⟨γ, W_ρ F⟩_{L²(λ_α)} = ⟨Λ_ρ γ, F⟩_{L²(ν_α)}`. -/
theorem prop_coefficient_projection_iv (ν : Measure H) [SigmaFinite ν] [ν.IsOpenPosMeasure]
    {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
    (hρ : IsAdmissible α ρ) :
    ∀ (γ : Lp ℂ 2 (parameterMeasure ν)) (F : H → ℂ), Measurable F → MemLp F 2 ν →
      ∫ p, γ p * (starRingEnd ℂ) ((spectralCoefficient ν ρ F : H × ℝ → ℂ) p)
          ∂parameterMeasure ν =
        ∫ ξ, backprojection α ν ρ γ ξ * (starRingEnd ℂ) (F ξ) ∂ν := by

Status: verified by comparator.

OperatorRidgelet.Paper.prop_coefficient_projection_v, theorem in Challenge/Reconstruction.lean:

/-- **Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  `Λ_ρ W_ρ = C Id`. -/
theorem prop_coefficient_projection_v (ν : 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.prop_coefficient_projection_vi, theorem in Challenge/Reconstruction.lean:

/-- **Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  `Π_ρ = C⁻¹ W_ρ P_{𝒦_α} Λ_ρ` is the orthogonal projection onto `Ran R_ρ`:
`Π_ρ γ ∈ Ran R_ρ` and `γ - Π_ρ γ ⊥ Ran R_ρ`. -/
theorem prop_coefficient_projection_vi (μ ν : Measure H) [IsProbabilityMeasure μ]
    [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) :
    ∀ γ : Lp ℂ 2 (parameterMeasure ν),
      coefficientProjection α μ ν ρ γ ∈ ridgeletRange μ ν ρ ∧
        γ - coefficientProjection α μ ν ρ γ ∈ (ridgeletRange μ ν ρ)ᗮ := by

Status: verified by comparator.

OperatorRidgelet.Paper.prop_coefficient_projection_vii, theorem in Challenge/Reconstruction.lean:

/-- **Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  The minimum-norm solution of `S_ρ γ = F ∈ 𝓔_α'` is `C⁻¹ R_ρ J_α⁻¹ F`: it solves
the equation, and every solution has at least its norm. -/
theorem prop_coefficient_projection_vii (μ ν : Measure H) [IsProbabilityMeasure μ]
    [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) :
    ∀ F : SpectralAntiDual μ ν,
      synthesis μ ν ρ
          ((((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) • ridgeletExtension μ ν ρ (rieszInv μ ν F)) =
        F ∧
      ∀ γ : Lp ℂ 2 (parameterMeasure ν), synthesis μ ν ρ γ = F →
        ‖(((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) • ridgeletExtension μ ν ρ (rieszInv μ ν F)‖ ≤
          ‖γ‖ := by

Status: verified by comparator.

OperatorRidgelet.Paper.prop_coefficient_projection_viii, theorem in Challenge/Reconstruction.lean:

/-- **Proposition [prop:coefficient-projection]** Bounded backprojection and orthogonal range
projection.  The solutions of `S_ρ γ = F` are exactly the coefficients that differ from the
minimum-norm solution by an element of `(Ran R_ρ)^⊥`. -/
theorem prop_coefficient_projection_viii (μ ν : Measure H) [IsProbabilityMeasure μ]
    [SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α) (hν : IsHomogeneous α ν)
    (ρ : SchwartzMap ℝ ℝ) (hρ : IsAdmissible α ρ) :
    ∀ (F : SpectralAntiDual μ ν) (γ : Lp ℂ 2 (parameterMeasure ν)),
      synthesis μ ν ρ γ = F ↔
        γ - (((admissibilityConst α ρ)⁻¹ : ℝ) : ℂ) • ridgeletExtension μ ν ρ (rieszInv μ ν F) ∈
          (ridgeletRange μ ν ρ)ᗮ := by

Status: verified by comparator.