Final sorry + PDF Overfills

Physicslib4/Geometry/PseudoRiemannian/Basic.lean

@@ -24,9 +24,12 @@ metrics are included. The smoothness condition has the same bundle-section shape
 ## Main results
 
 * `Physicslib4.Geometry.PseudoRiemannianMetric.bijective_val`: at each point, `v ↦ g_x(v, ·)` is
-  a linear isomorphism `T_xM → T_x*M` (the musical isomorphism).
+  a linear isomorphism `T_xM → T_x*M` (the musical isomorphism), packaged as `flatEquiv`.
+* `Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm`: `x ↦ ♭_x⁻¹` is a `C^∞`
+  section of `Hom(T*M, TM)`.
 
-Blueprint reference: `def:pseudo-riemannian-metric`, `lmm:musical-isomorphism`.
+Blueprint reference: `def:pseudo-riemannian-metric`, `lmm:musical-isomorphism`,
+`lmm:musical-inverse-smooth`.
 -/
 
 open Bundle
@@ -78,6 +81,59 @@ theorem bijective_val [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M)
     exact (Subspace.dual_finrank_eq).symm
   exact ⟨hinj, (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hrank).1 hinj⟩
 
+/-- The musical isomorphism `♭_x : T_xM ≃ T_x*M`, `v ↦ g_x(v, ·)`, as a continuous linear
+equivalence (`bijective_val`; continuity of the inverse is automatic in finite dimension).
+
+Blueprint reference: `lmm:musical-isomorphism`. -/
+noncomputable def flatEquiv [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) (x : M) :
+    TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
+  haveI : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E)
+  (LinearEquiv.ofBijective (g.val x : TangentSpace I x →ₗ[ℝ] (TangentSpace I x →L[ℝ] ℝ))
+    (g.bijective_val x)).toContinuousLinearEquiv
+
+theorem flatEquiv_apply [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) (x : M)
+    (v : TangentSpace I x) : g.flatEquiv x v = g.val x v :=
+  rfl
+
+/-- **Smoothness of the inverse musical isomorphism.** The map `x ↦ ♭_x⁻¹` is a `C^∞` section of
+the bundle `Hom(T*M, TM)`, whose fibre at `x` is `T_x*M →L[ℝ] T_xM`, stated in the same
+bundle-section idiom as the smoothness of `g` itself.
+
+Blueprint reference: `lmm:musical-inverse-smooth`. -/
+theorem contMDiff_flatEquiv_symm [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) :
+    ContMDiff I (I.prod 𝓘(ℝ, (E →L[ℝ] ℝ) →L[ℝ] E)) ∞
+      (fun x ↦ TotalSpace.mk' ((E →L[ℝ] ℝ) →L[ℝ] E)
+        (E := fun x ↦ (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x) x
+        ((g.flatEquiv x).symm : (TangentSpace I x →L[ℝ] ℝ) →L[ℝ] TangentSpace I x)) := by
+  intro x₀
+  rw [contMDiffAt_hom_bundle]
+  refine ⟨contMDiffAt_id, ?_⟩
+  have hg := (contMDiffAt_hom_bundle _).1 (g.contMDiff x₀) |>.2
+  simp only at hg ⊢
+  have h₁ : x₀ ∈ (trivializationAt E (TangentSpace I) x₀).baseSet :=
+    FiberBundle.mem_baseSet_trivializationAt' x₀
+  have h₂ : x₀ ∈ (trivializationAt (E →L[ℝ] ℝ)
+      (fun x ↦ TangentSpace I x →L[ℝ] ℝ) x₀).baseSet :=
+    FiberBundle.mem_baseSet_trivializationAt' x₀
+  have hinv := (ContinuousLinearMap.IsInvertible.contDiffAt_map_inverse (𝕜 := ℝ) (n := ∞)
+    (e := ContinuousLinearMap.inCoordinates E (TangentSpace I)
+      (E →L[ℝ] ℝ) (fun x ↦ TangentSpace I x →L[ℝ] ℝ) x₀ x₀ x₀ x₀ (g.val x₀)) ?_).contMDiffAt
+  · refine (hinv.comp x₀ hg).congr_of_eventuallyEq ?_
+    filter_upwards [(trivializationAt _ _ x₀).open_baseSet.mem_nhds h₁,
+      (trivializationAt _ _ x₀).open_baseSet.mem_nhds h₂] with x hx hx'
+    simp only [Function.comp_apply]
+    rw [ContinuousLinearMap.inCoordinates_eq hx hx', ContinuousLinearMap.inCoordinates_eq hx' hx]
+    change _ = ContinuousLinearMap.inverse
+      (_ ∘L ((g.flatEquiv x : TangentSpace I x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ)) ∘L _))
+    simp only [ContinuousLinearMap.inverse_equiv_comp, ContinuousLinearMap.inverse_comp_equiv,
+      ContinuousLinearMap.inverse_equiv, ContinuousLinearEquiv.symm_symm]
+    rfl
+  · rw [ContinuousLinearMap.inCoordinates_eq h₁ h₂]
+    change ContinuousLinearMap.IsInvertible
+      (_ ∘L ((g.flatEquiv x₀ : TangentSpace I x₀ →L[ℝ] (TangentSpace I x₀ →L[ℝ] ℝ)) ∘L _))
+    exact ContinuousLinearMap.isInvertible_equiv.comp
+      (ContinuousLinearMap.isInvertible_equiv.comp ContinuousLinearMap.isInvertible_equiv)
+
 end PseudoRiemannianMetric
 
 end Geometry

Physicslib4/Geometry/PseudoRiemannian/LeviCivita.lean

@@ -143,18 +143,6 @@ each point, and the musical isomorphism `flatEquiv` turns it into the desired `
 
 variable (g : PseudoRiemannianMetric I M)
 
-/-- The **musical isomorphism** `v ↦ g_x(v, ·)` as a continuous linear equivalence
-(`bijective_val`).
-
-Blueprint reference: `lmm:musical-isomorphism`. -/
-noncomputable def flatEquiv (x : M) :
-    TangentSpace I x ≃L[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
-  haveI : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E)
-  (LinearEquiv.ofBijective (g.val x : TangentSpace I x →ₗ[ℝ] TangentSpace I x →L[ℝ] ℝ)
-    (g.bijective_val x)).toContinuousLinearEquiv
-
-theorem flatEquiv_apply (x : M) (v : TangentSpace I x) : g.flatEquiv x v = g.val x v := rfl
-
 variable {X Y Z : Π x : M, TangentSpace I x}
 
 variable (X Y Z) in

blueprint/src/macros/print.tex

@@ -26,4 +26,22 @@
 \NewDocumentCommand{\proves}{m}
  {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}%
   \ignorespaces}
-\ExplSyntaxOff
+\ExplSyntaxOff
+% Line breaking for long Lean names and paths (pdf only). Lean identifiers such as
+% `Physicslib4.Spectral.Stone.isEssentiallySelfAdjoint_generator` are set with \texttt,
+% which TeX never breaks, so they overflow the margin. Allow a break after each `.`, `_`
+% and `/` inside \texttt, and give TeX extra stretch before it resorts to an overfull line.
+\NewCommandCopy{\bpOrigTexttt}{\texttt}
+\ExplSyntaxOn
+\tl_new:N \l__bp_texttt_tl
+\RenewDocumentCommand{\texttt}{m}
+ {
+  \tl_set:Nn \l__bp_texttt_tl {#1}
+  \tl_replace_all:Nnn \l__bp_texttt_tl {\_} {\_\allowbreak}
+  \tl_replace_all:Nnn \l__bp_texttt_tl {.} {.\allowbreak}
+  \tl_replace_all:Nnn \l__bp_texttt_tl {/} {/\allowbreak}
+  \exp_args:NV \bpOrigTexttt \l__bp_texttt_tl
+ }
+\ExplSyntaxOff
+\setlength{\emergencystretch}{3em}
+\tolerance=2000

blueprint/src/move

@@ -0,0 +1,29 @@
+git mv sections/sec1/1-1_original_haag_kastler_axioms.tex sections/sec1/original-haag-kastler-axioms.tex
+git mv sections/sec10/10-1_gns-construction-details.tex sections/sec10/gns-construction-details.tex
+git mv sections/sec10/10-2_spacetime.tex sections/sec10/spacetime.tex
+git mv sections/sec10/10-3_haag-kastler-axioms.tex sections/sec10/haag-kastler-axioms.tex
+git mv sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex
+git mv sections/sec10/10-5_general-covariance-in-curved-spacetime.tex sections/sec10/general-covariance-in-curved-spacetime.tex
+git mv sections/sec2/2-1_standard_topology_on_minkowski_space.tex sections/sec2/standard-topology-on-minkowski-space.tex
+git mv sections/sec2/2-2_indiscrete_topology_on_minkowski_space.tex sections/sec2/indiscrete-topology-on-minkowski-space.tex
+git mv sections/sec2/2-3_euclidean_topology_on_minkowski_space.tex sections/sec2/euclidean-topology-on-minkowski-space.tex
+git mv sections/sec2/2-4_alexandrov_topology_on_minkowski_space.tex sections/sec2/alexandrov-topology-on-minkowski-space.tex
+git mv sections/sec3/3-1_regions_of_measurement.tex sections/sec3/regions-of-measurement.tex
+git mv sections/sec4/4-1_gns_construction.tex sections/sec4/gns-construction.tex
+git mv sections/sec4/4-2_isotony.tex sections/sec4/isotony.tex
+git mv sections/sec4/4-3_common_unit.tex sections/sec4/common-unit.tex
+git mv sections/sec5/5-1_completely_spacelike.tex sections/sec5/completely-spacelike.tex
+git mv sections/sec5/5-2_quasilocal_algebra.tex sections/sec5/quasilocal-algebra.tex
+git mv sections/sec6/6-1_set_theoretic_union.tex sections/sec6/set-theoretic-union.tex
+git mv sections/sec6/6-2_completion_of_the_set_theoretic_union.tex sections/sec6/completion-of-the-set-theoretic-union.tex
+git mv sections/sec6/6-3_all_observables_of_interest.tex sections/sec6/all-observables-of-interest.tex
+git mv sections/sec7/7-1_inhomogeneous_lorentz_group.tex sections/sec7/inhomogeneous-lorentz-group.tex
+git mv sections/sec7/7-2_action_of_the_inhomogeneous_lorentz_groups_identity_component.tex sections/sec7/action-of-the-inhomogeneous-lorentz-groups-identity-component.tex
+git mv sections/sec8/8-1_faithful_representations.tex sections/sec8/faithful-representations.tex
+git mv sections/sec8/8-2_faithful_and_irreducible_representations.tex sections/sec8/faithful-and-irreducible-representations.tex
+git mv sections/sec9/9-1_prologue.tex sections/sec9/prologue.tex
+git mv sections/sec9/9-2_axiom_1_local_algebras.tex sections/sec9/axiom-1-local-algebras.tex
+git mv sections/sec9/9-3_axiom_2_isotony.tex sections/sec9/axiom-2-isotony.tex
+git mv sections/sec9/9-4_axiom_3_local_commutativity.tex sections/sec9/axiom-3-local-commutativity.tex
+git mv sections/sec9/9-4_axiom_4_local_algebra.tex sections/sec9/axiom-4-local-algebra.tex
+git mv sections/sec9/9-5_axiom_5_isometric_covariance.tex sections/sec9/axiom-5-isometric-covariance.tex

blueprint/src/sections/sec10/haag-kastler-axioms-in-curved-spacetime.tex

@@ -267,7 +267,7 @@ \subsection{Local von Neumann Algebras in Curved Spacetime}
 \begin{proof}
     \leanok
     \uses{def:spacelike-complement, thrm:additive-free-locality, thrm:von-neumann-bundled-order-in-curved-spacetime}
-    The Galois bridge discharges the spacelike hypothesis, and $L.\mathtt{toAbstractIdentityComponent}$ identifies the concrete and abstract spacelike relations.
+    The Galois bridge discharges the spacelike hypothesis, and \texttt{L.toAbstractIdentityComponent} identifies the concrete and abstract spacelike relations.
 \end{proof}
 
 \begin{theorem}[Geometric Covariance of the von Neumann Net (Curved Spacetime)]

blueprint/src/sections/sec10/spacetime.tex

@@ -8,7 +8,8 @@ \section{Spacetime}\label{sctn:spacetime}
 
     \emph{The smoothness clause, precisely.} The metric field is a family of \emph{continuous bilinear forms} $g_x : TM|_x \to_L[\mathbb{R}] TM|_x \to_L[\mathbb{R}] \mathbb{R}$, and ``smooth'' is the field \texttt{contMDiff}, which asserts that $g$ is a $C^\infty$ \emph{section of the bundle of continuous bilinear forms on the tangent bundle} --- the regularity index being $\infty$, on which see the remark on the index below. Writing $E$ for the model space and $I$ for the model with corners of $M$, it reads
     \begin{align}
-        \mathtt{ContMDiff}\;I\;\Big(I.\mathtt{prod}\;\mathcal{I}\big(\mathbb{R},\, E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\Big)\;\infty\;\Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\;\big(E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\;x\;(g_x)\Big),
+        &\mathtt{ContMDiff}\;I\;\Big(I.\mathtt{prod}\;\mathcal{I}\big(\mathbb{R},\, E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\Big)\;\infty \notag \\
+        &\qquad \Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\;\big(E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\;x\;(g_x)\Big),
     \end{align}
     the fibre over $x$ being $TM|_x \to_L[\mathbb{R}] TM|_x \to_L[\mathbb{R}] \mathbb{R}$ and the index being $\infty$.
 
@@ -18,7 +19,8 @@ \section{Spacetime}\label{sctn:spacetime}
 
     \emph{It is Mathlib's idiom.} The clause is deliberately the shape of the \texttt{contMDiff} field of Mathlib's \texttt{Bundle.ContMDiffRiemannianMetric}, whose own field is
     \begin{align}
-        \mathtt{ContMDiff}\;I_B\;\big(I_B.\mathtt{prod}\;\mathcal{I}(\mathbb{R}, F \to_L[\mathbb{R}] F \to_L[\mathbb{R}] \mathbb{R})\big)\;n\;\big(b \mapsto \mathtt{TotalSpace.mk'}\;(F \to_L[\mathbb{R}] F \to_L[\mathbb{R}] \mathbb{R})\;b\;(\mathtt{inner}\;b)\big),
+        &\mathtt{ContMDiff}\;I_B\;\big(I_B.\mathtt{prod}\;\mathcal{I}(\mathbb{R}, F \to_L[\mathbb{R}] F \to_L[\mathbb{R}] \mathbb{R})\big)\;n \notag \\
+        &\qquad \big(b \mapsto \mathtt{TotalSpace.mk'}\;(F \to_L[\mathbb{R}] F \to_L[\mathbb{R}] \mathbb{R})\;b\;(\mathtt{inner}\;b)\big),
     \end{align}
     read with $\mathtt{inner}$ replaced by $g$. Matching it verbatim is what makes the whole bundle-section API of \texttt{Mathlib/Geometry/Manifold/VectorBundle/} apply to $g$ without translation.
 
@@ -385,10 +387,13 @@ \section{Spacetime}\label{sctn:spacetime}
 
 \begin{lemma}[Smoothness of the Inverse Musical Isomorphism]
     \label{lmm:musical-inverse-smooth}
+    \lean{Physicslib4.Geometry.PseudoRiemannianMetric.contMDiff_flatEquiv_symm, Physicslib4.Geometry.PseudoRiemannianMetric.flatEquiv}
     \uses{lmm:musical-isomorphism}
+    \leanok
     The map $x \mapsto \flat_x^{-1}$ of \ref{lmm:musical-isomorphism} is smooth: it is a $C^\infty$ section of the bundle $\mathrm{Hom}(T^*M, TM)$.
 \end{lemma}
 \begin{proof}
+    \leanok
     \uses{lmm:musical-isomorphism, def:pseudo-riemannian-metric}
     Work in a local trivialisation of the bundle of bilinear forms: there $x \mapsto \flat_x$ is a $C^\infty$ map into the invertible elements of $E \to_L E^*$ by the smoothness clause of $g$, and inversion of continuous linear equivalences is $C^\infty$ (\texttt{contDiffAt\_map\_inverse}), so the composite $x \mapsto \flat_x^{-1}$ is $C^\infty$ in each trivialisation.
 \end{proof}
@@ -400,7 +405,8 @@ \section{Spacetime}\label{sctn:spacetime}
     \leanok
     Let $\nabla$ be a Levi-Civita connection of $g$. For every $x \in M$ and all vector fields $X, Y, Z$ differentiable at $x$,
     \begin{align}
-        2\,g\big(\nabla_X Y, Z\big) = X\,g(Y,Z) + Y\,g(X,Z) - Z\,g(X,Y) + g\big([X,Y],Z\big) - g\big([X,Z],Y\big) - g\big([Y,Z],X\big),
+        2\,g\big(\nabla_X Y, Z\big) &= X\,g(Y,Z) + Y\,g(X,Z) - Z\,g(X,Y) \notag \\
+        &\qquad + g\big([X,Y],Z\big) - g\big([X,Z],Y\big) - g\big([Y,Z],X\big),
     \end{align}
     both sides evaluated at $x$.
 \end{lemma}
@@ -1653,7 +1659,8 @@ \subsection{Pullback metrics and cross-metric isometries}
 
     The chain rule to cite is \texttt{mfderiv\_comp\_apply\_of\_eq}, \emph{not} \texttt{mfderiv\_comp} (nor its \texttt{\_apply} form). Its exact shape is
     \begin{align}
-        \big(hg : \mathtt{MDifferentiableAt}\;f\text{'s target model}\;g\;y\big) \to \big(hf : \mathtt{MDifferentiableAt}\;f\;x\big) \to \big(hy : f\,x = y\big) \to \mathtt{mfderiv}\,(g \circ f)\,x\,v = \mathtt{mfderiv}\,g\,y\,\big(\mathtt{mfderiv}\,f\,x\,v\big),
+        &\big(hg : \mathtt{MDifferentiableAt}\;f\text{'s target model}\;g\;y\big) \to \big(hf : \mathtt{MDifferentiableAt}\;f\;x\big) \notag \\
+        &\qquad \to \big(hy : f\,x = y\big) \to \mathtt{mfderiv}\,(g \circ f)\,x\,v = \mathtt{mfderiv}\,g\,y\,\big(\mathtt{mfderiv}\,f\,x\,v\big),
     \end{align}
     and the base-point argument $hy$ is exactly what is needed here: instantiated at $g := \psi$, $f := \psi.\mathtt{symm}$, base point $\psi(x)$ and $y := x$, it requires $hy : \psi.\mathtt{symm}(\psi\,x) = x$, which is \texttt{Diffeomorph.symm\_apply\_apply}. Without that transport the plain \texttt{mfderiv\_comp} produces the outer factor as $\mathtt{mfderiv}\;\psi\;\big(\psi.\mathtt{symm}(\psi\,x)\big)$, whose value lives in the tangent space at $\psi(\psi.\mathtt{symm}(\psi\,x))$ rather than at $\psi(x)$; those two tangent spaces are propositionally but not definitionally identified, so the composition does not typecheck until the base point has been transported. The \texttt{\_of\_eq} variant is the lemma that takes the transport as an argument and states its conclusion at $y$.
 
@@ -1745,7 +1752,8 @@ \subsection{Pullback metrics and cross-metric isometries}
     \leanok
     The assignment $x \mapsto (\psi^*g)_x$ of \ref{def:pullback-metric} satisfies the \texttt{contMDiff} field of \ref{def:spacetime}: it is a section of the bundle of continuous bilinear forms on the tangent bundle of regularity index $\infty$, i.e.\ a $C^\infty$ section,
     \begin{align}
-        \mathtt{ContMDiff}\;I\;\Big(I.\mathtt{prod}\;\mathcal{I}\big(\mathbb{R},\, E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\Big)\;\infty\;\Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\;\big(E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\;x\;\big((\psi^*g)_x\big)\Big).
+        &\mathtt{ContMDiff}\;I\;\Big(I.\mathtt{prod}\;\mathcal{I}\big(\mathbb{R},\, E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\Big)\;\infty \notag \\
+        &\qquad \Big(x \mapsto \mathtt{Bundle.TotalSpace.mk'}\;\big(E \to_L[\mathbb{R}] E \to_L[\mathbb{R}] \mathbb{R}\big)\;x\;\big((\psi^*g)_x\big)\Big).
     \end{align}
     The index is $\infty$: that is what \ref{def:spacetime} demands.
 
@@ -1984,7 +1992,8 @@ \subsection{Pullback metrics and cross-metric isometries}
     \leanok
     This is \texttt{mfderivWithin\_comp} for the composite of $\mu$ with $\psi$. Write $P$ for the parameter space of $\mu$ (the inner set), $u$ for the outer set, and keep $s \in P$ for the parameter of the statement; the set and the point must be kept notationally apart, since \texttt{mfderivWithin\_comp} takes both. With that convention its exact hypotheses are
     \begin{align}
-        hg &: \mathtt{MDifferentiableWithinAt}\;I'\;I''\;\psi\;u\;(\mu(s)), \qquad hf : \mathtt{MDifferentiableWithinAt}\;I\;I'\;\mu\;P\;s, \\
+        hg &: \mathtt{MDifferentiableWithinAt}\;I'\;I''\;\psi\;u\;(\mu(s)), \\
+        hf &: \mathtt{MDifferentiableWithinAt}\;I\;I'\;\mu\;P\;s, \\
         h &: P \subseteq \mu^{-1}(u), \qquad hxs : \mathtt{UniqueMDiffWithinAt}\;I\;P\;s,
     \end{align}
     of which two are easy to overlook. The uniqueness hypothesis is \emph{pointwise} --- a $\mathtt{UniqueMDiffWithinAt}$ at the single parameter $s$, not a $\mathtt{UniqueMDiffOn}$ on the whole of $P$ --- so what \ref{lmm:path-parameter-unique-diff} supplies must be specialised to $s$ and converted, as $(\dots\,s\,hs).\mathtt{uniqueMDiffWithinAt}$. And there is a set side condition $P \subseteq \mu^{-1}(u)$ relating the inner set to the outer one; here $u = \mathtt{univ}$, so it is immediate, and correspondingly the outer derivative is an unrestricted \texttt{mfderiv} obtained by \texttt{mfderivWithin\_univ}. Differentiability of $\mu$ within $P$ comes from its smoothness, and differentiability of $\psi$ from \texttt{Diffeomorph.mdifferentiable} (with side condition $n \neq 0$), which is what the repository template cited below actually uses --- not from \ref{lmm:mfderiv-diffeo-linear-equiv}, which delivers a \texttt{ContinuousLinearEquiv} rather than an $\mathtt{MDifferentiableWithinAt}$ hypothesis.

blueprint/src/sections/sec10/spectral-theorems.tex

@@ -4596,8 +4596,10 @@ \subsubsection{Spectral Theorem for Bounded Self-Adjoint Operators}
     \leanok
     Let $A \in \mathcal{B}(\mathbf{H})$ be self-adjoint, and let $f \mapsto f(A)$ be the bounded Borel functional calculus of Definition~\ref{def:hall-8.8}. Write
     \begin{align}
-        \mathcal{F}_1 &\equiv \{ f \text{ bounded, Borel-measurable on } \sigma(A) \mid (fg)(A) = f(A)g(A) \text{ for all } g \in C^0(\sigma(A); \mathbb{R}) \}, \\
-        \mathcal{F}_2 &\equiv \{ g \text{ bounded, Borel-measurable on } \sigma(A) \mid (fg)(A) = f(A)g(A) \text{ for all bounded, Borel-measurable } f \}.
+        \mathcal{F}_1 &\equiv \{ f \text{ bounded, Borel-measurable on } \sigma(A) \mid \notag \\
+            &\qquad (fg)(A) = f(A)g(A) \text{ for all } g \in C^0(\sigma(A); \mathbb{R}) \}, \\
+        \mathcal{F}_2 &\equiv \{ g \text{ bounded, Borel-measurable on } \sigma(A) \mid \notag \\
+            &\qquad (fg)(A) = f(A)g(A) \text{ for all bounded, Borel-measurable } f \}.
     \end{align}
     These are distinct from the class $\mathcal{F}$ of Definition~\ref{def:F-class}: the subscripted classes concern \textit{multiplicativity} of the functional calculus, not boundedness of a quadratic form.
 \end{definition}