Estimation.NPIV.Operator

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

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

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 (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]

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 (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]

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 (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 (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