The Lean 4 theorem `friedrichs_bounded_nontrivial_example` in the `ChapterYangMillsFriedrichsLimit` chapter of the timepiece formalization
ProvedBookProof.YangMillsFriedrichsLimit.friedrichs_bounded_nontrivial_exampletimepiece
The Lean 4 theorem friedrichs_bounded_nontrivial_example in the ChapterYangMillsFriedrichsLimit chapter of the timepiece formalization.
Preamble
-- Generated from ChapterYangMillsFriedrichsLimit.lean — theorem BookProof.YangMillsFriedrichsLimit.friedrichs_bounded_nontrivial_example
import Mathlib
import Definitions.Def_ChapterYangMillsFriedrichsLimit
open BookProof.YangMillsFriedrichsLimit
open BookProof.FarisLavine BookProof.YangMillsFriedrichs
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]Formal statement
theorem BookProof.YangMillsFriedrichsLimit.friedrichs_bounded_nontrivial_example [CompleteSpace F] (D : Submodule ℂ F)
(hdense : Dense (D : Set F)) :
∃ A : F →L[ℂ] F, (∀ x : D, A (x : F) = D.subtype x) ∧
IsPositiveSelfAdjointExtension (D.subtype) (topRestrict A) := by sorrySource