production module
AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation
Read the mathematical statements and proofs in order
1 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Analysis/HilbertCorrectorPerturbation.lean.
Declarations
theorem AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation.quadratic_corrector_perturbation Partial Not mapped
Read the complete mathematical statement and proof, with Lean below each
No declaration docstring.
theorem quadratic_corrector_perturbation
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
[CompleteSpace H]
(A G Inv : H →L[ℝ] H)
(hA : IsSelfAdjoint A) (hG : IsSelfAdjoint G)
(hInv : IsSelfAdjoint Inv) (hAInv : Commute A Inv)
(hInvG : Inv * G = 1) (hGInv : G * Inv = 1)
(hSquares : A * A + G * G = 1)
(u v r : H) :
let C : H → H → ℝ := fun u v =>
(‖u‖^2 - ‖v‖^2)/2 - inner ℝ (A (Inv u)) v
C (u + G r) (v - A r) - C u v =
inner ℝ u (Inv r) + ‖r‖^2/2
:= by
dsimp only
have ha (x y : H) : inner ℝ (A x) y=inner ℝ x (A y) := hA.isSymmetric x y
have hg (x y : H) : inner ℝ (G x) y=inner ℝ x (G y) := hG.isSymmetric x y
have hi (x y : H) : inner ℝ (Inv x) y=inner ℝ x (Inv y) := hInv.isSymmetric x y
have hIG (x : H) : Inv (G x)=x := by
have h := congrArg (fun L : H →L[ℝ] H => L x) hInvG
simpa only [ContinuousLinearMap.mul_apply,ContinuousLinearMap.one_apply] using h
have hSq (x : H) : A (A x)+G (G x)=x := by
have h := congrArg (fun L : H →L[ℝ] H => L x) hSquares
simpa only [ContinuousLinearMap.add_apply,ContinuousLinearMap.mul_apply,
ContinuousLinearMap.one_apply] using h
have hEnergy (x : H) : ‖A x‖^2+‖G x‖^2=‖x‖^2 := by
have h := congrArg (fun z : H => inner ℝ z x) (hSq x)
rw [inner_add_left,ha (A x) x,hg (G x) x] at h
simpa only [real_inner_self_eq_norm_sq] using h
have hLinear (x : H) : Inv (A (A x))+G x=Inv x := by
calc
Inv (A (A x))+G x=Inv (A (A x))+Inv (G (G x)) := by rw [hIG]
_ = Inv (A (A x)+G (G x)) := by rw [map_add]
_ = Inv x := congrArg Inv (hSq x)
have hMixed : inner ℝ (A (Inv u)) (A r)+inner ℝ u (G r)=inner ℝ u (Inv r) := by
rw [ha (Inv u) (A r),hi u (A (A r)),
← inner_add_right,hLinear r]
rw [norm_add_sq_real,norm_sub_sq_real]
simp only [map_add,hIG,inner_add_left,inner_sub_right,real_inner_self_eq_norm_sq]
rw [real_inner_comm v (A r)]
nlinarith only [hEnergy r,hMixed]
end
end AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation
-- Source excerpt truncated; follow the exact source link.AutoSamplingTheory/TechnicalLemmas/Analysis/HilbertCorrectorPerturbation.lean:9published source at ed709a7f320dOpen detailed card
Excerpt truncated; the exact source link is authoritative.
Complete Lean source
AutoSamplingTheory/TechnicalLemmas/Analysis/HilbertCorrectorPerturbation.lean — full module with imports and context
import Mathlib.Analysis.InnerProductSpace.Adjoint
import Mathlib.Tactic.Linarith
namespace AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation
noncomputable section
open scoped RealInnerProductSpace
set_option autoImplicit false
theorem quadratic_corrector_perturbation
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
[CompleteSpace H]
(A G Inv : H →L[ℝ] H)
(hA : IsSelfAdjoint A) (hG : IsSelfAdjoint G)
(hInv : IsSelfAdjoint Inv) (hAInv : Commute A Inv)
(hInvG : Inv * G = 1) (hGInv : G * Inv = 1)
(hSquares : A * A + G * G = 1)
(u v r : H) :
let C : H → H → ℝ := fun u v =>
(‖u‖^2 - ‖v‖^2)/2 - inner ℝ (A (Inv u)) v
C (u + G r) (v - A r) - C u v =
inner ℝ u (Inv r) + ‖r‖^2/2
:= by
dsimp only
have ha (x y : H) : inner ℝ (A x) y=inner ℝ x (A y) := hA.isSymmetric x y
have hg (x y : H) : inner ℝ (G x) y=inner ℝ x (G y) := hG.isSymmetric x y
have hi (x y : H) : inner ℝ (Inv x) y=inner ℝ x (Inv y) := hInv.isSymmetric x y
have hIG (x : H) : Inv (G x)=x := by
have h := congrArg (fun L : H →L[ℝ] H => L x) hInvG
simpa only [ContinuousLinearMap.mul_apply,ContinuousLinearMap.one_apply] using h
have hSq (x : H) : A (A x)+G (G x)=x := by
have h := congrArg (fun L : H →L[ℝ] H => L x) hSquares
simpa only [ContinuousLinearMap.add_apply,ContinuousLinearMap.mul_apply,
ContinuousLinearMap.one_apply] using h
have hEnergy (x : H) : ‖A x‖^2+‖G x‖^2=‖x‖^2 := by
have h := congrArg (fun z : H => inner ℝ z x) (hSq x)
rw [inner_add_left,ha (A x) x,hg (G x) x] at h
simpa only [real_inner_self_eq_norm_sq] using h
have hLinear (x : H) : Inv (A (A x))+G x=Inv x := by
calc
Inv (A (A x))+G x=Inv (A (A x))+Inv (G (G x)) := by rw [hIG]
_ = Inv (A (A x)+G (G x)) := by rw [map_add]
_ = Inv x := congrArg Inv (hSq x)
have hMixed : inner ℝ (A (Inv u)) (A r)+inner ℝ u (G r)=inner ℝ u (Inv r) := by
rw [ha (Inv u) (A r),hi u (A (A r)),
← inner_add_right,hLinear r]
rw [norm_add_sq_real,norm_sub_sq_real]
simp only [map_add,hIG,inner_add_left,inner_sub_right,real_inner_self_eq_norm_sq]
rw [real_inner_comm v (A r)]
nlinarith only [hEnergy r,hMixed]
end
end AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation
#print axioms AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation.quadratic_corrector_perturbation