Estimation.NPIV.Operator
The NPIV conditional-expectation operator: compactness, singular systems, and the source condition.
Operator 11 core · 9 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 sigma-algebras generated by the covariate X and instrument Z, with the facts that both are coarser than the ambient sigma-algebra on the sample space and coincide with the sigma-algebras pulled back along X and Z, that the ambient probability measure is finite, and candidate submodules of L²(σ(X)) and L²(σ(Z)), with the instrument-side space having 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 primal submodule and the analogous coherence on the instrument side.
Definition (Lean source)
parameters
fields
The σ-algebra generated by `X = xOf ∘ W : Ω → 𝒳`.
m_X :
`m_X` is coarser than `m₀`.
m_X_le :
m_X ≤ m₀
`m_X` is the pullback sigma-algebra generated by `X`.
m_X_eq :
m_X = @comap Ω 𝒳 (fun ω => xOf (W ω)) inst𝒳
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`, as a submodule of `L²(σ(X))`.
Hbar_L2 :
Submodule ℝ (@lpMeas Ω ℝ ℝ _ _ _ m_X m₀ 2 μ)
L² realization of `Qbar`, as a submodule of `L²(σ(Z))`. The
following projection field supplies its closedness.
Qbar_L2 :
Submodule ℝ (@lpMeas Ω ℝ ℝ _ _ _ m_Z m₀ 2 μ)
`Qbar_L2` has 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 submodule
`Hbar_L2`.
hbar_mem_L2 :
∀ h (hh : h ∈ Hbar),
let hLp := (toHbarL2 h hh).toLp _ let hMeas : hLp ∈ @lpMeas Ω ℝ ℝ _ _ _ m_X m₀ 2 μ := by rw [mem_lpMeas_iff_aestronglyMeasurable] exact ((meas_of_Hbar h hh).comp (by rw [m_X_eq]; exact comap_measurable _)).aestronglyMeasurable.congr (toHbarL2 h hh).coeFn_toLp.symm (⟨hLp, hMeas⟩ : @lpMeas Ω ℝ ℝ _ _ _ m_X m₀ 2 μ) ∈ Hbar_L2
Coherence: the `Lp` class of `q ∘ Z` lies in `Qbar_L2`.
qbar_mem_L2 :
∀ q (hq : q ∈ Qbar),
let qLp := (toQbarL2 q hq).toLp _ let qMeas : qLp ∈ @lpMeas Ω ℝ ℝ _ _ _ m_Z m₀ 2 μ := by rw [mem_lpMeas_iff_aestronglyMeasurable] exact ((meas_of_Qbar q hq).comp (by rw [m_Z_eq]; exact comap_measurable _)).aestronglyMeasurable.congr (toQbarL2 q hq).coeFn_toLp.symm (⟨qLp, qMeas⟩ : @lpMeas Ω ℝ ℝ _ _ _ m_Z m₀ 2 μ) ∈ Qbar_L2
abbrev PrimalL2 reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the primal Hilbert space is the space of square-integrable random variables measurable with respect to the sigma-algebra generated by the covariate X.
Definition (Lean source)
abbrev InstrumentL2 reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the instrument Hilbert space is the space of square-integrable random variables measurable with respect to the sigma-algebra generated by the instrument Z.
Definition (Lean source)
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 its equivalence class in L²(σ(X)).
Definition (Lean source)
parameters
def
hL2 S hh :
S.PrimalL2
given by
hLp :
(S.toHbarL2 h hh).toLp _
have hX : @Measurable Ω S.𝒳 S.m_X S.inst𝒳 (fun ω => S.xOf (S.W ω)) := by rw [S.m_X_eq] exact comap_measurable _ have hm : hLp ∈ S.PrimalL2 := by rw [mem_lpMeas_iff_aestronglyMeasurable] exact ((S.meas_of_Hbar h hh).comp hX).aestronglyMeasurable.congr (S.toHbarL2 h hh).coeFn_toLp.symm ⟨hLp, hm⟩
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 its equivalence class in L²(σ(Z)).
Definition (Lean source)
parameters
def
qL2 S hq :
S.InstrumentL2
given by
qLp :
(S.toQbarL2 q hq).toLp _
have hZ : @Measurable Ω S.𝒵 S.m_Z S.inst𝒵 (fun ω => S.zOf (S.W ω)) := by rw [S.m_Z_eq] exact comap_measurable _ have hm : qLp ∈ S.InstrumentL2 := by rw [mem_lpMeas_iff_aestronglyMeasurable] exact ((S.meas_of_Qbar q hq).comp hZ).aestronglyMeasurable.congr (S.toQbarL2 q hq).coeFn_toLp.symm ⟨qLp, hm⟩
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 Ω μ
def
condExpStep S :
S.PrimalL2 → S.InstrumentL2
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 element of the full primal space L²(σ(X)), the NPIV projection operator is the orthogonal projection onto the closed dual candidate space of that element's conditional expectation given the instrument.
Definition (Lean source)
parameters
def
T S f :
S.InstrumentL2
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, every instrument function belonging to its critic space is almost-everywhere strongly measurable after composition with the instrument map.
Definition (Lean source)
parameters
def
QbarAEMeasurableMZ S :
Prop
given by
AEStronglyMeasurable[S.m_Z] (fun ω => f (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 : S.PrimalL2 := 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.PrimalL2) : Lp ℝ 2 μ)
((S.qL2 hf : S.InstrumentL2) : Lp ℝ 2 μ) := by
change inner ℝ
((S.condExpStep u : S.InstrumentL2) : Lp ℝ 2 μ)
((S.qL2 hf : S.InstrumentL2) : Lp ℝ 2 μ) =
inner ℝ ((u : S.PrimalL2) : Lp ℝ 2 μ)
((S.qL2 hf : S.InstrumentL2) : Lp ℝ 2 μ)
simpa [OperatorSystem.condExpStep] using
(MeasureTheory.inner_condExpL2_eq_inner_fun (E := ℝ) (𝕜 := ℝ)
S.m_Z_le (u : Lp ℝ 2 μ)
((S.qL2 hf : S.InstrumentL2) : Lp ℝ 2 μ) hq_meas)
have h_inner :
inner ℝ ((u : S.PrimalL2) : Lp ℝ 2 μ)
((S.qL2 hf : S.InstrumentL2) : Lp ℝ 2 μ) =
∫ ω, (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.PrimalL2) : Lp ℝ 2 μ)
((S.hL2 hh' : S.PrimalL2) : Lp ℝ 2 μ),
(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.PrimalL2) : Lp ℝ 2 μ) ω,
((S.qL2 hf : S.InstrumentL2) : Lp ℝ 2 μ) ω⟫_ℝ
= ⟪((S.hL2 hh : S.PrimalL2) : Lp ℝ 2 μ) ω
- ((S.hL2 hh' : S.PrimalL2) : Lp ℝ 2 μ) ω,
((S.qL2 hf : S.InstrumentL2) : Lp ℝ 2 μ) ω⟫_ℝ := by
have huω : ((u : S.PrimalL2) : Lp ℝ 2 μ) ω =
((S.hL2 hh : S.PrimalL2) : Lp ℝ 2 μ) ω
- ((S.hL2 hh' : S.PrimalL2) : Lp ℝ 2 μ) ω := 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.PrimalL2) : Lp ℝ 2 μ)
((S.qL2 hf : S.InstrumentL2) : Lp ℝ 2 μ) := 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 a random variable in L²(σ(X)), 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 a random variable in L²(σ(X)), the weak norm is the L²(σ(Z)) norm of its projected conditional expectation.
Definition (Lean source)
parameters
def
weakNorm S f :
ℝ
given by
‖S.T f‖
9 supporting declarations (lemmas, instances)
-
instCompleteSpacePrimalL2instance — For an NPIV operator system, its primal Hilbert space is complete.parametersS :OperatorSystem Ω μinstancegiven byby letI : Fact (S.m_X ≤ m₀) := ⟨S.m_X_le⟩ infer_instance -
instCompleteSpaceInstrumentL2instance — For an NPIV operator system, its instrument Hilbert space is complete.parametersS :OperatorSystem Ω μinstancegiven byby letI : Fact (S.m_Z ≤ m₀) := ⟨S.m_Z_le⟩ infer_instance -
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 : S.PrimalL2) : 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 : S.PrimalL2) : 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)) : S.InstrumentL2) = ((S.Qbar_L2.orthogonalProjection (S.condExpStep f)) : S.InstrumentL2) - ((S.Qbar_L2.orthogonalProjection (S.condExpStep g)) : S.InstrumentL2) 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 : S.PrimalL2) : 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 : S.PrimalL2) : Lp ℝ 2 μ))) : S.InstrumentL2) = ((S.Qbar_L2.orthogonalProjection (MeasureTheory.condExpL2 ℝ ℝ S.m_Z_le (f : Lp ℝ 2 μ))) : S.InstrumentL2) + ((S.Qbar_L2.orthogonalProjection (MeasureTheory.condExpL2 ℝ ℝ S.m_Z_le (g : Lp ℝ 2 μ))) : S.InstrumentL2) 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 : S.PrimalL2) : 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_le (E := ℝ) (𝕜 := ℝ) S.m_Z_le (f : Lp ℝ 2 μ)) _ = 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.PrimalL2) : Lp ℝ 2 μ) ω, ((S.hL2 hh : S.PrimalL2) : Lp ℝ 2 μ) ω⟫_ℝ ∂μ := by change inner ℝ ((S.hL2 hh : S.PrimalL2) : Lp ℝ 2 μ) ((S.hL2 hh : S.PrimalL2) : Lp ℝ 2 μ) = _ 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] -
strongNorm_hL2_sub_eq_eLpNorm_toReallemma — For an NPIV operator system, two primal candidate functions, and their membership proofs, the strong norm of the lifted difference equals the real extended $L^2$ norm of the pointwise difference.hypothesesProof (Lean source)
lemma strongNorm_hL2_sub_eq_eLpNorm_toReal (S : OperatorSystem Ω μ) {h h' : S.𝒳 → ℝ} (hh : h ∈ S.Hbar) (hh' : h' ∈ S.Hbar) : S.strongNorm (S.hL2 hh - S.hL2 hh') = (eLpNorm (fun ω => h (S.xOf (S.W ω)) - h' (S.xOf (S.W ω))) 2 μ).toReal := by rw [OperatorSystem.strongNorm] change ‖(S.toHbarL2 h hh).toLp _ - (S.toHbarL2 h' hh').toLp _‖ = _ rw [← MemLp.toLp_sub, Lp.norm_toLp] rfl
Adjoint 9 core · 2 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 Ω μ
def
condExpStepL S :
S.PrimalL2 →L[ℝ] S.InstrumentL2
given by
haveI := S.isFiniteMeasure (MeasureTheory.condExpL2 ℝ ℝ S.m_Z_le).comp S.PrimalL2.subtypeL
def Tlin reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the bundled NPIV operator is the continuous linear map on the full primal space that conditions an L²(σ(X)) element on the instrument and then orthogonally projects it onto the closed dual candidate space.
Definition (Lean source)
parameters
S :
OperatorSystem Ω μ
def
Tlin S :
S.PrimalL2 →L[ℝ] S.InstrumentL2
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)
parameters
S :
OperatorSystem Ω μ
def
Tstar_T S :
S.PrimalL2 →L[ℝ] S.PrimalL2
given by
S.Tadjoint.comp S.Tlin
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
letI : Fact (S.m_X ≤ m₀) := ⟨S.m_X_le⟩
letI : Fact (S.m_Z ≤ m₀) := ⟨S.m_Z_le⟩
have h :=
(IsSelfAdjoint.one (S.InstrumentL2 →L[ℝ] S.InstrumentL2)).adjoint_conj S.Tlin
simpa [Tstar_T, Tadjoint, ContinuousLinearMap.one_def] using h
def primalTrimEquiv reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the canonical isometric identification of L²(σ(X)) with ordinary L² under the measure trimmed to σ(X) is Mathlib's lpMeasToLpTrimLie.
Definition (Lean source)
def TlinTrim reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the trimmed-measure realization of its NPIV operator first maps ordinary L² under the σ(X)-trimmed measure back to L²(σ(X)) and then applies T.
Definition (Lean source)
parameters
S :
OperatorSystem Ω μ
def
given by
S.Tlin.comp S.primalTrimEquiv.symm.toContinuousLinearEquiv.toContinuousLinearMap
def TadjointTrim reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the adjoint of the trimmed-measure realization of its NPIV operator maps L²(σ(Z)) to ordinary L² under the σ(X)-trimmed measure.
Definition (Lean source)
def Tstar_T_trim reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the transported normal operator on ordinary L² under the σ(X)-trimmed measure is the adjoint-product of the transported NPIV operator.
Definition (Lean source)
2 supporting declarations (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)
-
Tstar_T_trim_isSelfAdjointlemma — For an NPIV operator system, the transported normal operator is self-adjoint.Proof (Lean source)
lemma Tstar_T_trim_isSelfAdjoint (S : OperatorSystem Ω μ) : IsSelfAdjoint S.Tstar_T_trim := by have h := (IsSelfAdjoint.one (S.InstrumentL2 →L[ℝ] S.InstrumentL2)).adjoint_conj S.TlinTrim simpa [Tstar_T_trim, TadjointTrim, ContinuousLinearMap.one_def] using h
Complexification_Part1 9 core · 14 supporting This first implementation part constructs real and imaginary projections, the isometric real embedding, and the complex lift of a real continuous linear operator. ★ complexLift_adjoint
Real-to-complex maps and operator lifts on L²
This first implementation part constructs real and imaginary projections, the
isometric real embedding, and the complex lift of a real continuous linear
operator. It proves reconstruction, adjoint, and self-adjointness laws, then
defines realCFC and establishes its application and identity rules.
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 I_smulCLM reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
Multiplication by the imaginary unit is a continuous real-linear transformation of complex-valued square-integrable functions. This helper supplies the imaginary-component transformation used to lift real NPIV operators to complex functions.
Definition (Lean source)
parameters
given by
L :
{ toFun := fun f => (Complex.I : ℂ) • f map_add' := by intro f g simp [smul_add] map_smul' := by intro r f apply Lp.ext filter_upwards [Lp.coeFn_smul (Complex.I : ℂ) (r • f), Lp.coeFn_smul r f, Lp.coeFn_smul r ((Complex.I : ℂ) • f), Lp.coeFn_smul (Complex.I : ℂ) f] with ω h_left h_rf h_right h_if change ((((Complex.I : ℂ) • (r • f : Lp ℂ 2 μ) : Lp ℂ 2 μ) : Ω → ℂ) ω) = (((r • ((Complex.I : ℂ) • f) : Lp ℂ 2 μ) : Ω → ℂ) ω) rw [h_left, h_right] simp only [Pi.smul_apply] rw [h_rf, h_if] change Complex.I * ((r : ℂ) * (((f : Lp ℂ 2 μ) : Ω → ℂ) ω)) = (r : ℂ) * (Complex.I * (((f : Lp ℂ 2 μ) : Ω → ℂ) ω)) ring } (: Lp ℂ 2 μ →ₗ[ℝ] Lp ℂ 2 μ)
L.mkContinuous 1 (by intro f rw [show ‖L f‖ = ‖f‖ by change ‖(Complex.I : ℂ) • f‖ = ‖f‖ simpa using (norm_smul (Complex.I : ℂ) f)] rw [one_mul])
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)
theorem complexLift_adjoint reviewed
⚑ flagged
Causalean.Estimation.NPIV.Complexification
For a measurable sample space with a measure and a continuous real-linear operator on real-valued square-integrable functions, complexifying the operator and then taking its adjoint gives the same operator as complexifying its real adjoint.
Formal statement
hypotheses
conclusion
(complexLift A).adjoint = complexLift A.adjoint
Proof (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]
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)
14 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] -
reLp_complexLiftlemma — Given a real continuous linear operator on a square-integrable space and a complex-valued square-integrable function, the real part of the operator's complexification equals the original operator applied to the function's real part.hypothesesconclusionProof (Lean source)
lemma reLp_complexLift (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (f : Lp ℂ 2 μ) : reLp (complexLift A f) = A (reLp f) := by rw [complexLift_apply] simp [map_add, reLp_I_smul, reLp_comp_ιLp, imLp_comp_ιLp] -
imLp_complexLiftlemma — Given a real continuous linear operator on a square-integrable space and a complex-valued square-integrable function, the imaginary part of the operator's complexification equals the original operator applied to the function's imaginary part.hypothesesconclusionProof (Lean source)
lemma imLp_complexLift (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (f : Lp ℂ 2 μ) : imLp (complexLift A f) = A (imLp f) := by rw [complexLift_apply] simp [map_add, imLp_I_smul, reLp_comp_ιLp, imLp_comp_ιLp] -
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] -
reLp_ofReal_smullemma — Given a real scalar and a complex-valued square-integrable function, the real part of their scalar product is the scalar times the function's real part.hypothesesProof (Lean source)
lemma reLp_ofReal_smul (r : ℝ) (f : Lp ℂ 2 μ) : reLp ((r : ℂ) • f) = r • reLp f := by apply Lp.ext filter_upwards [ContinuousLinearMap.coeFn_compLpL (RCLike.reCLM (K := ℂ)) ((r : ℂ) • f), Lp.coeFn_smul (r : ℂ) f, Lp.coeFn_smul r (reLp f), ContinuousLinearMap.coeFn_compLpL (RCLike.reCLM (K := ℂ)) f] with ω h_re_smul h_smul h_rhs h_re rw [h_rhs] simp only [Pi.smul_apply] rw [show (((reLp ((r : ℂ) • f) : Lp ℝ 2 μ) : Ω → ℝ) ω) = (RCLike.reCLM (K := ℂ)) ((((r : ℂ) • f : Lp ℂ 2 μ) : Ω → ℂ) ω) by simpa [reLp] using h_re_smul] rw [h_smul] simp only [Pi.smul_apply] rw [show (((reLp f : Lp ℝ 2 μ) : Ω → ℝ) ω) = (RCLike.reCLM (K := ℂ)) (((f : Lp ℂ 2 μ) : Ω → ℂ) ω) by simpa [reLp] using h_re] change ((r : ℂ) * (((f : Lp ℂ 2 μ) : Ω → ℂ) ω)).re = r * ((((f : Lp ℂ 2 μ) : Ω → ℂ) ω).re) simp -
inner_reLp_leftlemma — Given a complex-valued and a real-valued square-integrable function, the real inner product of the first function's real part with the second equals the real part of the complex inner product with the complex embedding of the second.hypothesesProof (Lean source)
lemma inner_reLp_left (u : Lp ℂ 2 μ) (v : Lp ℝ 2 μ) : inner ℝ (reLp u) v = (inner ℂ u (ιLp v)).re := by have h := inner_ιLp_right (μ := μ) v u calc inner ℝ (reLp u) v = inner ℝ v (reLp u) := by rw [real_inner_comm] _ = (inner ℂ (ιLp v) u).re := by rw [h] simp _ = (inner ℂ u (ιLp v)).re := by simpa using (inner_re_symm (𝕜 := ℂ) (x := u) (y := ιLp v)).symm -
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
Tikhonov 5 core · 4 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.tikhonovTarget, 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 primal Tikhonov bilinear form sends two elements of L²(σ(X)) to .
Definition (Lean source)
parameters
def
tikhonovBilin S lambda :
S.PrimalL2 →L[ℝ] S.PrimalL2 →L[ℝ] ℝ
given by
(((innerSL ℝ : S.InstrumentL2 →L[ℝ] S.InstrumentL2 →L[ℝ] ℝ).comp S.Tlin).flip.comp S.Tlin).flip
+ lambda • (innerSL ℝ : S.PrimalL2 →L[ℝ] S.PrimalL2 →L[ℝ] ℝ)
def tikhonovTarget reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, the Tikhonov target functional sends each element of L²(σ(X)) to the inner product of its transformed image with the transformed structural function.
Definition (Lean source)
parameters
S :
OperatorSystem Ω μ
def
tikhonovTarget S :
S.PrimalL2 →L[ℝ] ℝ
given by
((innerSL ℝ : S.InstrumentL2 →L[ℝ] S.InstrumentL2 →L[ℝ] ℝ) (S.Tlin (S.hL2 S.h₀_mem))).comp S.Tlin
def tikhonovMinimiserL2 reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system and a real regularization level, the population Tikhonov minimiser is the unique variational solution in L²(σ(X)) when λ is positive, and is zero otherwise. The construction applies Lax–Milgram to the coercive Tikhonov form and target functional for positive λ, and returns zero otherwise.
Definition (Lean source)
parameters
def
tikhonovMinimiserL2 S lambda :
S.PrimalL2
given by
if h : 0 < lambda then let complete : CompleteSpace S.PrimalL2 := inferInstance let coercive := tikhonovBilin_isCoercive S h let Bsharp := @IsCoercive.continuousLinearEquivOfBilin S.PrimalL2 _ _ complete (S.tikhonovBilin lambda) coercive let w : S.PrimalL2 := (@InnerProductSpace.toDual ℝ S.PrimalL2 _ _ _ complete).symm S.tikhonovTarget Bsharp.symm w 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 element v of L²(σ(X)), 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
conclusion
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)
Proof (Lean source)
lemma tikhonovMinimiserL2_optimality
(S : OperatorSystem Ω μ)
{lambda : ℝ} (lambda_pos : 0 < lambda)
(v : S.PrimalL2) :
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.PrimalL2 := inferInstance
let coercive := tikhonovBilin_isCoercive S lambda_pos
let Bsharp :=
@IsCoercive.continuousLinearEquivOfBilin S.PrimalL2 _ _ complete
(S.tikhonovBilin lambda) coercive
let w : S.PrimalL2 :=
(@InnerProductSpace.toDual ℝ S.PrimalL2 _ _ _ complete).symm S.tikhonovTarget
let ustar : S.PrimalL2 := Bsharp.symm w
have hmin : S.tikhonovMinimiserL2 lambda = ustar := by
simp [tikhonovMinimiserL2, lambda_pos, Bsharp, w, ustar]
have hLM :=
@IsCoercive.continuousLinearEquivOfBilin_apply S.PrimalL2 _ _ complete
(S.tikhonovBilin lambda) coercive ustar v
have htarget : inner ℝ w v = S.tikhonovTarget v := by
exact @InnerProductSpace.toDual_symm_apply ℝ S.PrimalL2 _ _ _ complete
(x := v) (y := S.tikhonovTarget)
have hvar : S.tikhonovBilin lambda ustar v = S.tikhonovTarget v := by
calc
S.tikhonovBilin lambda ustar v = inner ℝ (Bsharp ustar) v :=
hLM.symm
_ = inner ℝ w v := by simp [ustar]
_ = S.tikhonovTarget v := htarget
rw [hmin]
simpa [tikhonovBilin_apply, tikhonovTarget_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 element h of L²(σ(X)), 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
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 Ω μ)
{lambda : ℝ} (lambda_pos : 0 < lambda)
(h : S.PrimalL2) :
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 hopt := S.tikhonovMinimiserL2_optimality lambda_pos (h - hstar)
apply le_of_eq
simp [hstar, norm_sub_sq_real, ContinuousLinearMap.map_sub, inner_sub_right,
real_inner_comm] at hopt ⊢
nlinarith [hopt]
4 supporting declarations (lemmas, instances)
-
tikhonovBilin_applylemma — Pointwise formula for tikhonovBilin.hypothesesconclusionS.tikhonovBilin lambda u v = inner ℝ (S.Tlin u) (S.Tlin v) + lambda * inner ℝ u vProof (Lean source)
lemma tikhonovBilin_apply (S : OperatorSystem Ω μ) (lambda : ℝ) (u v : S.PrimalL2) : S.tikhonovBilin lambda u v = inner ℝ (S.Tlin u) (S.Tlin v) + lambda * inner ℝ u v := by change (((((innerSL ℝ : S.InstrumentL2 →L[ℝ] S.InstrumentL2 →L[ℝ] ℝ).comp S.Tlin).flip.comp S.Tlin).flip + lambda • (innerSL ℝ : S.PrimalL2 →L[ℝ] S.PrimalL2 →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 : S.PrimalL2) : S.tikhonovBilin lambda u v = S.tikhonovBilin lambda v u := by simp [tikhonovBilin_apply, real_inner_comm] -
tikhonovBilin_isCoercivelemma — For a nonparametric instrumental-variables operator system and a strictly positive regularization level, the primal Tikhonov bilinear form is coercive.hypothesesconclusionIsCoercive (S.tikhonovBilin lambda)Proof (Lean source)
lemma tikhonovBilin_isCoercive (S : OperatorSystem Ω μ) {lambda : ℝ} (lambda_pos : 0 < lambda) : IsCoercive (S.tikhonovBilin lambda) := by refine ⟨lambda, lambda_pos, ?_⟩ intro u change lambda * ‖u‖ * ‖u‖ ≤ S.tikhonovBilin lambda u u rw [tikhonovBilin_apply] simp nlinarith [sq_nonneg ‖S.Tlin u‖] -
tikhonovTarget_applylemma — Pointwise formula for the target functional.hypothesesconclusionS.tikhonovTarget v = inner ℝ (S.Tlin (S.hL2 S.h₀_mem)) (S.Tlin v)Proof (Lean source)
lemma tikhonovTarget_apply (S : OperatorSystem Ω μ) (v : S.PrimalL2) : S.tikhonovTarget v = inner ℝ (S.Tlin (S.hL2 S.h₀_mem)) (S.Tlin v) := by simp [tikhonovTarget, coe_innerSL_apply]
SpectralCalculus_Part1 7 core · 9 supporting This first spectral part defines SpectralSourceCondition, the real functional-calculus power (T†T)^(β/2), and its uniform bias constant. ★ tikhonovMinimiserL2_eq_resolvent
Spectral source operators and the Tikhonov resolvent
This first spectral part defines SpectralSourceCondition, the real
functional-calculus power (T†T)^(β/2), and its uniform bias constant. It
identifies the ambient Lax–Milgram Tikhonov minimizer with the resolvent formula
and proves the scalar residual estimates used by the later bias bounds.
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
For an NPIV operator system and a source exponent, a spectral source condition is the standard source condition on the normal operator of T : L²(σ(X)) → L²(σ(Z)).
Definition (Lean source)
parameters
def realCFCTrim reviewed
⚑ flagged
Causalean.Estimation.NPIV.OperatorSystem
For an NPIV operator system, an operator on the trimmed realization of L²(σ(X)), and a real symbol, the real continuous functional calculus of that operator uses the measurable structure σ(X) explicitly.
Definition (Lean source)
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.m_X (μ.trim S.m_X_le) S.Tstar_T_trim (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. 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
conclusion
S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda)
= @Complexification.realCFC Ω S.m_X (μ.trim S.m_X_le) S.Tstar_T_trim (fun x => x / (lambda + x)) (S.primalTrimEquiv (S.hL2 S.h₀_mem))
Proof (Lean source)
theorem tikhonovMinimiserL2_eq_resolvent
{lambda : ℝ} (lambda_pos : 0 < lambda) :
S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda)
= @Complexification.realCFC Ω S.m_X (μ.trim S.m_X_le)
S.Tstar_T_trim (fun x => x / (lambda + x))
(S.primalTrimEquiv (S.hL2 S.h₀_mem)) := by
set A := S.Tstar_T_trim with hA_def
set h₀ := S.primalTrimEquiv (S.hL2 S.h₀_mem) with hh₀_def
set R : Lp ℝ 2 (μ.trim S.m_X_le) :=
@Complexification.realCFC Ω S.m_X (μ.trim S.m_X_le)
A (fun x => x / (lambda + x)) h₀
set h_star : Lp ℝ 2 (μ.trim S.m_X_le) :=
S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda)
have hvar : ∀ v : Lp ℝ 2 (μ.trim S.m_X_le),
inner ℝ (S.TlinTrim h_star) (S.TlinTrim v) + lambda * inner ℝ h_star v
= inner ℝ (S.TlinTrim h₀) (S.TlinTrim v) := by
intro v
have hopt := S.tikhonovMinimiserL2_optimality lambda_pos
(S.primalTrimEquiv.symm v)
have hinner :
inner ℝ (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda)) v =
inner ℝ (S.tikhonovMinimiserL2 lambda)
(S.primalTrimEquiv.symm v) := by
calc
inner ℝ (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda)) v =
inner ℝ (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda))
(S.primalTrimEquiv (S.primalTrimEquiv.symm v)) := by
rw [S.primalTrimEquiv.apply_symm_apply]
_ = inner ℝ (S.tikhonovMinimiserL2 lambda)
(S.primalTrimEquiv.symm v) :=
S.primalTrimEquiv.inner_map_map _ _
rw [hinner]
simpa [h_star, h₀, OperatorSystem.TlinTrim] using hopt
have hop_star :
S.TadjointTrim (S.TlinTrim h_star) + lambda • h_star =
S.TadjointTrim (S.TlinTrim h₀) := by
apply ext_inner_right ℝ
intro v
rw [inner_add_left, inner_smul_left]
rw [OperatorSystem.TadjointTrim]
rw [ContinuousLinearMap.adjoint_inner_left, ContinuousLinearMap.adjoint_inner_left]
simpa using hvar v
have hop_star' :
A h_star + lambda • h_star = A h₀ := by
simpa [hA_def, OperatorSystem.Tstar_T_trim,
ContinuousLinearMap.comp_apply] using hop_star
have hA_sa : IsSelfAdjoint A := by
simpa [hA_def] using S.Tstar_T_trim_isSelfAdjoint
have hres :
(algebraMap ℝ
(Lp ℝ 2 (μ.trim S.m_X_le) →L[ℝ]
Lp ℝ 2 (μ.trim S.m_X_le)) lambda + A) R = A h₀ := by
have h := @resolvent_left_inverse Ω S.m_X (μ.trim S.m_X_le) A hA_sa (by
intro x hx
exact Tstar_T_spectrum_nonneg S x (by simpa [hA_def] using hx)) lambda lambda_pos
have happ :=
congrArg (fun T : Lp ℝ 2 (μ.trim S.m_X_le) →L[ℝ]
Lp ℝ 2 (μ.trim S.m_X_le) => T h₀) h
simpa [R] using happ
have hop_R : A R + lambda • R = A h₀ := 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
rw [map_sub, smul_sub]
abel
_ = 0 := by rw [heq]; simp
have hpos_self :
inner ℝ (A (h_star - R)) (h_star - R) = ‖S.TlinTrim (h_star - R)‖ ^ 2 := by
subst A
change inner ℝ (S.TadjointTrim (S.TlinTrim (h_star - R))) (h_star - R) = _
rw [OperatorSystem.TadjointTrim, ContinuousLinearMap.adjoint_inner_left]
exact real_inner_self_eq_norm_sq _
have hzero :
‖S.TlinTrim (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.TlinTrim (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, h₀] using sub_eq_zero.mp hsub_zero
9 supporting declarations (lemmas, instances)
-
Tstar_T_isPositivelemma — T†T is a positive operator.Proof (Lean source)
lemma Tstar_T_isPositive (S : OperatorSystem Ω μ) : S.Tstar_T_trim.IsPositive := by unfold OperatorSystem.Tstar_T_trim OperatorSystem.TadjointTrim simpa [ContinuousLinearMap.comp_def, ContinuousLinearMap.comp_apply] using ContinuousLinearMap.isPositive_adjoint_comp_self S.TlinTrim -
Tstar_T_spectrum_nonneglemma — Positivity of T†T: its real spectrum lies in [0, ∞).hypothesesconclusion0 ≤ xProof (Lean source)
lemma Tstar_T_spectrum_nonneg (S : OperatorSystem Ω μ) : ∀ x ∈ spectrum ℝ S.Tstar_T_trim, 0 ≤ x := by intro x hx exact spectrum_nonneg_of_nonneg (a := S.Tstar_T_trim) (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.primalTrimEquiv (S.hL2 S.h₀_mem)= sc.spectralPower (S.primalTrimEquiv (S.hL2 sc.w₀_mem))Proof (Lean source)
lemma spectral_identity_h₀ (sc : SpectralSourceCondition S β) : S.primalTrimEquiv (S.hL2 S.h₀_mem) = sc.spectralPower (S.primalTrimEquiv (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) _ -
realCFC_congr_on_spectrum_locallemma — Given a continuous linear operator and two real functions, if the functions agree on the operator's spectrum and the operator is self-adjoint, then their real continuous functional calculi at that operator agree.hypothesesconclusionComplexification.realCFC A f = Complexification.realCFC A gProof (Lean source)
lemma realCFC_congr_on_spectrum_local (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (f g : ℝ → ℝ) (h : ∀ x ∈ spectrum ℝ A, f x = g x) (hA : IsSelfAdjoint A) : Complexification.realCFC A f = Complexification.realCFC A g := by apply ContinuousLinearMap.ext intro v change Complexification.reLp (cfc (fun z : ℂ => (f z.re : ℂ)) (Complexification.complexLift A) (Complexification.ιLp v)) = Complexification.reLp (cfc (fun z : ℂ => (g z.re : ℂ)) (Complexification.complexLift A) (Complexification.ιLp v)) congr 2 apply cfc_congr intro z hz have hzr : z.re ∈ spectrum ℝ A := spectrum_complexLift_subset_real_local hA hz simpa using congrArg (fun r : ℝ => (r : ℂ)) (h z.re hzr) -
realCFC_sub_locallemma — Given a self-adjoint continuous linear operator and two continuous real functions, the real continuous functional calculus of their difference equals the difference of their calculi.hypotheseshA :f g :ℝ → ℝhf :hg :conclusionComplexification.realCFC A (fun x => f x - g x)= Complexification.realCFC A f - Complexification.realCFC A gProof (Lean source)
lemma realCFC_sub_local (A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ) (hA : IsSelfAdjoint A) (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) : Complexification.realCFC A (fun x => f x - g x) = Complexification.realCFC A f - Complexification.realCFC A g := by ext1 v rw [Complexification.realCFC_apply A hA (fun x => f x - g x) (hf.sub hg) v] simp only [ContinuousLinearMap.sub_apply] rw [Complexification.realCFC_apply A hA f hf v] rw [Complexification.realCFC_apply 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_sub (fun z : ℂ => (f z.re : ℂ)) (fun z : ℂ => (g z.re : ℂ)) (Complexification.complexLift A) (hf := (Complex.continuous_ofReal.comp (hf.comp Complex.continuous_re)).continuousOn) (hg := (Complex.continuous_ofReal.comp (hg.comp Complex.continuous_re)).continuousOn)] simp -
residual_symbol_bound_smalllemma — For a nonnegative spectral value, a positive regularization level, smoothness between zero and two, and a scale at least one, the absolute residual source symbol is bounded by the stated scale and regularization power.hypothesesx lambda β B :ℝhl :0 < lambdahx :0 ≤ xhβ0 :0 ≤ βhβ2 :β ≤ 2hB :1 ≤ BconclusionProof (Lean source)
lemma residual_symbol_bound_small {x lambda β B : ℝ} (hl : 0 < lambda) (hx : 0 ≤ x) (hβ0 : 0 ≤ β) (hβ2 : β ≤ 2) (hB : 1 ≤ B) : |(-lambda * sourceSymbol β x / (lambda + max 0 x))| ≤ B ^ (β / 2) * lambda ^ (min β 2 / 2) := by have hb_nonneg : 0 ≤ β / 2 := by linarith have hb_le_one : β / 2 ≤ 1 := by linarith have hden_pos : 0 < lambda + x := by linarith have hden_max : lambda + max 0 x = lambda + x := by rw [max_eq_right hx] have hsrc : sourceSymbol β x = x ^ (β / 2) := by simp [sourceSymbol, max_eq_left hx] have hmin : min β 2 = β := min_eq_left hβ2 rw [hden_max, hsrc, hmin] rw [abs_div, abs_mul, abs_neg, abs_of_pos hl] rw [abs_of_nonneg (Real.rpow_nonneg hx _), abs_of_pos hden_pos] have hx_le_den : x ≤ lambda + x := by linarith have hl_le_den : lambda ≤ lambda + x := by linarith have hpow_le : x ^ (β / 2) ≤ (lambda + x) ^ (β / 2) := Real.rpow_le_rpow hx hx_le_den hb_nonneg have hdiv_le : x ^ (β / 2) / (lambda + x) ≤ (lambda + x) ^ (β / 2) / (lambda + x) := div_le_div_of_nonneg_right hpow_le (le_of_lt hden_pos) have hden_pow : (lambda + x) ^ (β / 2) / (lambda + x) = (lambda + x) ^ (β / 2 - 1) := by rw [Real.rpow_sub hden_pos, Real.rpow_one] have hpow_neg : (lambda + x) ^ (β / 2 - 1) ≤ lambda ^ (β / 2 - 1) := by exact Real.rpow_le_rpow_of_nonpos hl hl_le_den (by linarith) have hmul_lam : lambda * lambda ^ (β / 2 - 1) = lambda ^ (β / 2) := by calc lambda * lambda ^ (β / 2 - 1) = lambda ^ 1 * lambda ^ (β / 2 - 1) := by simp _ = lambda ^ (1 + (β / 2 - 1)) := (Real.rpow_add hl 1 (β / 2 - 1)).symm _ = lambda ^ (β / 2) := by ring_nf have hsmall : lambda * x ^ (β / 2) / (lambda + x) ≤ lambda ^ (β / 2) := by calc lambda * x ^ (β / 2) / (lambda + x) = lambda * (x ^ (β / 2) / (lambda + x)) := by ring _ ≤ lambda * ((lambda + x) ^ (β / 2) / (lambda + x)) := by gcongr _ = lambda * (lambda + x) ^ (β / 2 - 1) := by rw [hden_pow] _ ≤ lambda * lambda ^ (β / 2 - 1) := by gcongr _ = lambda ^ (β / 2) := hmul_lam have hBpow : 1 ≤ B ^ (β / 2) := Real.one_le_rpow hB hb_nonneg have hlpow_nonneg : 0 ≤ lambda ^ (β / 2) := Real.rpow_nonneg (le_of_lt hl) _ calc lambda * x ^ (β / 2) / (lambda + x) ≤ lambda ^ (β / 2) := hsmall _ ≤ B ^ (β / 2) * lambda ^ (β / 2) := by nlinarith -
residual_symbol_bound_largelemma — For a nonnegative spectral value bounded by a scale, a positive regularization level, a smoothness value above two, and a scale at least one, the absolute residual source symbol is bounded by the stated scale and regularization power.hypothesesx lambda β B :ℝhl :0 < lambdahx :0 ≤ xhxB :x ≤ Bhβ2 :2 < βhB :1 ≤ BconclusionProof (Lean source)
lemma residual_symbol_bound_large {x lambda β B : ℝ} (hl : 0 < lambda) (hx : 0 ≤ x) (hxB : x ≤ B) (hβ2 : 2 < β) (hB : 1 ≤ B) : |(-lambda * sourceSymbol β x / (lambda + max 0 x))| ≤ B ^ (β / 2) * lambda ^ (min β 2 / 2) := by have hb_pos : 0 < β / 2 := by linarith have hb_minus_nonneg : 0 ≤ β / 2 - 1 := by linarith have hden_pos : 0 < lambda + x := by linarith have hden_max : lambda + max 0 x = lambda + x := by rw [max_eq_right hx] have hsrc : sourceSymbol β x = x ^ (β / 2) := by simp [sourceSymbol, max_eq_left hx] have hmin : min β 2 = 2 := min_eq_right (le_of_lt hβ2) rw [hden_max, hsrc, hmin] rw [abs_div, abs_mul, abs_neg, abs_of_pos hl] rw [abs_of_nonneg (Real.rpow_nonneg hx _), abs_of_pos hden_pos] rw [show (2 : ℝ) / 2 = 1 by norm_num, Real.rpow_one] have hB_pos : 0 < B := lt_of_lt_of_le zero_lt_one hB have hquot : x ^ (β / 2) / (lambda + x) ≤ B ^ (β / 2) := by by_cases hxzero : x = 0 · subst x have hb_ne : β / 2 ≠ 0 := ne_of_gt hb_pos rw [Real.zero_rpow hb_ne] have hden0 : lambda + 0 = lambda := by ring rw [hden0, zero_div] exact Real.rpow_nonneg (le_of_lt hB_pos) _ · have hx_pos : 0 < x := lt_of_le_of_ne hx (Ne.symm hxzero) have hx_le_den : x ≤ lambda + x := by linarith have hdiv_le : x ^ (β / 2) / (lambda + x) ≤ x ^ (β / 2) / x := div_le_div_of_nonneg_left (Real.rpow_nonneg hx _) hx_pos hx_le_den have hxpow_div : x ^ (β / 2) / x = x ^ (β / 2 - 1) := by rw [Real.rpow_sub hx_pos, Real.rpow_one] have hxBpow : x ^ (β / 2 - 1) ≤ B ^ (β / 2 - 1) := Real.rpow_le_rpow hx hxB hb_minus_nonneg have hBexp : B ^ (β / 2 - 1) ≤ B ^ (β / 2) := Real.rpow_le_rpow_of_exponent_le hB (by linarith) calc x ^ (β / 2) / (lambda + x) ≤ x ^ (β / 2) / x := hdiv_le _ = x ^ (β / 2 - 1) := hxpow_div _ ≤ B ^ (β / 2 - 1) := hxBpow _ ≤ B ^ (β / 2) := hBexp calc lambda * x ^ (β / 2) / (lambda + x) = lambda * (x ^ (β / 2) / (lambda + x)) := by ring _ ≤ lambda * B ^ (β / 2) := by gcongr _ = B ^ (β / 2) * lambda := by ring
SpectralCalculus_Part2 3 core · 0 supporting This second spectral part lifts the scalar residual estimates to the normal operator and proves the strong- and weak-metric bias inequalities. ★ strong_bias★ weak_bias
Strong and weak spectral Tikhonov bias bounds
This second spectral part lifts the scalar residual estimates to the normal
operator and proves the strong- and weak-metric bias inequalities. It ends
with TikhonovPullback, the explicit witness that an ambient L² minimizer is
represented by a member of the primal candidate set.
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
‖S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem)‖ ^ 2
≤ sc.biasConst * ‖S.primalTrimEquiv (S.hL2 sc.w₀_mem)‖ ^ 2 * lambda ^ (min β 2)
Proof (Lean source)
theorem strong_bias (sc : SpectralSourceCondition S β)
{lambda : ℝ} (lambda_pos : 0 < lambda) :
‖S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem)‖ ^ 2
≤ sc.biasConst * ‖S.primalTrimEquiv (S.hL2 sc.w₀_mem)‖ ^ 2 * lambda ^ (min β 2) := by
by_cases hnt : Nontrivial (Lp ℝ 2 (μ.trim S.m_X_le))
swap
· haveI : Subsingleton (Lp ℝ 2 (μ.trim S.m_X_le)) := not_nontrivial_iff_subsingleton.mp hnt
have hdiff : S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (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.primalTrimEquiv (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 (μ.trim S.m_X_le)) := hnt
haveI : NormOneClass (Lp ℝ 2 (μ.trim S.m_X_le) →L[ℝ] Lp ℝ 2 (μ.trim S.m_X_le)) := ContinuousLinearMap.normOneClass
set A := S.Tstar_T_trim with hA_def
set w := S.primalTrimEquiv (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_trim_isSelfAdjoint
have hβ : 0 ≤ β := sc.beta_pos.le
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 :
S.realCFCTrim A (fun x => x / (lambda + x)) =
S.realCFCTrim A rSafe := by
unfold OperatorSystem.realCFCTrim
apply @realCFC_congr_on_spectrum_local Ω S.m_X (μ.trim S.m_X_le) A
· intro x hx
have hx0 : 0 ≤ x := Tstar_T_spectrum_nonneg S x (by simpa [hA_def] using hx)
dsimp [rSafe]
rw [max_eq_right hx0]
· exact hA_sa
have hmul : S.realCFCTrim A prod =
(S.realCFCTrim A rSafe).comp
(S.realCFCTrim A (sourceSymbol β)) := by
dsimp [prod]
simpa [OperatorSystem.realCFCTrim] using
(@Complexification.realCFC_mul Ω S.m_X (μ.trim S.m_X_le) A hA_sa
rSafe (sourceSymbol β) hr_cont hsrc_cont)
have hsub_cfc : S.realCFCTrim A (fun x => prod x - sourceSymbol β x) =
S.realCFCTrim A prod - S.realCFCTrim A (sourceSymbol β) :=
by
simpa [OperatorSystem.realCFCTrim] using
(@realCFC_sub_local Ω S.m_X (μ.trim S.m_X_le) A hA_sa
prod (sourceSymbol β) (hr_cont.mul hsrc_cont) hsrc_cont)
have hsymbol : S.realCFCTrim A (fun x => prod x - sourceSymbol β x) =
S.realCFCTrim A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) := by
unfold OperatorSystem.realCFCTrim
apply @realCFC_congr_on_spectrum_local Ω S.m_X (μ.trim S.m_X_le) A
· intro x hx
have hx0 : 0 ≤ x := Tstar_T_spectrum_nonneg S 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.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem) =
S.realCFCTrim A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) w := by
calc
S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem)
= (S.realCFCTrim A rSafe)
((S.realCFCTrim A (sourceSymbol β)) w) -
(S.realCFCTrim A (sourceSymbol β)) w := by
rw [tikhonovMinimiserL2_eq_resolvent (S := S) lambda_pos]
rw [sc.spectral_identity]
rw [hsource_eq]
change (S.realCFCTrim S.Tstar_T_trim (fun x => x / (lambda + x)))
((S.realCFCTrim S.Tstar_T_trim (sourceSymbol β))
(S.primalTrimEquiv (S.hL2 sc.w₀_mem))) -
(S.realCFCTrim S.Tstar_T_trim (sourceSymbol β))
(S.primalTrimEquiv (S.hL2 sc.w₀_mem)) = _
rw [← hA_def, ← hw_def]
rw [hres_safe]
_ = ((S.realCFCTrim A rSafe).comp
(S.realCFCTrim A (sourceSymbol β))) w -
(S.realCFCTrim A (sourceSymbol β)) w := by rfl
_ = (S.realCFCTrim A prod -
S.realCFCTrim A (sourceSymbol β)) w := by
rw [← hmul]
simp only [ContinuousLinearMap.sub_apply]
_ = S.realCFCTrim A (fun x => prod x - sourceSymbol β x) w := by
rw [hsub_cfc]
_ = S.realCFCTrim 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 := Tstar_T_spectrum_nonneg S 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 Ω S.m_X (μ.trim S.m_X_le) A hA_sa
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) hsafe_cont
c hc_nonneg hsup w
have hsq :
‖S.realCFCTrim 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
(S.realCFCTrim 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.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem)‖ ^ 2
= ‖S.realCFCTrim A
(fun x => -lambda * sourceSymbol β x / (lambda + max 0 x)) w‖ ^ 2 := by
rw [hresid]
_ ≤ (c * ‖w‖) ^ 2 := hsq
_ = sc.biasConst * ‖S.primalTrimEquiv (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
‖S.TlinTrim (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem))‖ ^ 2
≤ sc.biasConst * ‖S.primalTrimEquiv (S.hL2 sc.w₀_mem)‖ ^ 2 * lambda ^ (min (β + 1) 2)
Proof (Lean source)
theorem weak_bias (sc : SpectralSourceCondition S β)
{lambda : ℝ} (lambda_pos : 0 < lambda) :
‖S.TlinTrim (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem))‖ ^ 2
≤ sc.biasConst * ‖S.primalTrimEquiv (S.hL2 sc.w₀_mem)‖ ^ 2 * lambda ^ (min (β + 1) 2) := by
by_cases hnt : Nontrivial (Lp ℝ 2 (μ.trim S.m_X_le))
swap
· haveI : Subsingleton (Lp ℝ 2 (μ.trim S.m_X_le)) := not_nontrivial_iff_subsingleton.mp hnt
have hdom :
S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) -
S.primalTrimEquiv (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.primalTrimEquiv (S.hL2 sc.w₀_mem)‖ ^ 2 * lambda ^ (min (β + 1) 2) :=
mul_nonneg (mul_nonneg sc.biasConst_nonneg (sq_nonneg _)) hpow_nonneg
simpa [hdom] using hrhs_nonneg
haveI : Nontrivial (Lp ℝ 2 (μ.trim S.m_X_le)) := hnt
haveI : NormOneClass (Lp ℝ 2 (μ.trim S.m_X_le) →L[ℝ] Lp ℝ 2 (μ.trim S.m_X_le)) := ContinuousLinearMap.normOneClass
set A := S.Tstar_T_trim with hA_def
set w := S.primalTrimEquiv (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_trim_isSelfAdjoint
have hβ : 0 ≤ β := sc.beta_pos.le
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 :
S.realCFCTrim A (fun x => x / (lambda + x)) =
S.realCFCTrim A rSafe := by
unfold OperatorSystem.realCFCTrim
apply @realCFC_congr_on_spectrum_local Ω S.m_X (μ.trim S.m_X_le) A
· intro x hx
have hx0 : 0 ≤ x := Tstar_T_spectrum_nonneg S x (by simpa [hA_def] using hx)
dsimp [rSafe]
rw [max_eq_right hx0]
· exact hA_sa
have hmul : S.realCFCTrim A prod =
(S.realCFCTrim A rSafe).comp
(S.realCFCTrim A (sourceSymbol β)) := by
dsimp [prod]
simpa [OperatorSystem.realCFCTrim] using
(@Complexification.realCFC_mul Ω S.m_X (μ.trim S.m_X_le) A hA_sa
rSafe (sourceSymbol β) hr_cont hsrc_cont)
have hsub_cfc : S.realCFCTrim A (fun x => prod x - sourceSymbol β x) =
S.realCFCTrim A prod - S.realCFCTrim A (sourceSymbol β) :=
by
simpa [OperatorSystem.realCFCTrim] using
(@realCFC_sub_local Ω S.m_X (μ.trim S.m_X_le) A hA_sa
prod (sourceSymbol β) (hr_cont.mul hsrc_cont) hsrc_cont)
have hsymbol : S.realCFCTrim A (fun x => prod x - sourceSymbol β x) =
S.realCFCTrim A f := by
rw [hf_def]
unfold OperatorSystem.realCFCTrim
apply @realCFC_congr_on_spectrum_local Ω S.m_X (μ.trim S.m_X_le) A
· intro x hx
have hx0 : 0 ≤ x := Tstar_T_spectrum_nonneg S 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.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem) =
S.realCFCTrim A f w := by
calc
S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem)
= (S.realCFCTrim A rSafe)
((S.realCFCTrim A (sourceSymbol β)) w) -
(S.realCFCTrim A (sourceSymbol β)) w := by
rw [tikhonovMinimiserL2_eq_resolvent (S := S) lambda_pos]
rw [sc.spectral_identity]
rw [hsource_eq]
change (S.realCFCTrim S.Tstar_T_trim (fun x => x / (lambda + x)))
((S.realCFCTrim S.Tstar_T_trim (sourceSymbol β))
(S.primalTrimEquiv (S.hL2 sc.w₀_mem))) -
(S.realCFCTrim S.Tstar_T_trim (sourceSymbol β))
(S.primalTrimEquiv (S.hL2 sc.w₀_mem)) = _
rw [← hA_def, ← hw_def]
rw [hres_safe]
_ = ((S.realCFCTrim A rSafe).comp
(S.realCFCTrim A (sourceSymbol β))) w -
(S.realCFCTrim A (sourceSymbol β)) w := by rfl
_ = (S.realCFCTrim A prod -
S.realCFCTrim A (sourceSymbol β)) w := by
rw [← hmul]
simp only [ContinuousLinearMap.sub_apply]
_ = S.realCFCTrim A (fun x => prod x - sourceSymbol β x) w := by
rw [hsub_cfc]
_ = S.realCFCTrim A f w := by rw [hsymbol]
have hAcomp : A.comp (S.realCFCTrim A f) =
S.realCFCTrim A q := by
rw [hq_def]
rw [show (fun x : ℝ => x * f x) = fun x : ℝ => id x * f x by rfl]
unfold OperatorSystem.realCFCTrim
rw [@Complexification.realCFC_mul Ω S.m_X (μ.trim S.m_X_le) 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 Ω S.m_X (μ.trim S.m_X_le) A hA_sa
((@Complexification.realCFC Ω S.m_X (μ.trim S.m_X_le) A f) v)]
have hfg_comp : (S.realCFCTrim A f).comp (S.realCFCTrim A q) =
S.realCFCTrim A g := by
unfold OperatorSystem.realCFCTrim
rw [← @Complexification.realCFC_mul Ω S.m_X (μ.trim S.m_X_le) A hA_sa
f q hf_cont hq_cont]
rw [hg_def, hq_def]
congr 1
funext x
ring
have hTu_sq :
‖S.TlinTrim (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem))‖ ^ 2 =
inner ℝ (S.realCFCTrim A g w) w := by
rw [hresid]
have hTstar :
‖S.TlinTrim (S.realCFCTrim A f w)‖ ^ 2 =
inner ℝ (A (S.realCFCTrim A f w))
(S.realCFCTrim A f w) := by
rw [← real_inner_self_eq_norm_sq]
subst A
change inner ℝ (S.TlinTrim (S.realCFCTrim S.Tstar_T_trim f w))
(S.TlinTrim (S.realCFCTrim S.Tstar_T_trim f w)) =
inner ℝ (S.TadjointTrim (S.TlinTrim (S.realCFCTrim S.Tstar_T_trim f w)))
(S.realCFCTrim S.Tstar_T_trim f w)
rw [OperatorSystem.TadjointTrim, ContinuousLinearMap.adjoint_inner_left]
rw [hTstar]
have hAu : A (S.realCFCTrim A f w) =
S.realCFCTrim A q w := by
change (A.comp (S.realCFCTrim A f)) w =
S.realCFCTrim A q w
rw [hAcomp]
rw [hAu]
have hf_sa : IsSelfAdjoint (S.realCFCTrim A f) :=
by
simpa [OperatorSystem.realCFCTrim] using
(@Complexification.realCFC_isSelfAdjoint Ω S.m_X (μ.trim S.m_X_le)
A hA_sa f hf_cont)
calc
inner ℝ (S.realCFCTrim A q w) (S.realCFCTrim A f w)
= inner ℝ ((S.realCFCTrim A f) (S.realCFCTrim A q w)) w := by
exact ((ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mp hf_sa)
(S.realCFCTrim A q w) w).symm
_ = inner ℝ (((S.realCFCTrim A f).comp
(S.realCFCTrim A q)) w) w := by rfl
_ = inner ℝ (S.realCFCTrim A g w) w := by rw [hfg_comp]
have hsup : ∀ x ∈ spectrum ℝ A, |g x| ≤ c := by
intro x hx
have hx0 : 0 ≤ x := Tstar_T_spectrum_nonneg S 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 Ω S.m_X (μ.trim S.m_X_le)
A hA_sa g hg_cont c hc_nonneg hsup w
have hcs : inner ℝ (S.realCFCTrim A g w) w ≤ c * ‖w‖ ^ 2 := by
have hineq : |inner ℝ (S.realCFCTrim A g w) w| ≤
‖S.realCFCTrim A g w‖ * ‖w‖ :=
abs_real_inner_le_norm _ _
calc
inner ℝ (S.realCFCTrim A g w) w
≤ |inner ℝ (S.realCFCTrim A g w) w| := le_abs_self _
_ ≤ ‖S.realCFCTrim 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.TlinTrim (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem))‖ ^ 2
= inner ℝ (S.realCFCTrim A g w) w := hTu_sq
_ ≤ c * ‖w‖ ^ 2 := hcs
_ = sc.biasConst * ‖S.primalTrimEquiv (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
Family of function-level minimisers indexed by the regularization level.
h_lambda_star_fun :
ℝ → S.𝒳 → ℝ
Every positive-level function-level minimiser lies in `Hbar`.
h_lambda_star_mem :
∀ {lambda : ℝ}
if
0 < lambda
then
h_lambda_star_fun lambda ∈ S.Hbar
Coherence: at every positive level, lifting the function-level minimiser to
`L²(σ(X))` recovers the Lax–Milgram L² minimiser.
h_lambda_star_pullback :
∀ {lambda : ℝ} (hlambda : 0 < lambda),
S.hL2 (h_lambda_star_mem hlambda) = S.tikhonovMinimiserL2 lambda
Complexification_Part2 2 core · 2 supporting This second implementation part proves that realCFC preserves self-adjointness, multiplication, and the resolvent-times-operator identity. ★ realCFC_resolvent_mul_self★ realCFC_norm_le
Algebraic and norm laws for the real functional calculus
This second implementation part proves that realCFC preserves
self-adjointness, multiplication, and the resolvent-times-operator identity.
It also supplies the spectrum comparison and norm estimate used by the NPIV
spectral bias argument.
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]
2 supporting declarations (lemmas, instances)
-
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
SpectralCalculus_Part3 1 core · 0 supporting This final spectral part converts a SpectralSourceCondition and a TikhonovPullback into the uniform TikhonovBiasBound consumed by the primal rate theorem.
Packaging spectral bias for the primal rate theorem
This final spectral part converts a SpectralSourceCondition and a
TikhonovPullback into the uniform TikhonovBiasBound consumed by the primal
rate theorem. The pullback represents the ambient minimizer by a candidate
function; it does not turn the ambient construction into candidate-subspace
minimization.
def tikhonov_bias_from_spectral reviewed
⚑ flagged
Causalean.Estimation.NPIV
For an NPIV operator system, a real source exponent, a spectral source condition, and a simultaneous pullback of the population minimisers to candidate functions, the construction returns one Tikhonov bias certificate whose constant is uniform over every positive regularization level.
Definition (Lean source)
parameters
def
given by
by refine { 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 := ?_ } · intro lambda lambda_pos have hb := sc.strong_bias lambda_pos have hpull := pb.h_lambda_star_pullback lambda_pos have hC : sc.biasConst * ‖S.primalTrimEquiv (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 [S.primalTrimEquiv.norm_map, OperatorSystem.strongNorm, sq] ring rw [OperatorSystem.strongNorm, hpull] calc ‖S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem‖ ^ 2 = ‖S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem)‖ ^ 2 := by rw [S.primalTrimEquiv.norm_map] _ = ‖S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem)‖ ^ 2 := by rw [map_sub] _ ≤ sc.biasConst * ‖S.primalTrimEquiv (S.hL2 sc.w₀_mem)‖ ^ 2 * lambda ^ (min β 2) := hb _ = sc.biasConst * ‖S.hL2 sc.w₀_mem‖ * S.strongNorm (S.hL2 sc.w₀_mem) * lambda ^ (min β 2) := hC · intro lambda lambda_pos have hb := sc.weak_bias lambda_pos have hpull := pb.h_lambda_star_pullback lambda_pos have hC : sc.biasConst * ‖S.primalTrimEquiv (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 [S.primalTrimEquiv.norm_map, OperatorSystem.strongNorm, sq] ring rw [OperatorSystem.weakNorm, OperatorSystem.strongNorm, hpull] change ‖S.Tlin (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem)‖ ^ 2 ≤ _ calc ‖S.Tlin (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem)‖ ^ 2 = ‖S.TlinTrim (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda - S.hL2 S.h₀_mem))‖ ^ 2 := by simp [OperatorSystem.TlinTrim] _ = ‖S.TlinTrim (S.primalTrimEquiv (S.tikhonovMinimiserL2 lambda) - S.primalTrimEquiv (S.hL2 S.h₀_mem))‖ ^ 2 := by rw [map_sub] _ ≤ sc.biasConst * ‖S.primalTrimEquiv (S.hL2 sc.w₀_mem)‖ ^ 2 * lambda ^ (min (β + 1) 2) := hb _ = sc.biasConst * ‖S.hL2 sc.w₀_mem‖ * ‖S.hL2 sc.w₀_mem‖ * lambda ^ (min (β + 1) 2) := hC · intro lambda lambda_pos h hh have hconv := S.tikhonovMinimiserL2_strong_convexity (lambda_pos := lambda_pos) (h := S.hL2 hh) change lambda * ‖S.hL2 hh - S.hL2 (pb.h_lambda_star_mem lambda_pos)‖ ^ 2
+ ‖S.Tlin (S.hL2 hh - S.hL2 (pb.h_lambda_star_mem lambda_pos))‖ ^ 2
≤ ‖S.Tlin (S.hL2 hh - S.hL2 S.h₀_mem)‖ ^ 2
- ‖S.Tlin (S.hL2 (pb.h_lambda_star_mem lambda_pos) - S.hL2 S.h₀_mem)‖ ^ 2
+ lambda * (‖S.hL2 hh‖ ^ 2 - ‖S.hL2 (pb.h_lambda_star_mem lambda_pos)‖ ^ 2) rw [pb.h_lambda_star_pullback lambda_pos] exact hconv