Estimation.NPIV.Operator
The NPIV conditional-expectation operator: compactness, singular systems, and the source condition.
Operator 9 core · 6 supporting Extends the inverse-problem system with population operators for NPIV estimation. ★ T_inner_eq_integral
Extends the inverse-problem system with population operators for NPIV estimation. The module defines the operator interface connecting structural functions, instruments, and conditional-moment equations.
structure OperatorSystem reviewed
⚑ flagged
Causalean.Estimation.NPIV
An operator system: an InverseProblemSystem enriched with the L² data needed to define the concrete population projection operator T = Π_{Q̄} ∘ E[· | σ(Z)]. On top of the base system it packages the σ-algebra generated by the instrument Z, with the facts that it is coarser than the ambient σ-algebra on the sample space and coincides with the σ-algebra pulled back along Z, that the ambient probability measure is finite, and closed submodules of the ambient L²(μ) space realizing the primal and dual candidate function classes, the dual one further required to admit an orthogonal projection; finally, every candidate primal or dual function is square-integrable once composed with the covariate or instrument map, with its L² class coherently landing inside the matching submodule.
Definition (Lean source)
parameters
fields
The σ-algebra generated by `Z = zOf ∘ W : Ω → 𝒵`.
m_Z :
`m_Z` is coarser than `m₀`.
m_Z_le :
m_Z ≤ m₀
(Optional consistency:) `m_Z = comap (zOf ∘ W) inst𝒵`. This pins the
σ-algebra to the one generated by `Z`.
m_Z_eq :
m_Z = @comap Ω 𝒵 (fun ω => zOf (W ω)) inst𝒵
`μ` is finite (sufficient for the conditional-expectation identities
used in the rate proof).
isFiniteMeasure :
L² realization of `Hbar`: a closed submodule of the ambient `Lp ℝ 2 μ`.
L² realization of `Qbar`.
`Qbar_L2` admits an orthogonal projection (in particular, is closed).
Qbar_L2_hasProj :
Qbar_L2.HasOrthogonalProjection
Embedding witness: for every `h ∈ Hbar`, the function
`ω ↦ h (X ω) = h (xOf (W ω))` is square-integrable.
toHbarL2 :
∀ h ∈ Hbar, MemLp (fun ω => h (xOf (W ω))) 2 μ
Embedding witness: for every `q ∈ Qbar`, the function
`ω ↦ q (Z ω) = q (zOf (W ω))` is square-integrable.
toQbarL2 :
∀ q ∈ Qbar, MemLp (fun ω => q (zOf (W ω))) 2 μ
Coherence: the `Lp` class of `h ∘ X` lies in the closed subspace
`Hbar_L2`.
hbar_mem_L2 :
∀ h (hh : h ∈ Hbar), (toHbarL2 h hh).toLp _ ∈ Hbar_L2
Coherence: the `Lp` class of `q ∘ Z` lies in `Qbar_L2`.
qbar_mem_L2 :
∀ q (hq : q ∈ Qbar), (toQbarL2 q hq).toLp _ ∈ Qbar_L2
def hL2 reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system and a covariate function belonging to its primal candidate set, the lifted primal candidate is the equivalence class of that function evaluated at the covariates.
Definition (Lean source)
def qL2 reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system and an instrument function belonging to its dual candidate set, the lifted dual candidate is the equivalence class of that function evaluated at the instruments.
Definition (Lean source)
def condExpStep reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the conditional-expectation operator maps every ambient random variable to its conditional expectation given the σ-algebra generated by the instrument.
Definition (Lean source)
parameters
S :
OperatorSystem Ω μ
given by
haveI := S.isFiniteMeasure fun f => (MeasureTheory.condExpL2 ℝ ℝ S.m_Z_le f : Lp ℝ 2 μ)
def T reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system and an ambient random variable, the NPIV projection operator is the orthogonal projection onto the closed dual candidate space of that variable's conditional expectation given the instrument.
Definition (Lean source)
parameters
def
given by
haveI := S.Qbar_L2_hasProj S.Qbar_L2.orthogonalProjectionFn (S.condExpStep f)
def QbarAEMeasurableMZ reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, this predicate asserts that every dual candidate, evaluated at the instrument of a sampled observation, is almost-everywhere strongly measurable with respect to the instrument-generated σ-algebra.
Definition (Lean source)
parameters
def
QbarAEMeasurableMZ S :
Prop
given by
AEStronglyMeasurable[S.m_Z] (fun ω => q (S.zOf (S.W ω))) μ
theorem T_inner_eq_integral reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
Population identity for T. Consider an operator system S — an inverse-problem system enriched with an L² realization of the candidate sets — and fix two primal candidate functions h, h' in the primal candidate set Hbar together with a dual candidate function f in the dual candidate set Qbar. Writing T for the operator that conditions on the σ-algebra generated by the instrument Z and then orthogonally projects onto the L² realization of Qbar, the L²(μ) inner product of T applied to the lifted residual h − h' against the lifted f equals the expectation of the pointwise product (h(X) − h'(X))·f(Z).
Formal statement
hypotheses
conclusion
inner ℝ (S.T (S.hL2 hh - S.hL2 hh')) (S.qL2 hf)
= ∫ ω, (h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω))) * f (S.zOf (S.W ω)) ∂μ
Proof (Lean source)
theorem T_inner_eq_integral
(S : OperatorSystem Ω μ)
{h h' : S.𝒳 → ℝ} (hh : h ∈ S.Hbar) (hh' : h' ∈ S.Hbar)
{f : S.𝒵 → ℝ} (hf : f ∈ S.Qbar) :
inner ℝ (S.T (S.hL2 hh - S.hL2 hh')) (S.qL2 hf)
= ∫ ω, (h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω))) *
f (S.zOf (S.W ω)) ∂μ := by
haveI := S.isFiniteMeasure
haveI := S.Qbar_L2_hasProj
let u : Lp ℝ 2 μ := S.hL2 hh - S.hL2 hh'
have hq_mem : S.qL2 hf ∈ S.Qbar_L2 := S.qbar_mem_L2 f hf
have h_proj :
inner ℝ (S.T u) (S.qL2 hf) =
inner ℝ (S.condExpStep u) (S.qL2 hf) := by
have h_zero :
inner ℝ (S.condExpStep u - S.Qbar_L2.orthogonalProjectionFn (S.condExpStep u))
(S.qL2 hf) = 0 :=
S.Qbar_L2.orthogonalProjectionFn_inner_eq_zero (S.condExpStep u) (S.qL2 hf) hq_mem
have h_eq :
inner ℝ (S.condExpStep u) (S.qL2 hf) =
inner ℝ (S.Qbar_L2.orthogonalProjectionFn (S.condExpStep u)) (S.qL2 hf) := by
rw [inner_sub_left] at h_zero
exact sub_eq_zero.mp h_zero
simpa [OperatorSystem.T] using h_eq.symm
have hq_meas :
AEStronglyMeasurable[S.m_Z] (S.qL2 hf : Ω → ℝ) μ :=
(S.qbar_aestrongly_measurable_mZ f hf).congr (S.toQbarL2 f hf).coeFn_toLp.symm
have h_cond :
inner ℝ (S.condExpStep u) (S.qL2 hf) =
inner ℝ u (S.qL2 hf) := by
simpa [OperatorSystem.condExpStep] using
(MeasureTheory.inner_condExpL2_eq_inner_fun (E := ℝ) (𝕜 := ℝ)
S.m_Z_le u (S.qL2 hf) hq_meas)
have h_inner :
inner ℝ u (S.qL2 hf) =
∫ ω, (h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω))) *
f (S.zOf (S.W ω)) ∂μ := by
rw [MeasureTheory.L2.inner_def]
refine integral_congr_ae ?_
filter_upwards [Lp.coeFn_sub (S.hL2 hh) (S.hL2 hh'),
(S.toHbarL2 h hh).coeFn_toLp, (S.toHbarL2 h' hh').coeFn_toLp,
(S.toQbarL2 f hf).coeFn_toLp] with ω hu hhω hh'ω hfω
calc
⟪u ω, (S.qL2 hf) ω⟫_ℝ
= ⟪(S.hL2 hh) ω - (S.hL2 hh') ω, (S.qL2 hf) ω⟫_ℝ := by
have huω : u ω = (S.hL2 hh) ω - (S.hL2 hh') ω := by
simpa [u, Pi.sub_apply] using hu
rw [huω]
_ = ⟪h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω)),
f (S.zOf (S.W ω))⟫_ℝ := by
simp [OperatorSystem.hL2, OperatorSystem.qL2, hhω, hh'ω, hfω]
_ = (h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω))) *
f (S.zOf (S.W ω)) := by
change f (S.zOf (S.W ω)) *
(h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω))) =
(h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω))) *
f (S.zOf (S.W ω))
ring
calc
inner ℝ (S.T (S.hL2 hh - S.hL2 hh')) (S.qL2 hf)
= inner ℝ (S.T u) (S.qL2 hf) := by simp [u]
_ = inner ℝ (S.condExpStep u) (S.qL2 hf) := h_proj
_ = inner ℝ u (S.qL2 hf) := h_cond
_ = ∫ ω, (h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω))) *
f (S.zOf (S.W ω)) ∂μ := h_inner
def strongNorm reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system and an ambient random variable, the strong norm is that variable's norm.
Definition (Lean source)
parameters
def
strongNorm _S f :
ℝ
given by
‖f‖
def weakNorm reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system and an ambient random variable, the weak norm is the norm of its projected conditional expectation.
Definition (Lean source)
parameters
def
weakNorm S f :
ℝ
given by
‖S.T f‖
6 supporting declarations (lemmas, instances)
-
condExpStep_sublemma — condExpStep distributes over subtraction (linearity of condExpL2).hypothesesconclusionS.condExpStep (f - g) = S.condExpStep f - S.condExpStep gProof (Lean source)
lemma condExpStep_sub (S : OperatorSystem Ω μ) (f g : Lp ℝ 2 μ) : S.condExpStep (f - g) = S.condExpStep f - S.condExpStep g := by haveI := S.isFiniteMeasure unfold condExpStep simp [map_sub] -
T_sublemma — T distributes over subtraction.hypothesesconclusionS.T (f - g) = S.T f - S.T gProof (Lean source)
lemma T_sub (S : OperatorSystem Ω μ) (f g : Lp ℝ 2 μ) : S.T (f - g) = S.T f - S.T g := by haveI := S.Qbar_L2_hasProj unfold T rw [S.condExpStep_sub] -- Reduce `orthogonalProjectionFn (a - b)` to -- `orthogonalProjectionFn a - orthogonalProjectionFn b` via the -- rfl-equality `orthogonalProjectionFn = ((orthogonalProjection ·) : _)` -- and `map_sub` on the bundled CLM `orthogonalProjection`. change ((S.Qbar_L2.orthogonalProjection (S.condExpStep f - S.condExpStep g)) : Lp ℝ 2 μ) = ((S.Qbar_L2.orthogonalProjection (S.condExpStep f)) : Lp ℝ 2 μ) - ((S.Qbar_L2.orthogonalProjection (S.condExpStep g)) : Lp ℝ 2 μ) rw [map_sub] rfl -
T_addlemma — T distributes over addition (companion to T_sub).hypothesesconclusionS.T (f + g) = S.T f + S.T gProof (Lean source)
lemma T_add (S : OperatorSystem Ω μ) (f g : Lp ℝ 2 μ) : S.T (f + g) = S.T f + S.T g := by haveI := S.Qbar_L2_hasProj haveI := S.isFiniteMeasure unfold T condExpStep change ((S.Qbar_L2.orthogonalProjection ((MeasureTheory.condExpL2 ℝ ℝ S.m_Z_le (f + g) : Lp ℝ 2 μ))) : Lp ℝ 2 μ) = ((S.Qbar_L2.orthogonalProjection ((MeasureTheory.condExpL2 ℝ ℝ S.m_Z_le f : Lp ℝ 2 μ))) : Lp ℝ 2 μ) + ((S.Qbar_L2.orthogonalProjection ((MeasureTheory.condExpL2 ℝ ℝ S.m_Z_le g : Lp ℝ 2 μ))) : Lp ℝ 2 μ) simp [map_add] -
qbar_aestrongly_measurable_mZlemma — q ∘ zOf ∘ W is m_Z-strongly measurable for every q ∈ Qbar. Direct consequence of m_Z_eq : m_Z = comap (zOf ∘ W) inst𝒵 and meas_of_Qbar: the canonical map (zOf ∘ W) : Ω → 𝒵 is measurable from comap (zOf ∘ W) inst𝒵 to inst𝒵 (comap_measurable), so its composition with the inst𝒵-measurable q : 𝒵 → ℝ is m_Z-measurable, hence m_Z-strongly measurable into ℝ.Proof (Lean source)
lemma qbar_aestrongly_measurable_mZ (S : OperatorSystem Ω μ) : S.QbarAEMeasurableMZ := by intro q hq have hZ : @Measurable Ω S.𝒵 S.m_Z S.inst𝒵 (fun ω => S.zOf (S.W ω)) := by rw [S.m_Z_eq] exact comap_measurable _ have hq_meas : @Measurable S.𝒵 ℝ S.inst𝒵 _ q := S.meas_of_Qbar q hq have h_meas : @Measurable Ω ℝ S.m_Z _ (fun ω => q (S.zOf (S.W ω))) := @comp Ω S.𝒵 ℝ S.m_Z S.inst𝒵 _ q (fun ω => S.zOf (S.W ω)) hq_meas hZ exact h_meas.aestronglyMeasurable -
weakNorm_le_strongNormlemma — The projected conditional-expectation norm is bounded by the ambient L² norm.hypothesesconclusionS.weakNorm f ≤ S.strongNorm fProof (Lean source)
lemma weakNorm_le_strongNorm (S : OperatorSystem Ω μ) (f : Lp ℝ 2 μ) : S.weakNorm f ≤ S.strongNorm f := by haveI := S.isFiniteMeasure haveI := S.Qbar_L2_hasProj calc S.weakNorm f = ‖S.Qbar_L2.starProjection (S.condExpStep f)‖ := by rw [weakNorm, T] _ ≤ ‖S.condExpStep f‖ := S.Qbar_L2.norm_starProjection_apply_le (S.condExpStep f) _ ≤ ‖f‖ := by simpa [condExpStep] using (MeasureTheory.norm_condExpL2_coe_le (E := ℝ) (𝕜 := ℝ) S.m_Z_le f) _ = S.strongNorm f := by rw [strongNorm] -
strongNorm_sq_hL2_eq_integrallemma — Squared strong norm of a lifted Hbar member, unfolded as the integral of the squared representative.hypothesesconclusion(S.strongNorm (S.hL2 hh)) ^ 2 = ∫ ω, (h (S.xOf (S.W ω))) ^ 2 ∂μProof (Lean source)
lemma strongNorm_sq_hL2_eq_integral (S : OperatorSystem Ω μ) {h : S.𝒳 → ℝ} (hh : h ∈ S.Hbar) : (S.strongNorm (S.hL2 hh)) ^ 2 = ∫ ω, (h (S.xOf (S.W ω))) ^ 2 ∂μ := by calc (S.strongNorm (S.hL2 hh)) ^ 2 = inner ℝ (S.hL2 hh) (S.hL2 hh) := by rw [OperatorSystem.strongNorm, real_inner_self_eq_norm_sq] _ = ∫ ω, ⟪(S.hL2 hh) ω, (S.hL2 hh) ω⟫_ℝ ∂μ := by rw [MeasureTheory.L2.inner_def] _ = ∫ ω, (h (S.xOf (S.W ω))) ^ 2 ∂μ := by refine integral_congr_ae ?_ filter_upwards [(S.toHbarL2 h hh).coeFn_toLp] with ω hω simp [OperatorSystem.hL2, hω, pow_two]
Adjoint 5 core · 1 supporting Builds the bundled continuous-linear-map representation of the NPIV operator and its adjoint. ★ Tstar_T_isSelfAdjoint
Builds the bundled continuous-linear-map representation of the NPIV operator and its adjoint. These operator-theoretic objects feed Tikhonov regularization and spectral arguments.
def condExpStepL reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the bundled conditional-expectation operator is the continuous linear map sending each ambient random variable to its conditional expectation given the σ-algebra generated by the instrument.
Definition (Lean source)
parameters
S :
OperatorSystem Ω μ
given by
haveI := S.isFiniteMeasure (lpMeas ℝ ℝ S.m_Z 2 μ).subtypeL.comp (MeasureTheory.condExpL2 ℝ ℝ S.m_Z_le)
def Tlin reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the bundled NPIV operator is the continuous linear map that conditions an ambient random variable on the instrument and then orthogonally projects it onto the closed dual candidate space.
Definition (Lean source)
parameters
S :
OperatorSystem Ω μ
given by
haveI := S.Qbar_L2_hasProj S.Qbar_L2.starProjection.comp S.condExpStepL
def Tadjoint reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the adjoint operator is the Hilbert-space adjoint of its bundled NPIV projection operator.
Definition (Lean source)
def Tstar_T reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the self-adjoint positive-semidefinite composite is its bundled NPIV operator followed by its Hilbert-space adjoint.
Definition (Lean source)
lemma Tstar_T_isSelfAdjoint reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For any NPIV operator system, the composite operator T† T, obtained by composing the second-stage conditional-expectation operator with its adjoint, is self-adjoint.
Formal statement
Proof (Lean source)
lemma Tstar_T_isSelfAdjoint (S : OperatorSystem Ω μ) :
IsSelfAdjoint S.Tstar_T := by
unfold Tstar_T Tadjoint
simpa [ContinuousLinearMap.mul_def, ContinuousLinearMap.star_eq_adjoint] using
IsSelfAdjoint.star_mul_self S.Tlin
1 supporting declaration (lemmas, instances)
-
Tlin_applylemma — Coherence: applying the bundled CLM Tlin to f agrees with the function-level operator T from Causalean/Estimation/NPIV/Operator.lean. The proof unfolds both sides and uses Submodule.starProjection_apply = orthogonalProjectionFn.hypothesesconclusionS.Tlin f = S.T fProof (Lean source)
Complexification 9 core · 13 supporting Provides real-to-complex L2 operator glue for NPIV spectral calculations. ★ realCFC_resolvent_mul_self★ realCFC_norm_le
Provides real-to-complex L2 operator glue for NPIV spectral calculations. The module relates real conditional-moment operators to complexified continuous linear maps and their self-adjointness properties.
instance instAlgebraRealLpCLM reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
For a measurable sample space equipped with a measure, the real-scalar algebra structure on the algebra of continuous complex-linear operators on complex-valued square-integrable functions is obtained by restricting the usual complex scalar algebra to real scalars.
def reLp reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
For a measurable sample space equipped with a measure, the real-part operator maps each complex-valued square-integrable function to its pointwise real part, viewed as a real-valued square-integrable function.
def imLp reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
For a measurable sample space equipped with a measure, the imaginary-part operator maps each complex-valued square-integrable function to its pointwise imaginary part, viewed as a real-valued square-integrable function.
def ιLp reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
For a measurable sample space equipped with a measure, the real-to-complex embedding maps each real-valued square-integrable function to the complex-valued square-integrable function having that real part and zero imaginary part.
def complexLiftFun reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
For a measurable sample space equipped with a measure, a continuous real-linear operator on real-valued square-integrable functions, and a complex-valued square-integrable function, the function-level complex lift is the complex-valued function obtained by applying the operator separately to the real and imaginary parts and then combining the resulting real-valued functions as real part plus times imaginary part.
def complexLift reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
For a measurable sample space equipped with a measure and a continuous real-linear operator on real-valued square-integrable functions, the complex lift is the continuous complex-linear operator on complex-valued square-integrable functions that applies the original operator separately to real and imaginary parts. It first forms the continuous real-linear operator that combines the separately transformed components, then bundles that operator as a complex-linear map.
Definition (Lean source)
parameters
given by
L :
{ toFun := M map_add' := by intro f g exact M.map_add f g map_smul' := by intro c f simpa [M, complexLiftFun, I_smulCLM] using complexLiftFun_map_smul A c f } (: Lp ℂ 2 μ →ₗ[ℂ] Lp ℂ 2 μ)
L.mkContinuous ‖M‖ (by intro f have h := M.le_opNorm f simpa [L] using h)
def realCFC reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
For a measurable sample space equipped with a measure, a continuous real-linear operator on real-valued square-integrable functions, and a real-valued function of a real argument, the real continuous-functional-calculus operator applies the complex continuous functional calculus to the complex lift of the operator with the symbol extended from the real part, then restricts the result back to real-valued square-integrable functions. It first constructs the complex functional-calculus operator, then bundles its real-valued restriction as a continuous real-linear operator.
Definition (Lean source)
parameters
given by
C :
L.mkContinuous (‖reLp‖ * ‖C‖ * ‖ιLp‖) (by intro x calc ‖L x‖ = ‖reLp (C (ιLp x))‖ := rfl _ ≤ ‖reLp‖ * ‖C (ιLp x)‖ := reLp.le_opNorm (C (ιLp x)) _ ≤ ‖reLp‖ * (‖C‖ * ‖ιLp x‖) := by gcongr exact C.le_opNorm (ιLp x) _ ≤ ‖reLp‖ * (‖C‖ * (‖ιLp‖ * ‖x‖)) := by gcongr exact ιLp.le_opNorm x _ = ‖reLp‖ * ‖C‖ * ‖ιLp‖ * ‖x‖ := by ring)
theorem realCFC_resolvent_mul_self reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
Resolvent symbol for realCFC. For a self-adjoint bounded operator A whose real spectrum lies in the nonnegative reals, and for a strictly positive regularization parameter λ, composing the real-functional-calculus operator for the affine symbol x ↦ λ + x with that for the resolvent symbol x ↦ (λ + x)⁻¹ yields the identity operator on the ambient L² space.
Formal statement
Proof (Lean source)
theorem realCFC_resolvent_mul_self
(A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hA : IsSelfAdjoint A)
(hA_spec : ∀ x ∈ spectrum ℝ A, 0 ≤ x)
(lambda : ℝ) (hlam : 0 < lambda) :
(realCFC A (fun x => lambda + x)).comp
(realCFC A (fun x => (lambda + x)⁻¹))
= id ℝ (Lp ℝ 2 μ) := by
have hsafe_ne : ∀ x : ℝ, lambda + max 0 x ≠ 0 := fun x => by
have hmax : (0 : ℝ) ≤ max 0 x := le_max_left _ _
have hpos : 0 < lambda + max 0 x := by linarith
exact ne_of_gt hpos
have hsafe_cont : Continuous (fun x : ℝ => (lambda + max 0 x)⁻¹) :=
(continuous_const.add (continuous_const.max continuous_id)).inv₀ hsafe_ne
have hagree : ∀ x ∈ spectrum ℝ A,
(lambda + max 0 x)⁻¹ = (lambda + x)⁻¹ := fun x hx => by
have hx0 : 0 ≤ x := hA_spec x hx
rw [max_eq_right hx0]
rw [← realCFC_congr_on_spectrum A (fun x => (lambda + max 0 x)⁻¹)
(fun x => (lambda + x)⁻¹) hagree hA]
rw [← realCFC_mul A hA (fun x => lambda + x)
(fun x => (lambda + max 0 x)⁻¹) (continuous_const.add continuous_id) hsafe_cont]
have hprod : ∀ x ∈ spectrum ℝ A,
(lambda + x) * (lambda + max 0 x)⁻¹ = 1 := fun x hx => by
have hx0 : 0 ≤ x := hA_spec x hx
rw [max_eq_right hx0]
have hne : lambda + x ≠ 0 := by
have hpos : 0 < lambda + x := by linarith
exact ne_of_gt hpos
exact mul_inv_cancel₀ hne
rw [realCFC_congr_on_spectrum A
(fun x => (lambda + x) * (lambda + max 0 x)⁻¹)
(fun _ : ℝ => (1 : ℝ)) hprod hA]
apply ContinuousLinearMap.ext
intro v
rw [realCFC_apply A hA (fun _ : ℝ => (1 : ℝ)) continuous_const v]
rw [ContinuousLinearMap.id_apply]
change reLp (cfc (fun _ : ℂ => (1 : ℂ)) (complexLift A) (ιLp v)) = v
rw [cfc_const_one ℂ (complexLift A)
(ha := (complexLift_isSelfAdjoint hA).isStarNormal)]
rw [ContinuousLinearMap.one_apply, reLp_comp_ιLp]
theorem realCFC_norm_le reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
Norm-via-spectrum bound for realCFC. For a self-adjoint bounded operator A and a continuous real-valued symbol f, if f is bounded in absolute value by a nonnegative constant c on the real spectrum of A, then the operator realCFC A f is a contraction up to c: for every vector g, ‖realCFC A f g‖ ≤ c · ‖g‖.
Formal statement
Proof (Lean source)
theorem realCFC_norm_le
(A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hA : IsSelfAdjoint A)
(f : ℝ → ℝ) (hf : Continuous f)
(c : ℝ) (hc : 0 ≤ c) (hsup : ∀ x ∈ spectrum ℝ A, |f x| ≤ c)
(g : Lp ℝ 2 μ) :
‖realCFC A f g‖ ≤ c * ‖g‖ := by
let Acpx : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ := complexLift A
let C : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ :=
cfc (fun z : ℂ => (f z.re : ℂ)) Acpx
rw [realCFC_apply A hA f hf g]
change ‖reLp (C (ιLp g))‖ ≤ c * ‖g‖
have hC_norm : ‖C‖ ≤ c := by
rw [show C = cfc (fun z : ℂ => (f z.re : ℂ)) Acpx by rfl]
rw [norm_cfc_le_iff (fun z : ℂ => (f z.re : ℂ)) Acpx hc
(hf := (Complex.continuous_ofReal.comp (hf.comp Complex.continuous_re)).continuousOn)
(ha := (complexLift_isSelfAdjoint hA).isStarNormal)]
intro z hz
have hzr : z.re ∈ spectrum ℝ A := spectrum_complexLift_subset_real hA hz
simpa [Complex.norm_real, Real.norm_eq_abs] using hsup z.re hzr
calc
‖reLp (C (ιLp g))‖
≤ ‖C (ιLp g)‖ := norm_reLp_le _
_ = 1 * ‖C (ιLp g)‖ := by rw [one_mul]
_ ≤ 1 * (‖C‖ * ‖ιLp g‖) := by
gcongr
exact C.le_opNorm _
_ ≤ 1 * (c * ‖ιLp g‖) := by
gcongr
_ = c * ‖g‖ := by
rw [one_mul, ιLp_isometry]
13 supporting declarations (lemmas, instances)
-
reLp_comp_ιLplemma — reLp is a left-inverse of ιLp.Proof (Lean source)
lemma reLp_comp_ιLp (f : Lp ℝ 2 μ) : reLp (ιLp f) = f := by apply Lp.ext filter_upwards [ContinuousLinearMap.coeFn_compLpL (RCLike.reCLM (K := ℂ)) (ιLp f), ContinuousLinearMap.coeFn_compLpL (RCLike.ofRealCLM (K := ℂ)) f] with ω h₁ h₂ simpa [reLp, ιLp, h₂, RCLike.reCLM_apply, RCLike.ofRealCLM_apply, RCLike.ofReal_re] using h₁ -
imLp_comp_ιLplemma — The imaginary part vanishes on the image of ιLp (pointwise RCLike.im_ofReal : RCLike.im (r : ℂ) = 0).Proof (Lean source)
lemma imLp_comp_ιLp (f : Lp ℝ 2 μ) : imLp (ιLp f) = 0 := by apply Lp.ext filter_upwards [ContinuousLinearMap.coeFn_compLpL (RCLike.imCLM (K := ℂ)) (ιLp f), ContinuousLinearMap.coeFn_compLpL (RCLike.ofRealCLM (K := ℂ)) f, (Lp.coeFn_zero ℝ (2 : ENNReal) μ)] with ω h₁ h₂ hzero have hmain : (((imLp (ιLp f) : Lp ℝ 2 μ) : Ω → ℝ) ω) = (RCLike.imCLM (K := ℂ)) ((RCLike.ofRealCLM (K := ℂ)) (((f : Lp ℝ 2 μ) : Ω → ℝ) ω)) := by simpa [imLp, ιLp, h₂] using h₁ calc (((imLp (ιLp f) : Lp ℝ 2 μ) : Ω → ℝ) ω) = (RCLike.imCLM (K := ℂ)) ((RCLike.ofRealCLM (K := ℂ)) (((f : Lp ℝ 2 μ) : Ω → ℝ) ω)) := hmain _ = 0 := by change RCLike.im ((RCLike.ofRealCLM (K := ℂ)) (((f : Lp ℝ 2 μ) : Ω → ℝ) ω)) = 0 change RCLike.im ((((f : Lp ℝ 2 μ) : Ω → ℝ) ω : ℝ) : ℂ) = 0 exact RCLike.ofReal_im (((f : Lp ℝ 2 μ) : Ω → ℝ) ω) _ = ((0 : Lp ℝ 2 μ) : Ω → ℝ) ω := by rw [hzero]; rfl -
ιLp_isometrylemma — ιLp is an isometric embedding. Follows from RCLike.ofRealLI being a LinearIsometry and the fact that compLpL of a norm-one CLM preserves norms on L²; concretely, ‖ιLp f‖ = ‖f‖ reduces pointwise to ‖(r : ℂ)‖ = ‖r‖ (RCLike.norm_ofReal).Proof (Lean source)
lemma ιLp_isometry (f : Lp ℝ 2 μ) : ‖ιLp f‖ = ‖f‖ := by rw [Lp.norm_def, Lp.norm_def] apply congrArg toReal apply MeasureTheory.eLpNorm_congr_norm_ae filter_upwards [ContinuousLinearMap.coeFn_compLpL (RCLike.ofRealCLM (K := ℂ)) f] with ω h rw [show (((ιLp f : Lp ℂ 2 μ) : Ω → ℂ) ω) = (RCLike.ofRealCLM (K := ℂ)) (((f : Lp ℝ 2 μ) : Ω → ℝ) ω) by simpa [ιLp] using h] change ‖(RCLike.ofRealCLM (K := ℂ)) (((f : Lp ℝ 2 μ) : Ω → ℝ) ω)‖ = ‖(((f : Lp ℝ 2 μ) : Ω → ℝ) ω)‖ rw [show (RCLike.ofRealCLM (K := ℂ)) (((f : Lp ℝ 2 μ) : Ω → ℝ) ω) = ((((f : Lp ℝ 2 μ) : Ω → ℝ) ω : ℝ) : ℂ) by rw [RCLike.ofRealCLM_apply] rfl] exact RCLike.norm_ofReal (((f : Lp ℝ 2 μ) : Ω → ℝ) ω) -
reLp_add_smul_imLplemma — Reconstruction identity: every complex L²-class is the complex combination of its real and imaginary parts re-embedded via ιLp. Pointwise this is RCLike.re_add_im : (r.re : ℂ) + I * r.im = r.hypothesesProof (Lean source)
lemma reLp_add_smul_imLp (f : Lp ℂ 2 μ) : ιLp (reLp f) + (Complex.I : ℂ) • ιLp (imLp f) = f := by apply Lp.ext filter_upwards [Lp.coeFn_add (ιLp (reLp f)) ((Complex.I : ℂ) • ιLp (imLp f)), Lp.coeFn_smul (Complex.I : ℂ) (ιLp (imLp f)), ContinuousLinearMap.coeFn_compLpL (RCLike.ofRealCLM (K := ℂ)) (reLp f), ContinuousLinearMap.coeFn_compLpL (RCLike.ofRealCLM (K := ℂ)) (imLp f), ContinuousLinearMap.coeFn_compLpL (RCLike.reCLM (K := ℂ)) f, ContinuousLinearMap.coeFn_compLpL (RCLike.imCLM (K := ℂ)) f] with ω h_add h_smul h_re_embed h_im_embed h_re h_im rw [h_add] simp only [Pi.add_apply] rw [h_smul] simp only [Pi.smul_apply] rw [show (((ιLp (reLp f) : Lp ℂ 2 μ) : Ω → ℂ) ω) = (RCLike.ofRealCLM (K := ℂ)) (((reLp f : Lp ℝ 2 μ) : Ω → ℝ) ω) by simpa [ιLp] using h_re_embed] rw [show (((ιLp (imLp f) : Lp ℂ 2 μ) : Ω → ℂ) ω) = (RCLike.ofRealCLM (K := ℂ)) (((imLp f : Lp ℝ 2 μ) : Ω → ℝ) ω) by simpa [ιLp] using h_im_embed] rw [show (((reLp f : Lp ℝ 2 μ) : Ω → ℝ) ω) = (RCLike.reCLM (K := ℂ)) (((f : Lp ℂ 2 μ) : Ω → ℂ) ω) by simpa [reLp] using h_re] rw [show (((imLp f : Lp ℝ 2 μ) : Ω → ℝ) ω) = (RCLike.imCLM (K := ℂ)) (((f : Lp ℂ 2 μ) : Ω → ℂ) ω) by simpa [imLp] using h_im] change (RCLike.re (((f : Lp ℂ 2 μ) : Ω → ℂ) ω) : ℂ) + Complex.I * (RCLike.im (((f : Lp ℂ 2 μ) : Ω → ℂ) ω) : ℂ) = (((f : Lp ℂ 2 μ) : Ω → ℂ) ω) rw [mul_comm] exact RCLike.re_add_im (((f : Lp ℂ 2 μ) : Ω → ℂ) ω) -
complexLift_applytheorem — The action equation for complexLift: it agrees with complexLiftFun A on every input.hypothesesconclusionProof (Lean source)
theorem complexLift_apply (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (f : Lp ℂ 2 μ) : complexLift A f = ιLp (A (reLp f)) + (Complex.I : ℂ) • ιLp (A (imLp f)) := by rfl -
complexLift_realtheorem — Restriction of the complex lift to the real subspace recovers A. reLp_comp_ιLp gives reLp (ιLp g) = g and imLp_comp_ιLp gives imLp (ιLp g) = 0, so complexLift_apply collapses to ιLp (A g) + I • ιLp (A 0) = ιLp (A g).hypothesesconclusionProof (Lean source)
theorem complexLift_real (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (g : Lp ℝ 2 μ) : complexLift A (ιLp g) = ιLp (A g) := by rw [complexLift_apply, reLp_comp_ιLp, imLp_comp_ιLp] simp -
reLp_complexLift_realtheorem — Corollary of complexLift_real: projecting back via reLp gives exactly A g. Direct from reLp_comp_ιLp.hypothesesconclusionProof (Lean source)
theorem reLp_complexLift_real (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (g : Lp ℝ 2 μ) : reLp (complexLift A (ιLp g)) = A g := by rw [complexLift_real, reLp_comp_ιLp] -
complexLift_adjointtheorem — The complex lift commutes with taking adjoints.hypothesesconclusion(complexLift A).adjoint = complexLift A.adjointProof (Lean source)
theorem complexLift_adjoint (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) : (complexLift A).adjoint = complexLift A.adjoint := by ext f rw [← reLp_add_smul_imLp f] rw [map_add, map_smul] rw [complexLift_adjoint_apply_real, complexLift_adjoint_apply_real] rw [complexLift_apply] simp [map_add, reLp_comp_ιLp, imLp_comp_ιLp, reLp_I_smul, imLp_I_smul] -
complexLift_isSelfAdjointtheorem — Self-adjointness is preserved by the complex lift. Direct corollary of complexLift_adjoint (rewrite A.adjoint = A inside the RHS).hypothesesconclusionProof (Lean source)
theorem complexLift_isSelfAdjoint {A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ} (hA : IsSelfAdjoint A) : IsSelfAdjoint (complexLift A) := by rw [ContinuousLinearMap.isSelfAdjoint_iff'] rw [complexLift_adjoint, hA.adjoint_eq] -
realCFC_applytheorem — Action equation for realCFC — the basic rewrite rule used by spectral proofs.Proof (Lean source)
theorem realCFC_apply (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hA : IsSelfAdjoint A) (f : ℝ → ℝ) (hf : Continuous f) (g : Lp ℝ 2 μ) : realCFC A f g = reLp (cfc (fun z : ℂ => (f z.re : ℂ)) (complexLift A) (ιLp g)) := by have _hA : IsSelfAdjoint A := hA have _hf : Continuous f := hf rfl -
realCFC_idtheorem — realCFC of the identity symbol recovers A.hypothesesconclusionrealCFC A id g = A gProof (Lean source)
theorem realCFC_id (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hA : IsSelfAdjoint A) (g : Lp ℝ 2 μ) : realCFC A id g = A g := by rw [realCFC_apply A hA id continuous_id g] have hcl : IsSelfAdjoint (complexLift A) := complexLift_isSelfAdjoint hA rw [← cfc_real_eq_complex (a := complexLift A) (f := id) (ha := hcl)] rw [cfc_id ℝ (complexLift A) hcl] exact reLp_complexLift_real A g -
realCFC_isSelfAdjointtheorem — realCFC preserves self-adjointness.Proof (Lean source)
theorem realCFC_isSelfAdjoint (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hA : IsSelfAdjoint A) (f : ℝ → ℝ) (hf : Continuous f) : IsSelfAdjoint (realCFC A f) := by let C : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ := cfc (fun z : ℂ => (f z.re : ℂ)) (complexLift A) have hC : IsSelfAdjoint C := by have hcl : IsSelfAdjoint (complexLift A) := complexLift_isSelfAdjoint hA rw [show C = cfc (fun z : ℂ => (f z.re : ℂ)) (complexLift A) by rfl] rw [← cfc_real_eq_complex (a := complexLift A) (f := f) (ha := hcl)] exact IsSelfAdjoint.cfc rw [ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric] intro x y change inner ℝ (realCFC A f x) y = inner ℝ x (realCFC A f y) rw [realCFC_apply A hA f hf x, realCFC_apply A hA f hf y] rw [inner_reLp_left (C (ιLp x)) y] change (inner ℂ (C (ιLp x)) (ιLp y)).re = inner ℝ x (reLp (C (ιLp y))) rw [real_inner_comm (reLp (C (ιLp y))) x] rw [inner_reLp_left (C (ιLp y)) x] calc (inner ℂ (C (ιLp x)) (ιLp y)).re = (inner ℂ (ιLp x) (C (ιLp y))).re := by exact congrArg re ((ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mp hC) (ιLp x) (ιLp y)) _ = (inner ℂ (C (ιLp y)) (ιLp x)).re := by simpa using (inner_re_symm (𝕜 := ℂ) (x := C (ιLp y)) (y := ιLp x)).symm -
realCFC_multheorem — Symbol-multiplication law for realCFC.hypotheseshA :f g :ℝ → ℝhf :hg :Proof (Lean source)
theorem realCFC_mul (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hA : IsSelfAdjoint A) (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) : realCFC A (fun x => f x * g x) = (realCFC A f).comp (realCFC A g) := by ext v rw [realCFC_apply A hA (fun x => f x * g x) (hf.mul hg) v] rw [ContinuousLinearMap.comp_apply] rw [realCFC_apply A hA f hf (realCFC A g v), realCFC_apply A hA g hg v] rw [cfc_lifted_preserves_real A hA g hg v] rw [show (fun z : ℂ => ((f z.re * g z.re : ℝ) : ℂ)) = fun z : ℂ => (f z.re : ℂ) * (g z.re : ℂ) by funext z norm_num] rw [cfc_mul (fun z : ℂ => (f z.re : ℂ)) (fun z : ℂ => (g z.re : ℂ)) (complexLift A) (hf := (Complex.continuous_ofReal.comp (hf.comp Complex.continuous_re)).continuousOn) (hg := (Complex.continuous_ofReal.comp (hg.comp Complex.continuous_re)).continuousOn)] rfl
Tikhonov 6 core · 6 supporting Develops the Hilbert-space Tikhonov interface for NPIV inverse problems. ★ tikhonovMinimiserL2_optimality★ tikhonovMinimiserL2_strong_convexity
Develops the Hilbert-space Tikhonov interface for NPIV inverse problems.
The module defines OperatorSystem.tikhonovBilin,
OperatorSystem.tikhonovTargetSub, and
OperatorSystem.tikhonovMinimiserL2; proves coercivity and the minimizer's
variational identity; and exposes
OperatorSystem.tikhonovMinimiserL2_strong_convexity, the L²-level population
strong-convexity inequality used by the primal rate theorem.
def tikhonovBilin reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system and a real regularization level, the ambient Tikhonov bilinear form sends two random variables to .
Definition (Lean source)
def tikhonovBilinSub reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system and a real regularization level, the restricted Tikhonov bilinear form is the ambient Tikhonov bilinear form evaluated on two elements of the closed primal candidate subspace.
Definition (Lean source)
parameters
def
tikhonovBilinSub S lambda :
S.Hbar_L2 →L[ℝ] S.Hbar_L2 →L[ℝ] ℝ
given by
(((S.tikhonovBilin lambda).comp S.Hbar_L2.subtypeL).flip.comp S.Hbar_L2.subtypeL).flip
def tikhonovTargetSub reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the Tikhonov target functional sends each element of the closed primal candidate subspace to the inner product of its transformed image with the transformed structural function.
Definition (Lean source)
def tikhonovMinimiserL2 reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system whose closed primal candidate subspace admits orthogonal projection and a real regularization level, the population Tikhonov minimiser is the unique variational solution in that subspace when , and is the zero element when . It first equips the candidate subspace with its complete Hilbert-space structure; under , it obtains the coercive restricted Tikhonov form, constructs the associated variational equivalence, and maps the target functional to its representing candidate element, whose inverse image is returned as the minimiser; when , it returns zero.
Definition (Lean source)
parameters
def
given by
complete :
hbarL2_completeSpace S (: CompleteSpace S.Hbar_L2)
if h : 0 < lambda then let coercive := tikhonovBilinSub_isCoercive S h let Bsharp := @IsCoercive.continuousLinearEquivOfBilin S.Hbar_L2 _ _ complete (S.tikhonovBilinSub lambda) coercive let w : S.Hbar_L2 := (@InnerProductSpace.toDual ℝ S.Hbar_L2 _ _ _ complete).symm (S.tikhonovTargetSub) ↑(Bsharp.symm w : S.Hbar_L2) else 0
lemma tikhonovMinimiserL2_optimality reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
Variational identity for the Tikhonov minimiser. For a strictly positive Tikhonov regularization level λ and any function v in the closed primal candidate subspace Hbar_L2, the population Tikhonov minimiser h*_λ at level λ satisfies the identity ⟪T h*_λ, T v⟫ + λ · ⟪h*_λ, v⟫ = ⟪T h₀, T v⟫, where T is the projection-composed conditional-expectation operator and h₀ is the L² class of the structural function.
Formal statement
hypotheses
S :
OperatorSystem Ω μ
S.Hbar_L2.HasOrthogonalProjection
lambda :
ℝ
lambda_pos :
0 < lambda
v :
Lp ℝ 2 μ
hv :
v ∈ S.Hbar_L2
Proof (Lean source)
lemma tikhonovMinimiserL2_optimality
(S : OperatorSystem Ω μ) [S.Hbar_L2.HasOrthogonalProjection]
{lambda : ℝ} (lambda_pos : 0 < lambda)
{v : Lp ℝ 2 μ} (hv : v ∈ S.Hbar_L2) :
inner ℝ (S.Tlin (S.tikhonovMinimiserL2 lambda)) (S.Tlin v)
+ lambda * inner ℝ (S.tikhonovMinimiserL2 lambda) v
= inner ℝ (S.Tlin (S.hL2 S.h₀_mem)) (S.Tlin v) := by
let complete : CompleteSpace S.Hbar_L2 := hbarL2_completeSpace S
let coercive := tikhonovBilinSub_isCoercive S lambda_pos
let Bsharp :=
@IsCoercive.continuousLinearEquivOfBilin S.Hbar_L2 _ _ complete
(S.tikhonovBilinSub lambda) coercive
let w : S.Hbar_L2 :=
(@InnerProductSpace.toDual ℝ S.Hbar_L2 _ _ _ complete).symm (S.tikhonovTargetSub)
let ustar : S.Hbar_L2 := Bsharp.symm w
let vsub : S.Hbar_L2 := ⟨v, hv⟩
have hmin : S.tikhonovMinimiserL2 lambda = (ustar : Lp ℝ 2 μ) := by
simp [tikhonovMinimiserL2, lambda_pos, Bsharp, w, ustar]
have hLM :=
@IsCoercive.continuousLinearEquivOfBilin_apply S.Hbar_L2 _ _ complete
(S.tikhonovBilinSub lambda) coercive ustar vsub
have htarget : inner ℝ w vsub = S.tikhonovTargetSub vsub := by
change inner ℝ ((@InnerProductSpace.toDual ℝ S.Hbar_L2 _ _ _ complete).symm
S.tikhonovTargetSub) vsub = S.tikhonovTargetSub vsub
exact @InnerProductSpace.toDual_symm_apply ℝ S.Hbar_L2 _ _ _ complete
(x := vsub) (y := S.tikhonovTargetSub)
have hvar : S.tikhonovBilinSub lambda ustar vsub = S.tikhonovTargetSub vsub := by
calc
S.tikhonovBilinSub lambda ustar vsub = inner ℝ (Bsharp ustar) vsub :=
hLM.symm
_ = inner ℝ w vsub := by simp [ustar]
_ = S.tikhonovTargetSub vsub := htarget
rw [hmin]
simpa [vsub, tikhonovBilinSub_apply, tikhonovBilin_apply, tikhonovTargetSub_apply] using hvar
lemma tikhonovMinimiserL2_strong_convexity reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
Population strong convexity at the Tikhonov minimiser (L² level). For a strictly positive Tikhonov regularization level λ and any function h in the closed primal candidate subspace Hbar_L2, the non-negative excess λ‖h − h*_λ‖² + ‖T(h − h*_λ)‖² — the amount by which the quadratic Tikhonov objective at h exceeds its value at the population minimiser h*_λ — is bounded above by ‖T(h − h₀)‖² − ‖T(h*_λ − h₀)‖² + λ(‖h‖² − ‖h*_λ‖²), where T is the projection-composed conditional-expectation operator and h₀ is the structural function's L² class.
Formal statement
hypotheses
S :
OperatorSystem Ω μ
S.Hbar_L2.HasOrthogonalProjection
lambda :
ℝ
lambda_pos :
0 < lambda
h :
Lp ℝ 2 μ
hh :
h ∈ S.Hbar_L2
conclusion
lambda * ‖h - S.tikhonovMinimiserL2 lambda‖ ^ 2
+ ‖S.Tlin (h - S.tikhonovMinimiserL2 lambda)‖ ^ 2
≤ ‖S.Tlin (h - S.hL2 S.h₀_mem)‖ ^ 2
- ‖S.Tlin (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem)‖ ^ 2
+ lambda * (‖h‖ ^ 2 - ‖S.tikhonovMinimiserL2 lambda‖ ^ 2)
Proof (Lean source)
lemma tikhonovMinimiserL2_strong_convexity
(S : OperatorSystem Ω μ) [S.Hbar_L2.HasOrthogonalProjection]
{lambda : ℝ} (lambda_pos : 0 < lambda)
{h : Lp ℝ 2 μ} (hh : h ∈ S.Hbar_L2) :
lambda * ‖h - S.tikhonovMinimiserL2 lambda‖ ^ 2
+ ‖S.Tlin (h - S.tikhonovMinimiserL2 lambda)‖ ^ 2
≤ ‖S.Tlin (h - S.hL2 S.h₀_mem)‖ ^ 2
- ‖S.Tlin (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem)‖ ^ 2
+ lambda * (‖h‖ ^ 2 - ‖S.tikhonovMinimiserL2 lambda‖ ^ 2) := by
let hstar := S.tikhonovMinimiserL2 lambda
have hstar_mem : hstar ∈ S.Hbar_L2 := S.tikhonovMinimiserL2_mem lambda
have hdiff : h - hstar ∈ S.Hbar_L2 := S.Hbar_L2.sub_mem hh hstar_mem
have hopt := S.tikhonovMinimiserL2_optimality lambda_pos (v := h - hstar) hdiff
apply le_of_eq
simp [hstar, norm_sub_sq_real, ContinuousLinearMap.map_sub, inner_sub_right,
real_inner_comm] at hopt ⊢
nlinarith [hopt]
6 supporting declarations (lemmas, instances)
-
tikhonovBilin_applylemma — Pointwise formula for tikhonovBilin.hypothesesProof (Lean source)
lemma tikhonovBilin_apply (S : OperatorSystem Ω μ) (lambda : ℝ) (u v : Lp ℝ 2 μ) : S.tikhonovBilin lambda u v = inner ℝ (S.Tlin u) (S.Tlin v) + lambda * inner ℝ u v := by change (((((innerSL ℝ : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ →L[ℝ] ℝ).comp S.Tlin).flip.comp S.Tlin).flip + lambda • (innerSL ℝ : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ →L[ℝ] ℝ)) u v) = inner ℝ (S.Tlin u) (S.Tlin v) + lambda * inner ℝ u v simp [coe_innerSL_apply] -
tikhonovBilin_symmlemma — Symmetry of tikhonovBilin.hypothesesconclusionS.tikhonovBilin lambda u v = S.tikhonovBilin lambda v uProof (Lean source)
lemma tikhonovBilin_symm (S : OperatorSystem Ω μ) (lambda : ℝ) (u v : Lp ℝ 2 μ) : S.tikhonovBilin lambda u v = S.tikhonovBilin lambda v u := by simp [tikhonovBilin_apply, real_inner_comm] -
tikhonovBilinSub_applylemma — Pointwise formula for the restricted bilinear form.hypothesesProof (Lean source)
lemma tikhonovBilinSub_apply (S : OperatorSystem Ω μ) (lambda : ℝ) (u v : S.Hbar_L2) : S.tikhonovBilinSub lambda u v = S.tikhonovBilin lambda (u : Lp ℝ 2 μ) (v : Lp ℝ 2 μ) := by rfl -
tikhonovBilinSub_isCoercivelemma — Coercivity of tikhonovBilinSub for 0 < λ. Witness constant: λ. Proof: bilin u u = ‖T u‖² + λ ‖u‖² ≥ λ ‖u‖² since ‖T u‖² ≥ 0.hypothesesconclusionIsCoercive (S.tikhonovBilinSub lambda)Proof (Lean source)
lemma tikhonovBilinSub_isCoercive (S : OperatorSystem Ω μ) [S.Hbar_L2.HasOrthogonalProjection] {lambda : ℝ} (lambda_pos : 0 < lambda) : IsCoercive (S.tikhonovBilinSub lambda) := by refine ⟨lambda, lambda_pos, ?_⟩ intro u change lambda * ‖u‖ * ‖u‖ ≤ S.tikhonovBilin lambda (u : Lp ℝ 2 μ) (u : Lp ℝ 2 μ) rw [tikhonovBilin_apply] simp nlinarith [sq_nonneg (‖S.Tlin (u : Lp ℝ 2 μ)‖)] -
tikhonovTargetSub_applylemma — Pointwise formula for the target functional.hypothesesProof (Lean source)
lemma tikhonovTargetSub_apply (S : OperatorSystem Ω μ) (v : S.Hbar_L2) : S.tikhonovTargetSub v = inner ℝ (S.Tlin (S.hL2 S.h₀_mem)) (S.Tlin (v : Lp ℝ 2 μ)) := by simp [tikhonovTargetSub, coe_innerSL_apply] -
tikhonovMinimiserL2_memlemma — The minimiser lies in Hbar_L2.hypothesesconclusionS.tikhonovMinimiserL2 lambda ∈ S.Hbar_L2Proof (Lean source)
lemma tikhonovMinimiserL2_mem (S : OperatorSystem Ω μ) [S.Hbar_L2.HasOrthogonalProjection] (lambda : ℝ) : S.tikhonovMinimiserL2 lambda ∈ S.Hbar_L2 := by by_cases h : 0 < lambda · simp [tikhonovMinimiserL2, h] · simp [tikhonovMinimiserL2, h]
SpectralCalculus 10 core · 6 supporting This file proves the Tikhonov bias bounds for the primal NPIV estimator from a spectral β-source condition. ★ tikhonovMinimiserL2_eq_resolvent★ strong_bias★ weak_bias
Spectral Discharge of Tikhonov Bias
This file proves the Tikhonov bias bounds for the primal NPIV estimator from a
spectral β-source condition. It defines the strengthened
SpectralSourceCondition, builds the real functional-calculus operator
spectralPower = (T†T)^{β/2}, identifies the full-space Lax–Milgram
Tikhonov minimizer with its resolvent expression, proves the strong- and
weak-metric bias bounds, and packages them as tikhonov_bias_from_spectral
for the rate theorem.
instance instAlgebraRealLpCLM reviewed
⚑ flagged
Causalean.Estimation.NPIV
For a measurable sample space and its measure, the real-scalar algebra is the algebra of bounded complex-linear operators on the corresponding complex-valued space.
structure SpectralSourceCondition reviewed
⚑ flagged
Causalean.Estimation.NPIV
Spectral β-source condition at the primal nuisance h₀: strengthens SourceCondition by additionally requiring that the primal candidate subspace coincides with the full ambient L² space, which is what lets the Lax–Milgram Tikhonov minimiser on the candidate class agree with the resolvent expression needed to run the spectral argument.
Definition (Lean source)
parameters
fields
The primal candidate subspace is the full L² space.
Hbar_L2_eq_top :
S.Hbar_L2 = ⊤
def sourceSymbol reviewed
⚑ flagged
Causalean.Estimation.NPIV.SpectralSourceCondition
For a real source exponent, the source symbol is the function sending each real number to .
def spectralPower reviewed
⚑ flagged
Causalean.Estimation.NPIV.SpectralSourceCondition
For a spectral source condition, the spectral-power operator is the real functional-calculus transform of the adjoint-product NPIV operator by the symbol .
Definition (Lean source)
parameters
given by
Complexification.realCFC S.Tstar_T (sourceSymbol β)
def biasConst reviewed
⚑ flagged
Causalean.Estimation.NPIV.SpectralSourceCondition
For a spectral source condition, the bias constant is .
Definition (Lean source)
parameters
def
biasConst _sc :
ℝ
theorem tikhonovMinimiserL2_eq_resolvent reviewed
⚑ flagged
Causalean.Estimation.NPIV.SpectralSourceCondition
Resolvent identification of the Lax–Milgram minimiser. Given a spectral β-source condition sc whose primal candidate set coincides with the whole ambient L² space, for any strictly positive Tikhonov regularization level λ, the population Tikhonov minimiser at level λ equals the resolvent expression obtained by applying the real functional calculus of T†T to the symbol x ↦ x/(λ+x), evaluated at the L² class of the structural function h₀.
Formal statement
hypotheses
β :
ℝ
sc :
lambda :
ℝ
lambda_pos :
0 < lambda
conclusion
haveI
Proof (Lean source)
theorem tikhonovMinimiserL2_eq_resolvent
(sc : SpectralSourceCondition S β) {lambda : ℝ} (lambda_pos : 0 < lambda) :
haveI := sc.Hbar_L2_hasProj
S.tikhonovMinimiserL2 lambda
= Complexification.realCFC S.Tstar_T
(fun x => x / (lambda + x)) (S.hL2 S.h₀_mem) := by
haveI := sc.Hbar_L2_hasProj
set A := S.Tstar_T with hA_def
set R : Lp ℝ 2 μ :=
Complexification.realCFC A (fun x => x / (lambda + x)) (S.hL2 S.h₀_mem)
set h_star : Lp ℝ 2 μ := S.tikhonovMinimiserL2 lambda
have hvar : ∀ v : Lp ℝ 2 μ,
inner ℝ (S.Tlin h_star) (S.Tlin v) + lambda * inner ℝ h_star v
= inner ℝ (S.Tlin (S.hL2 S.h₀_mem)) (S.Tlin v) := by
intro v
have hv : v ∈ S.Hbar_L2 := by
rw [sc.Hbar_L2_eq_top]
exact Submodule.mem_top
exact S.tikhonovMinimiserL2_optimality lambda_pos hv
have hop_star :
S.Tadjoint (S.Tlin h_star) + lambda • h_star =
S.Tadjoint (S.Tlin (S.hL2 S.h₀_mem)) := by
apply ext_inner_right ℝ
intro v
rw [inner_add_left, inner_smul_left]
rw [OperatorSystem.Tadjoint]
rw [ContinuousLinearMap.adjoint_inner_left, ContinuousLinearMap.adjoint_inner_left]
simpa using hvar v
have hop_star' :
A h_star + lambda • h_star = A (S.hL2 S.h₀_mem) := by
simpa [hA_def, OperatorSystem.Tstar_T, ContinuousLinearMap.comp_apply] using hop_star
have hA_sa : IsSelfAdjoint A := by
simpa [hA_def] using S.Tstar_T_isSelfAdjoint
have hres :
(algebraMap ℝ (Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) lambda + A) R =
A (S.hL2 S.h₀_mem) := by
have h := resolvent_left_inverse A hA_sa (by
intro x hx
exact sc.Tstar_T_spectrum_nonneg x (by simpa [hA_def] using hx)) lambda_pos
have happ :=
congrArg (fun T : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ => T (S.hL2 S.h₀_mem)) h
simpa [R] using happ
have hop_R : A R + lambda • R = A (S.hL2 S.h₀_mem) := by
simpa [ContinuousLinearMap.add_apply, Algebra.algebraMap_eq_smul_one,
ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply, add_comm] using hres
have hdiff : A (h_star - R) + lambda • (h_star - R) = 0 := by
have heq : A h_star + lambda • h_star = A R + lambda • R :=
hop_star'.trans hop_R.symm
calc
A (h_star - R) + lambda • (h_star - R)
= (A h_star + lambda • h_star) - (A R + lambda • R) := by
simp [sub_eq_add_neg, add_assoc, add_left_comm, add_comm]
_ = 0 := by rw [heq]; simp
have hpos_self :
inner ℝ (A (h_star - R)) (h_star - R) = ‖S.Tlin (h_star - R)‖ ^ 2 := by
subst A
change inner ℝ (S.Tadjoint (S.Tlin (h_star - R))) (h_star - R) = _
rw [OperatorSystem.Tadjoint, ContinuousLinearMap.adjoint_inner_left]
exact real_inner_self_eq_norm_sq _
have hzero :
‖S.Tlin (h_star - R)‖ ^ 2 + lambda * ‖h_star - R‖ ^ 2 = 0 := by
have hpair := congrArg (fun u => inner ℝ u (h_star - R)) hdiff
simp only [inner_zero_left, inner_add_left, inner_smul_left] at hpair
have hnorm_sq : inner ℝ (h_star - R) (h_star - R) = ‖h_star - R‖ ^ 2 :=
real_inner_self_eq_norm_sq _
rw [hpos_self, hnorm_sq] at hpair
simpa using hpair
have hsq_zero : ‖h_star - R‖ ^ 2 = 0 := by
have hT_nn : 0 ≤ ‖S.Tlin (h_star - R)‖ ^ 2 := sq_nonneg _
have hw_nn : 0 ≤ ‖h_star - R‖ := norm_nonneg _
nlinarith [hzero, hT_nn, lambda_pos, hw_nn]
have hnorm_zero : ‖h_star - R‖ = 0 := by
exact sq_eq_zero_iff.mp hsq_zero
have hsub_zero : h_star - R = 0 := norm_eq_zero.mp hnorm_zero
simpa [h_star, R, hA_def] using sub_eq_zero.mp hsub_zero
theorem strong_bias reviewed
⚑ flagged
Causalean.Estimation.NPIV.SpectralSourceCondition
Strong-metric Tikhonov bias bound. Given a spectral β-source condition sc linking the structural function h₀ to a coefficient w₀ through the spectral power operator (T†T)^{β/2}, for any strictly positive Tikhonov regularization level λ, the squared strong-metric () distance between the Tikhonov minimiser h*_λ at level λ and h₀ is bounded by biasConst · ‖w₀‖² · λ^{min(β,2)}, where biasConst is a constant determined by T†T and β.
Formal statement
hypotheses
β :
ℝ
sc :
lambda :
ℝ
lambda_pos :
0 < lambda
conclusion
haveI
Proof (Lean source)
theorem strong_bias (sc : SpectralSourceCondition S β)
{lambda : ℝ} (lambda_pos : 0 < lambda) :
haveI := sc.Hbar_L2_hasProj
‖S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem‖ ^ 2
≤ sc.biasConst * ‖S.hL2 sc.w₀_mem‖ ^ 2 * lambda ^ (min β 2) := by
haveI := sc.Hbar_L2_hasProj
by_cases hnt : Nontrivial (Lp ℝ 2 μ)
swap
· haveI : Subsingleton (Lp ℝ 2 μ) := not_nontrivial_iff_subsingleton.mp hnt
have hdiff : S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem = 0 := Subsingleton.elim _ _
have hpow_nonneg : 0 ≤ lambda ^ (min β 2) := Real.rpow_nonneg (le_of_lt lambda_pos) _
have hrhs_nonneg :
0 ≤ sc.biasConst * ‖S.hL2 sc.w₀_mem‖ ^ 2 * lambda ^ (min β 2) :=
mul_nonneg (mul_nonneg sc.biasConst_nonneg (sq_nonneg _)) hpow_nonneg
simpa [hdiff] using hrhs_nonneg
haveI : Nontrivial (Lp ℝ 2 μ) := hnt
haveI : NormOneClass (Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) := ContinuousLinearMap.normOneClass
set A := S.Tstar_T with hA_def
set w := S.hL2 sc.w₀_mem with hw_def
set B : ℝ := max 1 (‖A‖ + 1) with hB_def
set c : ℝ := B ^ (β / 2) * lambda ^ (min β 2 / 2) with hc_def
have hA_sa : IsSelfAdjoint A := by simpa [hA_def] using S.Tstar_T_isSelfAdjoint
have hβ : 0 ≤ β := sc.beta_nonneg
have hB_ge_one : 1 ≤ B := by
rw [hB_def]
exact le_max_left _ _
have hB_pos : 0 < B := lt_of_lt_of_le zero_lt_one hB_ge_one
have hc_nonneg : 0 ≤ c := by
rw [hc_def]
exact mul_nonneg (Real.rpow_nonneg (le_of_lt hB_pos) _)
(Real.rpow_nonneg (le_of_lt lambda_pos) _)
have hden : ∀ x : ℝ, lambda + max 0 x ≠ 0 := fun x => by
have hmax : (0 : ℝ) ≤ max 0 x := le_max_left _ _
have hpos : 0 < lambda + max 0 x := by linarith
exact ne_of_gt hpos
let rSafe : ℝ → ℝ := fun x => x / (lambda + max 0 x)
let prod : ℝ → ℝ := fun x => rSafe x * sourceSymbol β x
have hr_cont : Continuous rSafe := by
dsimp [rSafe]
exact continuous_id.div (continuous_const.add (continuous_const.max continuous_id)) hden
have hsrc_cont : Continuous (sourceSymbol β) := continuous_sourceSymbol hβ
have hsource_eq : (fun x : ℝ => rpow (max x 0) (β / 2)) = sourceSymbol β := rfl
have hres_safe : Complexification.realCFC A (fun x => x / (lambda + x)) =
Complexification.realCFC A rSafe := by
apply realCFC_congr_on_spectrum_local A
· intro x hx
have hx0 : 0 ≤ x := sc.Tstar_T_spectrum_nonneg x (by simpa [hA_def] using hx)
dsimp [rSafe]
rw [max_eq_right hx0]
· exact hA_sa
have hmul : Complexification.realCFC A prod =
(Complexification.realCFC A rSafe).comp
(Complexification.realCFC A (sourceSymbol β)) := by
dsimp [prod]
exact Complexification.realCFC_mul A hA_sa rSafe (sourceSymbol β) hr_cont hsrc_cont
have hsub_cfc : Complexification.realCFC A (fun x => prod x - sourceSymbol β x) =
Complexification.realCFC A prod - Complexification.realCFC A (sourceSymbol β) :=
realCFC_sub_local A hA_sa prod (sourceSymbol β) (hr_cont.mul hsrc_cont) hsrc_cont
have hsymbol : Complexification.realCFC A (fun x => prod x - sourceSymbol β x) =
Complexification.realCFC A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) := by
apply realCFC_congr_on_spectrum_local A
· intro x hx
have hx0 : 0 ≤ x := sc.Tstar_T_spectrum_nonneg x (by simpa [hA_def] using hx)
have hne : lambda + max 0 x ≠ 0 := hden x
dsimp [prod, rSafe]
rw [max_eq_right hx0]
field_simp [hne]
ring
· exact hA_sa
have hresid :
S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem =
Complexification.realCFC A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) w := by
calc
S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem
= (Complexification.realCFC A rSafe)
((Complexification.realCFC A (sourceSymbol β)) w) -
(Complexification.realCFC A (sourceSymbol β)) w := by
rw [tikhonovMinimiserL2_eq_resolvent (S := S) (β := β) sc lambda_pos]
rw [sc.spectral_identity]
rw [hsource_eq]
rw [hres_safe]
_ = ((Complexification.realCFC A rSafe).comp
(Complexification.realCFC A (sourceSymbol β))) w -
(Complexification.realCFC A (sourceSymbol β)) w := by rfl
_ = (Complexification.realCFC A prod -
Complexification.realCFC A (sourceSymbol β)) w := by
rw [← hmul]
simp only [ContinuousLinearMap.sub_apply]
_ = Complexification.realCFC A (fun x => prod x - sourceSymbol β x) w := by
rw [hsub_cfc]
_ = Complexification.realCFC A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) w := by
rw [hsymbol]
have hsafe_cont :
Continuous (fun x : ℝ => -lambda * sourceSymbol β x / (lambda + max 0 x)) :=
(continuous_const.mul hsrc_cont).div
(continuous_const.add (continuous_const.max continuous_id)) hden
have hsup : ∀ x ∈ spectrum ℝ A,
|(-lambda * sourceSymbol β x / (lambda + max 0 x))| ≤ c := by
intro x hx
have hx0 : 0 ≤ x := sc.Tstar_T_spectrum_nonneg x (by simpa [hA_def] using hx)
rw [hc_def]
by_cases hβ2 : β ≤ 2
· exact residual_symbol_bound_small lambda_pos hx0 hβ hβ2 hB_ge_one
· have hxnorm : ‖x‖ ≤ ‖A‖ := spectrum.norm_le_norm_of_mem hx
have hx_le_norm : x ≤ ‖A‖ := by
rw [Real.norm_eq_abs, abs_of_nonneg hx0] at hxnorm
exact hxnorm
have hnorm_le_B : ‖A‖ ≤ B := by
calc
‖A‖ ≤ ‖A‖ + 1 := by linarith [norm_nonneg A]
_ ≤ max 1 (‖A‖ + 1) := le_max_right _ _
_ = B := by rw [hB_def]
have hxB : x ≤ B := le_trans hx_le_norm hnorm_le_B
exact residual_symbol_bound_large lambda_pos hx0 hxB (lt_of_not_ge hβ2) hB_ge_one
have hnorm :=
Complexification.realCFC_norm_le A hA_sa
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) hsafe_cont
c hc_nonneg hsup w
have hsq :
‖Complexification.realCFC A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) w‖ ^ 2
≤ (c * ‖w‖) ^ 2 :=
sq_le_sq' (by
have hmul_nonneg : 0 ≤ c * ‖w‖ := mul_nonneg hc_nonneg (norm_nonneg _)
nlinarith [norm_nonneg
(Complexification.realCFC A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) w), hmul_nonneg]) hnorm
have hcoef : (c * ‖w‖) ^ 2 =
sc.biasConst * ‖w‖ ^ 2 * lambda ^ (min β 2) := by
rw [hc_def, mul_pow, mul_pow]
rw [show (B ^ (β / 2)) ^ (2 : ℕ) = B ^ β by
rw [sq, ← Real.rpow_add hB_pos]
congr 1
ring]
rw [show (lambda ^ (min β 2 / 2)) ^ (2 : ℕ) = lambda ^ (min β 2) by
rw [sq, ← Real.rpow_add lambda_pos]
congr 1
ring]
rw [biasConst]
simp [hB_def, hA_def]
ring
calc
‖S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem‖ ^ 2
= ‖Complexification.realCFC A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) w‖ ^ 2 := by
rw [hresid]
_ ≤ (c * ‖w‖) ^ 2 := hsq
_ = sc.biasConst * ‖S.hL2 sc.w₀_mem‖ ^ 2 * lambda ^ (min β 2) := by
rw [hcoef, hw_def]
theorem weak_bias reviewed
⚑ flagged
Causalean.Estimation.NPIV.SpectralSourceCondition
Weak-metric Tikhonov bias bound. Given the same spectral β-source condition sc linking h₀ to w₀ through (T†T)^{β/2}, for any strictly positive Tikhonov regularization level λ, the squared weak-metric () norm of the operator T applied to the Tikhonov-minimiser bias h*_λ − h₀ is bounded by biasConst · ‖w₀‖² · λ^{min(β+1,2)}.
Formal statement
hypotheses
β :
ℝ
sc :
lambda :
ℝ
lambda_pos :
0 < lambda
conclusion
haveI
Proof (Lean source)
theorem weak_bias (sc : SpectralSourceCondition S β)
{lambda : ℝ} (lambda_pos : 0 < lambda) :
haveI := sc.Hbar_L2_hasProj
‖S.Tlin (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem)‖ ^ 2
≤ sc.biasConst * ‖S.hL2 sc.w₀_mem‖ ^ 2 * lambda ^ (min (β + 1) 2) := by
haveI := sc.Hbar_L2_hasProj
by_cases hnt : Nontrivial (Lp ℝ 2 μ)
swap
· haveI : Subsingleton (Lp ℝ 2 μ) := not_nontrivial_iff_subsingleton.mp hnt
have hdiff : S.Tlin (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem) = 0 :=
Subsingleton.elim _ _
have hpow_nonneg : 0 ≤ lambda ^ (min (β + 1) 2) :=
Real.rpow_nonneg (le_of_lt lambda_pos) _
have hrhs_nonneg :
0 ≤ sc.biasConst * ‖S.hL2 sc.w₀_mem‖ ^ 2 * lambda ^ (min (β + 1) 2) :=
mul_nonneg (mul_nonneg sc.biasConst_nonneg (sq_nonneg _)) hpow_nonneg
simpa [hdiff] using hrhs_nonneg
haveI : Nontrivial (Lp ℝ 2 μ) := hnt
haveI : NormOneClass (Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) := ContinuousLinearMap.normOneClass
set A := S.Tstar_T with hA_def
set w := S.hL2 sc.w₀_mem with hw_def
set B : ℝ := max 1 (‖A‖ + 1) with hB_def
set f : ℝ → ℝ := fun x => -lambda * sourceSymbol β x / (lambda + max 0 x) with hf_def
set q : ℝ → ℝ := fun x => x * f x with hq_def
set g : ℝ → ℝ := fun x => x * f x ^ 2 with hg_def
set c : ℝ := sc.biasConst * lambda ^ (min (β + 1) 2) with hc_def
have hA_sa : IsSelfAdjoint A := by simpa [hA_def] using S.Tstar_T_isSelfAdjoint
have hβ : 0 ≤ β := sc.beta_nonneg
have hB_ge_one : 1 ≤ B := by
rw [hB_def]
exact le_max_left _ _
have hB_pos : 0 < B := lt_of_lt_of_le zero_lt_one hB_ge_one
have hden : ∀ x : ℝ, lambda + max 0 x ≠ 0 := fun x => by
have hmax : (0 : ℝ) ≤ max 0 x := le_max_left _ _
have hpos : 0 < lambda + max 0 x := by linarith
exact ne_of_gt hpos
let rSafe : ℝ → ℝ := fun x => x / (lambda + max 0 x)
let prod : ℝ → ℝ := fun x => rSafe x * sourceSymbol β x
have hr_cont : Continuous rSafe := by
dsimp [rSafe]
exact continuous_id.div (continuous_const.add (continuous_const.max continuous_id)) hden
have hsrc_cont : Continuous (sourceSymbol β) := continuous_sourceSymbol hβ
have hf_cont : Continuous f := by
rw [hf_def]
exact (continuous_const.mul hsrc_cont).div
(continuous_const.add (continuous_const.max continuous_id)) hden
have hq_cont : Continuous q := by
rw [hq_def]
exact continuous_id.mul hf_cont
have hg_cont : Continuous g := by
rw [hg_def]
exact continuous_id.mul (hf_cont.pow 2)
have hsource_eq : (fun x : ℝ => rpow (max x 0) (β / 2)) = sourceSymbol β := rfl
have hres_safe : Complexification.realCFC A (fun x => x / (lambda + x)) =
Complexification.realCFC A rSafe := by
apply realCFC_congr_on_spectrum_local A
· intro x hx
have hx0 : 0 ≤ x := sc.Tstar_T_spectrum_nonneg x (by simpa [hA_def] using hx)
dsimp [rSafe]
rw [max_eq_right hx0]
· exact hA_sa
have hmul : Complexification.realCFC A prod =
(Complexification.realCFC A rSafe).comp
(Complexification.realCFC A (sourceSymbol β)) := by
dsimp [prod]
exact Complexification.realCFC_mul A hA_sa rSafe (sourceSymbol β) hr_cont hsrc_cont
have hsub_cfc : Complexification.realCFC A (fun x => prod x - sourceSymbol β x) =
Complexification.realCFC A prod - Complexification.realCFC A (sourceSymbol β) :=
realCFC_sub_local A hA_sa prod (sourceSymbol β) (hr_cont.mul hsrc_cont) hsrc_cont
have hsymbol : Complexification.realCFC A (fun x => prod x - sourceSymbol β x) =
Complexification.realCFC A f := by
rw [hf_def]
apply realCFC_congr_on_spectrum_local A
· intro x hx
have hx0 : 0 ≤ x := sc.Tstar_T_spectrum_nonneg x (by simpa [hA_def] using hx)
have hne : lambda + max 0 x ≠ 0 := hden x
dsimp [prod, rSafe]
rw [max_eq_right hx0]
field_simp [hne]
ring
· exact hA_sa
have hresid :
S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem =
Complexification.realCFC A f w := by
calc
S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem
= (Complexification.realCFC A rSafe)
((Complexification.realCFC A (sourceSymbol β)) w) -
(Complexification.realCFC A (sourceSymbol β)) w := by
rw [tikhonovMinimiserL2_eq_resolvent (S := S) (β := β) sc lambda_pos]
rw [sc.spectral_identity]
rw [hsource_eq]
rw [hres_safe]
_ = ((Complexification.realCFC A rSafe).comp
(Complexification.realCFC A (sourceSymbol β))) w -
(Complexification.realCFC A (sourceSymbol β)) w := by rfl
_ = (Complexification.realCFC A prod -
Complexification.realCFC A (sourceSymbol β)) w := by
rw [← hmul]
simp only [ContinuousLinearMap.sub_apply]
_ = Complexification.realCFC A (fun x => prod x - sourceSymbol β x) w := by
rw [hsub_cfc]
_ = Complexification.realCFC A f w := by rw [hsymbol]
have hAcomp : A.comp (Complexification.realCFC A f) =
Complexification.realCFC A q := by
rw [hq_def]
rw [show (fun x : ℝ => x * f x) = fun x : ℝ => id x * f x by rfl]
rw [Complexification.realCFC_mul A hA_sa id f continuous_id hf_cont]
apply ContinuousLinearMap.ext
intro v
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply]
rw [Complexification.realCFC_id A hA_sa (Complexification.realCFC A f v)]
have hfg_comp : (Complexification.realCFC A f).comp (Complexification.realCFC A q) =
Complexification.realCFC A g := by
rw [← Complexification.realCFC_mul A hA_sa f q hf_cont hq_cont]
rw [hg_def, hq_def]
congr 1
funext x
ring
have hTu_sq :
‖S.Tlin (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem)‖ ^ 2 =
inner ℝ (Complexification.realCFC A g w) w := by
rw [hresid]
have hTstar :
‖S.Tlin (Complexification.realCFC A f w)‖ ^ 2 =
inner ℝ (A (Complexification.realCFC A f w))
(Complexification.realCFC A f w) := by
rw [← real_inner_self_eq_norm_sq]
subst A
change inner ℝ (S.Tlin (Complexification.realCFC S.Tstar_T f w))
(S.Tlin (Complexification.realCFC S.Tstar_T f w)) =
inner ℝ (S.Tadjoint (S.Tlin (Complexification.realCFC S.Tstar_T f w)))
(Complexification.realCFC S.Tstar_T f w)
rw [OperatorSystem.Tadjoint, ContinuousLinearMap.adjoint_inner_left]
rw [hTstar]
have hAu : A (Complexification.realCFC A f w) =
Complexification.realCFC A q w := by
change (A.comp (Complexification.realCFC A f)) w =
Complexification.realCFC A q w
rw [hAcomp]
rw [hAu]
have hf_sa : IsSelfAdjoint (Complexification.realCFC A f) :=
Complexification.realCFC_isSelfAdjoint A hA_sa f hf_cont
calc
inner ℝ (Complexification.realCFC A q w) (Complexification.realCFC A f w)
= inner ℝ ((Complexification.realCFC A f) (Complexification.realCFC A q w)) w := by
exact ((ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mp hf_sa)
(Complexification.realCFC A q w) w).symm
_ = inner ℝ (((Complexification.realCFC A f).comp
(Complexification.realCFC A q)) w) w := by rfl
_ = inner ℝ (Complexification.realCFC A g w) w := by rw [hfg_comp]
have hsup : ∀ x ∈ spectrum ℝ A, |g x| ≤ c := by
intro x hx
have hx0 : 0 ≤ x := sc.Tstar_T_spectrum_nonneg x (by simpa [hA_def] using hx)
have hxnorm : ‖x‖ ≤ ‖A‖ := spectrum.norm_le_norm_of_mem hx
have hx_le_norm : x ≤ ‖A‖ := by
rw [Real.norm_eq_abs, abs_of_nonneg hx0] at hxnorm
exact hxnorm
have hnorm_le_B : ‖A‖ ≤ B := by
calc
‖A‖ ≤ ‖A‖ + 1 := by linarith [norm_nonneg A]
_ ≤ max 1 (‖A‖ + 1) := le_max_right _ _
_ = B := by rw [hB_def]
have hxB : x ≤ B := le_trans hx_le_norm hnorm_le_B
rw [hc_def, hg_def, hf_def]
have hbound := weak_residual_bound lambda_pos hx0 hxB hβ hB_ge_one
rw [biasConst]
simpa [hA_def, hB_def] using hbound
have hc_nonneg : 0 ≤ c := by
rw [hc_def]
exact mul_nonneg sc.biasConst_nonneg (Real.rpow_nonneg (le_of_lt lambda_pos) _)
have hnorm :=
Complexification.realCFC_norm_le A hA_sa g hg_cont c hc_nonneg hsup w
have hcs : inner ℝ (Complexification.realCFC A g w) w ≤ c * ‖w‖ ^ 2 := by
have hineq : |inner ℝ (Complexification.realCFC A g w) w| ≤
‖Complexification.realCFC A g w‖ * ‖w‖ :=
abs_real_inner_le_norm _ _
calc
inner ℝ (Complexification.realCFC A g w) w
≤ |inner ℝ (Complexification.realCFC A g w) w| := le_abs_self _
_ ≤ ‖Complexification.realCFC A g w‖ * ‖w‖ := hineq
_ ≤ (c * ‖w‖) * ‖w‖ := by
exact mul_le_mul_of_nonneg_right hnorm (norm_nonneg _)
_ = c * ‖w‖ ^ 2 := by ring
calc
‖S.Tlin (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem)‖ ^ 2
= inner ℝ (Complexification.realCFC A g w) w := hTu_sq
_ ≤ c * ‖w‖ ^ 2 := hcs
_ = sc.biasConst * ‖S.hL2 sc.w₀_mem‖ ^ 2 * lambda ^ (min (β + 1) 2) := by
rw [hc_def, hw_def]
ring
structure TikhonovPullback reviewed
⚑ flagged
Causalean.Estimation.NPIV
Function-level pullback datum for the discharge. The user provides a Hbar-element h_lambda_star_fun whose L² class equals the Lax–Milgram minimiser tikhonovMinimiserL2 S λ constructed in Operator/Tikhonov.lean. This single pullback is the only function-level commitment needed: the bias and convexity inequalities all live at the L² level and transport along this equation.
Definition (Lean source)
parameters
fields
Function-level minimiser.
h_lambda_star_fun :
S.𝒳 → ℝ
The function-level minimiser lies in `Hbar`.
h_lambda_star_mem :
h_lambda_star_fun ∈ S.Hbar
Coherence: lifting `h_lambda_star_fun` to `Lp ℝ 2 μ` recovers the
Lax–Milgram L² minimiser.
h_lambda_star_pullback :
haveI := sc.Hbar_L2_hasProj S.hL2 h_lambda_star_mem = S.tikhonovMinimiserL2 lambda
def tikhonov_bias_from_spectral reviewed
⚑ flagged
Causalean.Estimation.NPIV
For an NPIV operator system, a real source exponent, a real regularization level, a strictly positive regularization level, a spectral source condition, and a pullback of the Tikhonov minimiser to a primal candidate function, the construction returns a Tikhonov bias-bound bundle for that system, exponent, level, and the source condition underlying the spectral condition.
Definition (Lean source)
parameters
S :
OperatorSystem Ω μ
β :
ℝ
lambda :
ℝ
lambda_pos :
0 < lambda
sc :
pb :
TikhonovPullback S β lambda sc
def
tikhonov_bias_from_spectral S β lambda lambda_pos sc pb :
TikhonovBiasBound S β lambda sc.toSourceCondition
given by
by haveI := sc.Hbar_L2_hasProj refine { lambda_pos := lambda_pos h_lambda_star_fun := pb.h_lambda_star_fun h_lambda_star_mem := pb.h_lambda_star_mem C := sc.biasConst * ‖S.hL2 sc.w₀_mem‖ C_nonneg := mul_nonneg sc.biasConst_nonneg (norm_nonneg _) strong_bias := ?_ weak_bias := ?_ strong_convexity := ?_ } · have hb := sc.strong_bias lambda_pos have hpull := pb.h_lambda_star_pullback have hC : sc.biasConst * ‖S.hL2 sc.w₀_mem‖ ^ 2 * lambda ^ (min β 2)
= sc.biasConst * ‖S.hL2 sc.w₀_mem‖ * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min β 2) := by rw [OperatorSystem.strongNorm, sq] ring simpa [OperatorSystem.strongNorm, hpull, hC] using hb · have hb := sc.weak_bias lambda_pos have hpull := pb.h_lambda_star_pullback have hC : sc.biasConst * ‖S.hL2 sc.w₀_mem‖ ^ 2 * lambda ^ (min (β + 1) 2) = sc.biasConst * ‖S.hL2 sc.w₀_mem‖ * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min (β + 1) 2) := by rw [OperatorSystem.strongNorm, sq] ring simpa [OperatorSystem.weakNorm, OperatorSystem.strongNorm, OperatorSystem.Tlin_apply, hpull, hC] using hb · intro h hh have hconv := S.tikhonovMinimiserL2_strong_convexity (lambda_pos := lambda_pos) (h := S.hL2 hh) (hh := S.hbar_mem_L2 h hh) simpa [OperatorSystem.strongNorm, OperatorSystem.weakNorm, OperatorSystem.Tlin_apply, pb.h_lambda_star_pullback] using hconv
6 supporting declarations (lemmas, instances)
-
Hbar_L2_hasProjlemma — Closedness witness for the full primal candidate subspace.hypothesesconclusionS.Hbar_L2.HasOrthogonalProjectionProof (Lean source)
lemma Hbar_L2_hasProj (sc : SpectralSourceCondition S β) : S.Hbar_L2.HasOrthogonalProjection := by rw [sc.Hbar_L2_eq_top] infer_instance -
Tstar_T_isPositivelemma — T†T is a positive operator.Proof (Lean source)
lemma Tstar_T_isPositive (S : OperatorSystem Ω μ) : S.Tstar_T.IsPositive := by unfold OperatorSystem.Tstar_T OperatorSystem.Tadjoint simpa [ContinuousLinearMap.comp_def, ContinuousLinearMap.comp_apply] using ContinuousLinearMap.isPositive_adjoint_comp_self S.Tlin -
Tstar_T_spectrum_nonneglemma — Positivity of T†T: its real spectrum lies in [0, ∞).hypothesesβ :sharedℝ_sc :x ∈ spectrum ℝ S.Tstar_T :conclusion0 ≤ xProof (Lean source)
lemma Tstar_T_spectrum_nonneg (_sc : SpectralSourceCondition S β) : ∀ x ∈ spectrum ℝ S.Tstar_T, 0 ≤ x := by intro x hx exact spectrum_nonneg_of_nonneg (a := S.Tstar_T) (x := x) (by rw [ContinuousLinearMap.nonneg_iff_isPositive] exact Tstar_T_isPositive S) hx -
continuous_sourceSymbollemma — The source symbol is continuous whenever the source exponent is nonnegative.Proof (Lean source)
lemma continuous_sourceSymbol {β : ℝ} (h : 0 ≤ β) : Continuous (sourceSymbol β) := by unfold sourceSymbol refine (Real.continuous_rpow_const ?_).comp (continuous_id.max continuous_const) linarith -
spectral_identity_h₀lemma — Restated spectral identity using spectralPower.hypothesesconclusionS.hL2 S.h₀_mem = sc.spectralPower (S.hL2 sc.w₀_mem)Proof (Lean source)
lemma spectral_identity_h₀ (sc : SpectralSourceCondition S β) : S.hL2 S.h₀_mem = sc.spectralPower (S.hL2 sc.w₀_mem) := sc.spectral_identity -
biasConst_nonneglemma — The uniform Tikhonov bias constant is nonnegative.hypothesesconclusion0 ≤ sc.biasConstProof (Lean source)
lemma biasConst_nonneg (sc : SpectralSourceCondition S β) : 0 ≤ sc.biasConst := by unfold biasConst exact Real.rpow_nonneg (le_max_of_le_left zero_le_one) _