6 Ricci flow on a closed manifold
Everything from here on is blocked on analysis Mathlib does not have. It is stated so the dependency graph is honest, not because it is close. The point of writing it out is to see where the road forks and how much of it a given target actually requires.
A family \(g(t)\) of metrics with \(\partial _t g= -2\operatorname {Ric}(g)\).
Defined. Stated per time slice: at each \(t\) there is a \(C^1\) torsion-free metric-compatible connection whose Ricci curvature gives the rate of change of \(g\). By Theorem 11 this is a statement about \(g(t)\) alone, and Lemma 41 makes that explicit. \(\forall t\, \exists \nabla \) collapses to a family by choice, since no regularity in \(t\) is demanded of the connection. With the function \(g\mapsto \operatorname {Ric}(g)\) of Definition 13, the existential disappears altogether: Lemma 42 is the textbook equation.
The definition is on an interval rather than all of \(\mathbb {R}\): flows live on intervals, and short-time existence cannot be stated otherwise.
A constant family is a Ricci flow at \(t\) if and only if its Levi-Civita connection is Ricci-flat.
Uniqueness of derivatives against \(\partial _t(\text{const}) = 0\), in both directions. Proved — and it is the check that Definition 39 has content rather than being vacuously satisfiable.
For any \(C^1\) Levi-Civita connection \(\nabla \) of \(g(t)\), the family \(g\) is a Ricci flow at \(t\) if and only if \(\partial _t g(t)(X, Y) = -2\operatorname {Ric}_{\nabla }(X, Y)\) for all \(C^2\) fields \(X, Y\).
One direction is the witness. For the other, the witness \(\nabla '\) of the existential and the given \(\nabla \) have the same \(\operatorname {Ric}\) on \(C^2\) fields by Theorem 11.
\(g\) is a Ricci flow on \(s\) if and only if \(\partial _t g(t)(X, Y) = -2\operatorname {Ric}(g(t))(X, Y)\) for all \(t \in s\) and all \(C^2\) fields \(X, Y\), with \(\operatorname {Ric}(g(t))\) the Ricci curvature of the metric \(g(t)\). No connection is quantified over: this is the textbook equation.
On a closed manifold, Ricci flow has a unique solution on a maximal interval \([0,T)\) for any smooth initial metric.
Stated as ricciFlow_shortTime_existence, via proof_wanted: every metric on a closed manifold is the initial value of a flow on some \((0,T)\), with coefficients continuous up to \(t = 0\).
Blocked. Requires quasilinear parabolic systems on sections of vector bundles (via DeTurck’s trick, or Nash–Moser in Hamilton’s original), and hence Sobolev spaces of bundle sections and elliptic regularity. None of this exists in Mathlib. This is the single largest missing prerequisite on the whole road, and it is shared by every node below.
\(\nabla ^2_{X,Y} Z = \nabla _X \nabla _Y Z - \nabla _{\nabla _X Y} Z\), and for a function \(\nabla ^2 f(X,Y) = X(Yf) - (\nabla _X Y)f\). Both are tensorial in \(X\) and \(Y\) (tensorialAt_hessian_fst/snd), so the Hessian of a \(C^2\) field at a point is a bilinear map on \(T_xM\) (hessianAt).
For a torsion-free connection, \(\nabla ^2_{X,Y} Z - \nabla ^2_{Y,X} Z = R(X,Y)Z\), and the Hessian of a \(C^2\) function is symmetric (hessianFun_symm).
Expanding the definitions, the difference is \(R(X,Y)Z + \nabla _{[X,Y]}Z - \nabla _{\nabla _X Y - \nabla _Y X} Z\), and torsion-freeness kills the last two terms. For functions the antisymmetric part is \([X,Y]f - (\nabla _X Y - \nabla _Y X)f\), and \([X,Y]f = X(Yf) - Y(Xf)\) is Lemma 5.
The rough Laplacian of a \(C^2\) vector field is the metric trace of its Hessian, \(\Delta Z = \sum _i \nabla ^2_{e_i,e_i} Z\) over an orthonormal basis of \(T_xM\); it does not depend on the basis (laplacian_eq_sum, via OrthonormalBasis.sum_apply_self_eq, the statement that \(\sum _i B(e_i,e_i)\) is basis-independent for any bilinear \(B\) — and note that this holds for bilinear maps into any normed space, so no pairing against a covector is needed and the trace comes out vector-valued directly). laplacian_eq_sum_frame reads the same sum off a frame of honest vector fields, which is the form frame computations (Divergence.lean) use.
This is the operator the evolution equations below are written in, and it is what supplies the differential inequality at a spatial minimum that the abstract maximum principle 77 takes as its hypothesis; the link is the second-derivative test, Lemma 60.
For a metric connection,
and in particular \(\Delta |\sigma |^2 = 2\langle \Delta \sigma ,\sigma \rangle + 2\sum _i |\nabla _{e_i}\sigma |^2 \ \ge \ 2\langle \Delta \sigma ,\sigma \rangle \).
Proved (Bochner.lean). The pointwise statement behind it is the Hessian form,
which is metric compatibility applied twice — once to differentiate \(\langle \sigma ,\tau \rangle \) along \(Y\), once to differentiate the result along \(X\). The Hessian’s correction term \(-(\nabla _X Y)\langle \sigma ,\tau \rangle \) is what turns the two iterated derivatives into \(\nabla ^2\sigma \) and \(\nabla ^2\tau \); expanded, again by metric compatibility, it supplies exactly the two corrections needed.
The trace is taken over the frame \(\Delta \) and \(\Delta _{\text{fun}}\) are themselves defined on, the canonical extensions of the standard orthonormal basis of \(T_xM\), so no frame-independence is needed as an input, and the factor \(2\) comes from the two cross terms coinciding at \(X = Y\).
The gradient term is frame-independent on its own (sum_inner_cov_congr), and this needs neither metric compatibility nor the identity above: \((v,w) \mapsto \langle \nabla _v\sigma , \nabla _w\tau \rangle \) is a continuous bilinear form, because \(\nabla \sigma \) and \(\nabla \tau \) are continuous linear maps at each point, so its trace is basis-independent for the usual reason.
The inequality \(\Delta |\sigma |^2 \ge 2\langle \Delta \sigma ,\sigma \rangle \) is the form the maximum principle 77 consumes: the discarded term is a sum of squares.
\((\nabla _X R)(Y,Z)W\) is \(C^\infty (M)\)-linear in each of \(X\), \(Y\), \(Z\) and \(W\) separately: replacing any one of them by \(fV\) multiplies the value at \(x\) by \(f(x)\), and replacing it by a sum splits the value.
Proved (CurvatureDeriv.lean). Three different mechanisms, not one repeated.
The direction slot is the cheap one. Each of the four terms of \(\nabla R\) picks up exactly one factor of \(f(x)\), for the same reason: \(\nabla _{fX}\) is \(f\nabla _X\) on the nose, and the last three terms feed that into a slot of \(R\) in which \(R\) is already tensorial — the first two cheaply, the third by Lemma 9.
The \(Y\) and \(Z\) slots are a cancellation instead. Under \(Y \mapsto fY\) the first term picks up a Leibniz term, \(\nabla _X(f\, R(Y,Z)W) = f\nabla _X(R(Y,Z)W) + (Xf)R(Y,Z)W\), cancelled by the matching term from \(R(\nabla _X(fY),Z)W\) — so the direction slot was the easy one precisely because it has none. Applying Leibniz needs \(y \mapsto R(Y,Z)W(y)\) to be a differentiable section, which covCurvature does not require to be well defined. That is contMDiff_curvature, also proved here: a \(C^3\) triple has a \(C^1\) curvature section, the two \(\nabla \nabla \) terms by contMDiff_cov_apply twice and the bracket term by the same fed Mathlib’s ContMDiffAt.mlieBracket_vectorField. Once \(Y\) is done, covCurvature_antisymm hands over \(Z\) for nothing.
The \(W\) slot is the same cancellation with the other pairing: \(R(Y,Z)(fW) = f\, R(Y,Z)W\) as sections, so the leading \(\nabla _X\) contributes \((Xf)R(Y,Z)W\), and the last term contributes the matching one through \(\nabla _X(fW) = f\nabla _X W + (Xf)W\). It costs one derivative more of \(f\) than the others, and that is not slack: the second Leibniz term is \(R(Y,Z)\big((Xf)W\big)\), and tensoriality in \(R\)’s third slot wants its coefficient \(Xf\) to be \(C^2\), hence \(f \in C^3\). Stating this needed curvature_smul_third’, Lemma 9’s third-slot linearity restated asking of the first two slots only the \(C^1\) regularity its proof actually uses — the fields landing in them here are \(\nabla _X Y\) and \(\nabla _X Z\), which are one derivative worse than \(Y\) and \(Z\).
With all four slots, the divergence \(\operatorname {div}\operatorname {Rm}(Y,Z,W) = \sum _i \langle (\nabla _{e_i}R)(Y,Z)W, e_i \rangle \) is well defined — the trace is over the direction slot, and tensoriality is what makes the sum independent of the orthonormal frame. The divergence is what the contracted second Bianchi identity, and hence \(\Delta \operatorname {scal}\), are about.
\((\nabla _XR)(Y,Z)W\) at \(x\) depends only on the four values \(X(x)\), \(Y(x)\), \(Z(x)\), \(W(x)\). Together with Lemma 48 this makes \(\nabla R\) a genuine tensor, not merely an operator on fields.
Proved (CurvatureDeriv.lean). The direction slot was free (Definition 51). The other three are the frame-and-globalise argument of Lemma 9 one level up: expand the field in a local frame, globalise the frame fields and the coefficients, apply tensoriality, and read off that the coefficients at \(x\) depend only on the value at \(x\). Locality — the input that argument needs — is cheap in each case, because every term of \(\nabla R\) other than the leading one is \(R\) in a slot where \(R\) is already tensorial, hence pointwise; only \(\nabla _X(R(Y,Z)W)\) needs the germ.
Two asymmetries are worth recording. The \(Z\) slot is free from the \(Y\) slot by covCurvature_antisymm, as with tensoriality. And the \(W\) slot runs at one derivative higher: covCurvature_smul_fth asks its coefficient for three derivatives, so the frame fields and the coefficient functions must be globalised at \(C^3\) rather than \(C^2\), and the frame comes from IsOrthonormalFrameOn \(\ldots 3\).
Also proved here, as the first step towards \(\Delta \operatorname {Rm}\): contMDiff_curvature_two (the curvature of \(C^4\) fields is a \(C^2\) section) and contMDiff_covCurvature (\(\nabla R\) of \(C^3\) fields, \(C^4\) in the last slot, is a \(C^1\) section) — what is needed to differentiate \(\nabla R\) a second time.
one correction for each of \(\nabla R\)’s four slots, and
Defined and proved frame-independent (CurvatureLaplacian.lean).
The outer derivative slot is free, and this is where the four-slot work of Lemma 49 is cashed in: every term is either a continuous linear map evaluated at \(X(x)\), or \(\nabla R\) in a slot where it is pointwise, applied to a field whose value at \(x\) is determined by \(X(x)\). So cov2Curvature_congr_dir needs no frame argument at all.
The inner slot is the familiar cancellation — the Leibniz term of \(\nabla _X\big(f\, (\nabla _YR)(A,B)C\big)\) is matched by the one \(\nabla _X(fY) = f\nabla _X Y + (Xf)Y\) produces in the second term — and its pointwise statement is the frame-and-globalise argument once more, at \(C^3\), since the coefficient must be \(C^3\) for \((Xf)\) to be \(C^2\).
With both derivative slots pointwise and bilinear, \(\nabla ^2R\) is a continuous bilinear map \(T_xM\times T_xM\to T_xM\) and \(\Delta \operatorname {Rm}\) is its trace; frame-independence is then OrthonormalBasis.sum_apply_self_eq, which traces bilinear maps into any normed space, so the result is vector-valued directly with no pairing against a covector.
Regularity: \(X, Y, A, B\) are \(C^3\) and \(C\) is \(C^4\). The last slot is the expensive one at every level of this tower — \(C\) needs four derivatives because covCurvature_congr_fth needs \(C^3\) coefficients because curvature_smul_third needs \(C^2\) ones.
What this is for. \(\Delta \operatorname {Rm}\) is the right-hand side of Hamilton’s evolution equation \(\partial _t \operatorname {Rm}= \Delta \operatorname {Rm}+ Q(\operatorname {Rm})\), which is what carries Hamilton–Ivey pinching from the ODE (Theorem 115) to the flow. The geometry side of that equation is now in place; the analytic side, \(\partial _t\operatorname {Rm}\), still lives on the model space (CurvatureVariation.lean).
the trace of \(\nabla R\) over its direction slot against its fourth.
Defined and proved frame-independent (Divergence.lean). Two facts make this well posed, and neither is free.
First, \((\nabla _XR)(Y,Z)W\) at \(x\) depends only on \(X(x)\) (covCurvature_congr_dir). This costs no new frame argument, unlike Lemma 9: each of the four terms is separately pointwise in \(X\). The first is a continuous linear map evaluated at \(X(x)\); the next two are \(R\) in a slot where it is tensorial, applied to \(\nabla _X Y\) and \(\nabla _X Z\), whose values at \(x\) are \(\nabla _{X(x)}Y\) and \(\nabla _{X(x)}Z\); the last is \(R\)’s third slot applied to \(\nabla _X W\), which is Lemma 9 itself.
Second, it is \(C^\infty (M)\)-linear there (Lemma 48). So \(v \mapsto (\nabla _vR)(Y,Z)W\) is a genuine endomorphism of \(T_xM\) — covCurvatureEndo, built on globally \(C^2\) extensions of \(v\) as ricciAt is — and \(\operatorname {div}\operatorname {Rm}\) is its trace.
Frame-independence is then algebraic, not a computation: it is LinearMap.trace_eq_sum_inner, valid for any orthonormal basis of \(T_xM\) (divCurvature_eq_sum_basis), and divCurvature_eq_sum_frame reads it off any \(C^2\) frame whose values at \(x\) are orthonormal. Note the contrast with the scalar curvature: there the object traced is a bilinear form and the trace is metric; here it is an endomorphism and no metric enters the trace at all — the metric appears only in writing it as \(\sum _i \langle \cdot , e_i\rangle \).
This is the object the contracted second Bianchi identity is about, and through that identity the object \(\Delta \operatorname {scal}\) is about.
Proved (Divergence.lean). Take the second Bianchi identity with \(e_i\) in the direction slot,
pair with \(e_i\), and sum. The middle term is turned round by antisymmetry of \(\nabla R\) in its second and third slots (covCurvature_antisymm). Nothing is differentiated along the frame: the identity is pointwise in \(e_i\) and is only summed, so no derivative of \(e_i\) appears and no orthonormality is used beyond what Definition 51 already needs.
What is left to reach \(\operatorname {div}\operatorname {Ric}= \tfrac 12 d\operatorname {scal}\) is a single further identity: the two sums on the right are \((\nabla _Y\operatorname {Ric})(Z,W)\) and \((\nabla _Z\operatorname {Ric})(Y,W)\). That is the trace commuting with \(\nabla \) for the curvature endomorphism — the analogue for \(R\) of Lemma 59, and like it a statement about a frame that is not parallel, so the coefficients \(\langle \nabla _X e_i, e_j\rangle \) enter and are killed by antisymmetry. It is not proved yet.
For a Levi-Civita connection,
Proved (Divergence.lean). Lemma 52 already gives this with the right-hand side written as two frame sums \(\sum _i \langle (\nabla _XR)(e_i,Z)W, e_i\rangle \). What is proved here is that each such sum is \((\nabla _X\operatorname {Ric})(Z,W)\) — sum_inner_covCurvature_eq, the statement that the first-slot trace commutes with \(\nabla \).
Why that is not immediate. \(\operatorname {Ric}(Z,W)\) is a frame sum only where the frame is orthonormal, so differentiating it in \(X\) means differentiating the frame too, and a \(C^2\) orthonormal frame is not parallel. Expanding \(X\big(\sum _i \langle R(e_i,Z)W, e_i\rangle \big)\) by metric compatibility produces, besides the wanted terms, \(\sum _i \langle R(e_i,Z)W, \nabla _X e_i\rangle \); and \((\nabla _XR)(e_i,Z)W\) carries the matching \(-R(\nabla _X e_i, Z)W\). Their sum is
which vanishes because the coefficients \(\langle \nabla _X e_i, e_j\rangle \) are antisymmetric (metric compatibility plus local constancy of \(\langle e_i, e_j\rangle \)) while the bracket is symmetric in \(i,j\). That is exactly the mechanism of Lemma 59, and the same Lean lemma sum_bilin_of_antisymm does the work; what is new is that \(\beta \) has to be produced as a genuine continuous bilinear form, which is curvatureBilinFst, available only because \(R\) is tensorial in its first slot.
Both hypotheses on the connection are used, and for different things: torsion-freeness for the second Bianchi identity, metric compatibility for the trace to commute with \(\nabla \).
What is left is the second contraction, \(\operatorname {div}\operatorname {Ric}= \tfrac 12\, d\operatorname {scal}\): trace this identity again over \(Y\) and \(W\). That needs the pair symmetry of \(R\) carried through \(\nabla \), and Lemma 59 to turn \(\sum _j (\nabla _Z\operatorname {Ric})(e_j,e_j)\) into \(Z(\operatorname {scal})\).
For a Levi-Civita connection, \(\operatorname {div}\operatorname {Ric}= \tfrac 12\, d\operatorname {scal}\); in the frame form the Lean statement takes,
Proved (Divergence.lean). Contract Theorem 53 over its remaining two slots: sum
over \(j\). On the right the first sum is \(Y(\operatorname {scal})\) by Lemma 59, and the second is \(\operatorname {div}\operatorname {Ric}(Y)\) because \(\nabla \operatorname {Ric}\) is symmetric — which it is because \(\operatorname {Ric}\) is (Lemma 21), so this step too needs the connection to be metric. On the left, pair symmetry of \(\nabla R\) turns \(\langle (\nabla _{e_i}R)(Y,e_j)e_j, e_i\rangle \) into \(\langle (\nabla _{e_i}R)(e_j,e_i)Y, e_j\rangle \), whose sum over \(j\) is \((\nabla _{e_i}\operatorname {Ric})(e_i,Y)\) by Theorem 53’s trace lemma; summing over \(i\) gives \(\operatorname {div}\operatorname {Ric}(Y)\) back. So \(\operatorname {div}\operatorname {Ric}(Y) = Y(\operatorname {scal}) - \operatorname {div}\operatorname {Ric}(Y)\).
Pair symmetry of \(\nabla R\) is not inherited for free. What Lemma 17 gives is a symmetry of the \((0,4)\) tensor \(\langle R(A,B)C,D\rangle \), and \(\nabla R\) is defined as an operator on fields, not as the derivative of that tensor. The bridge is inner_covCurvature_expand: for a metric connection the leading \(\nabla _X\) can be moved onto the pairing, so
five corrections rather than four — the fifth is the metric one. Every term on the right is the \((0,4)\) tensor evaluated somewhere, so the pointwise symmetry transfers, and the two sides’ corrections are the same five numbers in a different order.
With this, roadmap item 2 is closed. The next link in the chain is \(\operatorname {tr}_g \partial _t \operatorname {Ric}= \Delta \operatorname {scal}\) under the flow; combined with RicciVariation.lean’s \(\partial _t \operatorname {scal}= \operatorname {tr}_g \partial _t\operatorname {Ric}+ 2|\operatorname {Ric}|^2\) that gives \(\partial _t \operatorname {scal}= \Delta \operatorname {scal}+ 2|\operatorname {Ric}|^2\).
Let \(h\) be a bilinear form field on \(TM\) and \(\nabla \) a connection. Then \((\nabla _X h)(Y,Z) = X(h(Y,Z)) - h(\nabla _X Y, Z) - h(Y, \nabla _X Z)\) is tensorial and pointwise in all three slots: a continuous trilinear form on \(T_xM\), not merely an operation on fields. In particular \(\nabla _X h\) is an honest bilinear form \(\texttt{covBilinForm}\), and the direction is an honest linear form \(\texttt{covBilinDir}\).
Proved (BilinDeriv.lean). All three slots are cheap, unlike the four slots of \(\nabla \operatorname {Rm}\) (Lemma 48). The direction slot needs nothing: each of the three terms is a continuous linear map — \(\mathrm{d}(h(Y,Z))_x\), \((\nabla Y)_x\), \((\nabla Z)_x\) — applied to \(X(x)\), so linearity and pointwiseness hold by construction, with no differentiability hypothesis whatever. The \(Y\) and \(Z\) slots are the usual Leibniz cancellation: replacing \(Y\) by \(fY\) produces \((Xf)\, h(Y,Z)\) from the derivative term, and \(-h(\nabla _X(fY),Z)\) produces \(-(Xf)\, h(Y,Z)\), which cancels it; only \(\mathrm{MDifferentiableAt}\) of the fields is used, as in the Hessian’s second slot, so no frame-and-globalise argument of the kind \(\operatorname {Rm}\)’s third slot needs (Lemma 9) appears. Hence TensorialAt.mkHom and mkHom\(_2\) apply directly.
The one hypothesis carried is IsMDiffBilinAt: that \(y \mapsto h_y(U_y, V_y)\) is differentiable at \(x\) for differentiable \(U\), \(V\). It is what makes the Leibniz rule available and is implied by \(h\) being \(C^1\) into the space of bilinear forms.
Consequence. \(\operatorname {tr}_g(\nabla _X h)\) is frame-independent on its own (sum_covBilin_congr), by the same trace-of-a-bilinear-map argument that Definition 16 uses for \(\operatorname {scal}\); so both sides of Lemma 59 are frame-independent, not just equal for each frame. This is the object the connection Laplacian \(\Delta _gh\) and the double divergence \(\operatorname {div}\operatorname {div} h\) are traces of, and those are what \(\operatorname {tr}_g(\partial _t \operatorname {Ric}) = \Delta \operatorname {scal}\) needs.
Direction: by construction, as above. Second slot: with \(\nabla _X(fY) = f\nabla _X Y + (Xf) Y\) and \(h(fY,Z) = f\, h(Y,Z)\),
and additivity is the same computation without the coefficient. The third slot is identical with the roles of \(Y\) and \(Z\) exchanged.
For a bilinear form field \(h\),
— one correction per slot of \(\nabla h\), so three, against the five of \(\nabla ^2\operatorname {Rm}\) (Definition 50). The connection Laplacian \(\Delta _gh\) is its metric trace in the two derivative slots, \((\Delta _gh)(Y,Z) = \sum _i (\nabla ^2_{e_i,e_i} h)(Y,Z)\).
Proved (BilinLaplacian.lean). \(\nabla ^2 h\) is tensorial and pointwise in both derivative slots, so \(\Delta _gh\) is well defined and frame-independent. The two slots behave differently, as they do for \(\nabla ^2\operatorname {Rm}\):
The outer direction \(W\) needs no frame argument. It is Lemma 55 cashed in: the leading term is a continuous linear map at \(W(x)\), and each of the three corrections is \(\nabla h\) in a slot it is already pointwise in, applied to a field whose value at \(x\) is determined by \(W(x)\).
The inner direction \(X\) is the Leibniz cancellation — and the cancellation is cheap, because every step other than the leading one uses only the direction slot of \(\nabla h\), which carries no hypotheses at all. Pointwiseness there is the frame-and-globalise argument, but it runs at \(C^1\): cov2Bilin_smul_snd asks its coefficient for one derivative, against the three that \(\nabla ^2\operatorname {Rm}\) asks.
The one hypothesis beyond Lemma 55’s is IsMDiffCovBilinAt: that \(y \mapsto (\nabla _V h)(Y,Z)\) is differentiable at \(x\) for \(C^1\) fields \(V\). Merely-differentiable \(V\) cannot supply this — the leading term of \(\nabla h\) differentiates \(h(Y,Z)\) in the direction \(V\), so it sees the germ of \(V\) — which is exactly why the inner slot needs the frame argument and the outer one does not.
The trace commutes with \(\nabla ^2\) too: \(\nabla ^2(\operatorname {tr}_gh)(X,Y) = \sum _i (\nabla ^2_{X,Y}h)(e_i,e_i)\) (traceBilin, hessianFun_traceBilin_eq), by the same mechanism as the divergence (Definition 57) one level up: differentiating the frame sum twice produces \(\nabla ^2h\) plus exactly the term \(\operatorname {tr}_g(\nabla _{\nabla _XY} h)\) that the Hessian’s connection correction subtracts. Tracing once more identifies \(\Delta (\operatorname {tr}_gh)\) with \(\operatorname {tr}_g(\Delta _gh)\).
This is what \(\operatorname {tr}_g(\partial _t\operatorname {Ric}) = \Delta \operatorname {scal}\) is assembled from. Tracing the first variation of \(\operatorname {Rm}\) (Lemma 62) twice against the Koszul formula for \(\partial _t\nabla \) gives, with no curvature terms,
and under the flow \(h = -2\operatorname {Ric}\), so \(\operatorname {tr}_gh = -2\operatorname {scal}\) and \(\operatorname {div}\operatorname {div} h = -2\operatorname {div}\operatorname {div}\operatorname {Ric}= -\Delta \operatorname {scal}\) by the second contraction (Theorem 54), giving \(2\Delta \operatorname {scal}- \Delta \operatorname {scal}= \Delta \operatorname {scal}\).
For a one-form field \(\omega \), \((\nabla _X \omega )(Y) = X(\omega (Y)) - \omega (\nabla _X Y)\), and \(\operatorname {div}\omega = \sum _i (\nabla _{e_i} \omega )(e_i)\). For a bilinear form field \(h\), \((\operatorname {div} h)(Z) = \sum _i (\nabla _{e_i} h)(e_i, Z)\), and the double divergence is \(\operatorname {div}\operatorname {div} h = \operatorname {div} (\operatorname {div} h)\).
Proved (OneForm.lean). The point is that \(\operatorname {div}\operatorname {div} h\) — the trace of \(\nabla ^2 h\) pairing slots \(1\& 3\) and \(2\& 4\) — needs no four-linear packaging of \(\nabla ^2h\) at all. It factors into two cheap traces:
\(\operatorname {div} h\) is the trace of the \((0,3)\)-tensor \(\nabla h\) (Lemma 55) in its first two slots, which is one \(\texttt{mkHom}_2\) over (direction, second slot): the direction slot is tensorial with no hypotheses, and the second is the Leibniz cancellation. It is tensorial in its remaining slot as a finite sum of third-slot tensorialities, so it is an honest one-form field.
\(\nabla \omega \) has two terms, against \(\nabla h\)’s three and \(\nabla \operatorname {Rm}\)’s four, so both of its slots are free of any frame argument: the direction is a continuous linear map by construction, and the \(Y\) slot is the plain Leibniz cancellation on merely differentiable fields. So \(\texttt{TensorialAt.mkHom}_2\) applies directly and \(\operatorname {div}\omega \) is frame-independent for free.
The two definitions agree. \(\operatorname {div}\operatorname {div} h\) is defined here as an iterated divergence, while the evolution of the scalar curvature produces the double trace of \(\nabla ^2h\). They are equal:
(covOneForm_divBilinOneForm_eq_sum, divDivBilin_eq_sum) — the divergence commutes with \(\nabla \). This is Lemma 59 applied to the bilinear form \((v,w) \mapsto (\nabla _v h)(w,Z)\): differentiating the frame sum produces \(\nabla ^2h\) plus exactly the term \((\operatorname {div} h)(\nabla _W Z)\) that \(\nabla _W\) of a one-form subtracts, so the two cancel and no curvature term survives.
For \(\omega = \mathrm{d}f\) these are the Hessian and Laplacian of a function (Definition 46) — not merely analogous: \(\nabla ^2 f(X,Y)\) and \((\nabla _X \mathrm{d}f)(Y)\) are the same expression, so hessianFun_eq_covOneForm and laplacianFun_eq_divOneForm are rfl. That is worth more than a remark: it hands the Hessian its bilinear packaging for free. \(\nabla ^2 f\) on its own has no cheap route to one — the analogue of TensorialAt would need \(y \mapsto \mathrm{d}f_y(Y_y)\) differentiable for merely differentiable \(Y\) — but \(\nabla \omega \) has two terms and needs no frame argument at all, so laplacianFun_eq_sum_frame (that \(\Delta f\) may be read off any frame orthonormal at \(x\)) follows from divOneForm_eq_sum_frame.
Consequence, and the last identification the flow needs: \(\Delta (\operatorname {tr}_gh) = \operatorname {tr}_g(\Delta _gh)\) (laplacianFun_traceBilin_eq). Both sides are read off the same frame and the terms match by the second-order trace lemma of Definition 56, plus one \(\texttt{Finset.sum\_ comm}\). So the second of the two canonical double traces of \(\nabla ^2h\) is the Laplacian of a function. For \(h = \operatorname {Ric}\) the double divergence is \(\tfrac 12\Delta \operatorname {scal}\) (divDivBilin_ricciForm_eq), which is the second contraction of the second Bianchi identity with the divergence taken once more: \(\operatorname {div}\operatorname {Ric}\) is the one-form \(\tfrac 12\, \mathrm{d}\operatorname {scal}\) (divBilin_ricciForm_eq, Theorem 54 read as an identity of one-forms rather than a frame sum), and the divergence of \(\mathrm{d}f\) is \(\Delta f\). The two steps in between are that \(\operatorname {div}\) is linear in \(\omega \) and depends only on its germ (divOneForm_smul, divOneForm_congr).
Hence \(\operatorname {tr}_g(\partial _t\operatorname {Ric}) = \Delta \operatorname {scal}\) under the flow (sum_cov2Bilin_neg_two_ricciForm_eq): at \(h = -2\operatorname {Ric}\) the first of the two canonical double traces is \(\operatorname {div}\operatorname {div} h = -2\cdot \tfrac 12\Delta \operatorname {scal}= -\Delta \operatorname {scal}\) and the second is \(\operatorname {tr}_g(\Delta _gh) = \Delta (\operatorname {tr}_gh) = -2\Delta \operatorname {scal}\), so their difference is \(\Delta \operatorname {scal}\). Getting there needs only that \(\nabla ^2h\) is linear in \(h\) (cov2Bilin_smul_form, from covBilin_smul_form) — everything else is already proved for \(\operatorname {Ric}\) itself, and \(\operatorname {tr}_g\operatorname {Ric}\) is \(\operatorname {scal}\) by definition, the same frame sum.
With \(\Delta _gh\) from Definition 56, both traces in
now exist, and under the flow \(h = -2\operatorname {Ric}\) the second contraction of the second Bianchi identity (Theorem 54) turns the right-hand side into \(2\Delta \operatorname {scal}- \Delta \operatorname {scal}= \Delta \operatorname {scal}\).
Let \(\nabla \) be a metric connection and \(A\) a \((1,2)\)-tensor field satisfying the Koszul characterisation of Lemma 61,
Then \(\nabla A\) satisfies the same combination one level up, with \(\nabla h\) replaced by \(\nabla ^2 h\) and no curvature terms:
Proved (KoszulSecondDeriv.lean). Metric compatibility moves \(\nabla _U\) onto the pairing, turning \(\langle \nabla _U(A(P,Q)), R\rangle \) into \(U\langle A(P,Q),R\rangle - \langle A(P,Q), \nabla _U R\rangle \); the first term differentiates the germ identity, producing the three \(\nabla ^2h\)-terms plus nine corrections, and those nine regroup — three by three, one group per differentiated field — into exactly the three Koszul combinations \(\langle A(\nabla _U P, Q),R\rangle \), \(\langle A(P,\nabla _U Q),R\rangle \), \(\langle A(P,Q),\nabla _U R\rangle \) that \(\nabla _U A\) and the pairing subtract. The regrouping is linear, so once the four expansions are in hand it is linarith.
This is what turns \(\partial _t \operatorname {Rm}= (\nabla \dot A)(\cdot ,\cdot ) - (\nabla \dot A)(\cdot ,\cdot )\) (Lemma 62) into a statement about \(\nabla ^2 h\) alone.
The double trace. Tracing it twice gives, for symmetric \(h\),
with no curvature terms at any stage (sum_inner_covTwoTensor_eq, and sum_inner_covTwoTensor_eq_divDiv with the two sums named as Definitions 57 and 56). Symmetry of \(h\) is what collapses six double sums to two: it identifies \((\nabla ^2_{U,a}h)(b,c)\) with \((\nabla ^2_{U,a}h)(c,b)\) (cov2Bilin_symm, from covBilin_symm), which merges the first two terms of each Koszul combination. The remaining bookkeeping is one \(\texttt{Finset.sum\_ comm}\), folding the two copies of \(\operatorname {tr}_g(\Delta _gh)\) together.
\(\operatorname {Rm}_A\) is \(\partial _t\operatorname {Rm}\), and this is now a theorem rather than a remark (FlowKoszul.lean). Two conventions had to be lined up: covEnd, which the first variation of the curvature is phrased in, takes a \((1,2)\)-tensor with its argument first and its direction second (matching differenceE), while covTwoTensor takes the direction first — so the two agree on flipped tensors, term for term (covEnd_eq_covTwoTensor_flip, a rfl). With derivDifferenceTensor the flip of \(\partial _t\nabla \), isKoszulOf_derivDifference says it is Koszul for \(h = \partial _t g\) — Lemma 61 states that on the constant-in-a-trivialisation extensions of the two vectors, and the covBilin congr lemmas transfer it to arbitrary differentiable fields — and hasDerivAt_curvatureE_covTwoTensor delivers \(\partial _t\operatorname {Rm}\) as \(\operatorname {Rm}_A\) for that tensor.
Reading the trace off a frame. The variation formula delivers \(\partial _t[v \mapsto \operatorname {Rm}(v,X)Y]\) on the constant-in-a-trivialisation extension of \(v\), while the double trace above is taken over a local orthonormal frame. Transferring between them is derivCurvatureEndoE_apply_field, which needs \(\nabla A\) to be pointwise in each of the two slots \(v\) lands in: the direction slot is free (covTwoTensor_congr_dir — all three terms are continuous linear maps at \(U(x)\)), and the tensor’s first argument slot is the Leibniz cancellation, so TensorialAt applies and covTwoTensor_congr_snd follows with no frame argument. The one hypothesis is IsMDiffTwoTensorAt: that \(y \mapsto A_y(P_y,Q_y)\) is differentiable for differentiable \(P\), \(Q\) — for \(A = \partial _t\nabla \) a regularity hypothesis on the first variation of the connection, carried alongside the commutation hypotheses the variation already needs.
And the double trace is \(\operatorname {tr}_g(\partial _t\operatorname {Ric})\), now as a theorem (metricTraceE_derivRicciFormOfMetric_eq_sub): with \(h = \partial _tg\),
with no curvature terms. The outer trace is Lemma 63’s \(\operatorname {tr}_g\) read off a \(g\)-orthonormal basis; the inner one is the endomorphism trace \(\operatorname {Ric}(v,w) = \operatorname {tr}(u \mapsto \operatorname {Rm}(u,v)w)\) read off the same basis; and the summand is derivCurvatureEndoE_apply_field. One \(\texttt{Finset.sum\_ comm}\) lines the two up with the double-trace theorem, whose Koszul hypothesis \(\partial _t\nabla \) supplies.
Under the Ricci flow \(h = -2\operatorname {Ric}\), so \(\operatorname {tr}_gh = -2\operatorname {scal}\) and the two contracted Bianchi identities (Theorems 53, 54) turn the right-hand side into \(2\Delta \operatorname {scal}- \Delta \operatorname {scal}= \Delta \operatorname {scal}\).
Let \(\nabla \) be a metric connection, \(B\) a bilinear form field on \(TM\) and \(e_1, \dots , e_n\) a local orthonormal frame near \(x\). Then
where \((\nabla _X B)(Y,Z) = X(B(Y,Z)) - B(\nabla _X Y, Z) - B(Y, \nabla _X Z)\). Since \(\sum _i B(e_i,e_i)\) is the metric trace \(\operatorname {tr}_gB\) for any orthonormal frame, this is \(X(\operatorname {tr}_gB) = \operatorname {tr}_g(\nabla _X B)\).
Proved (TraceCov.lean). This is the gate for every Laplacian identity below: the contracted second Bianchi identity, \(\partial _t R = \Delta R + 2|\operatorname {Ric}|^2\) inside Lemma 64, and \(\partial _t \operatorname {Rm}= \Delta \operatorname {Rm}+ Q\) (Lemma 66).
\(B\) need not be symmetric, and the frame need not be parallel — which is the point, since a parallel frame exists only along a curve. Two auxiliary results are stated separately and are of independent use: inner_cov_antisymm, that the connection coefficients of an orthonormal frame are antisymmetric, and sum_bilin_of_antisymm, the purely algebraic cancellation. A local orthonormal frame is supplied by OrthonormalFrame.lean, and exists_orthonormalBasis_of_isOrthonormalFrameOn turns it into an orthonormal basis of each fibre over its base set.
First consequence, and the reason for the node: \(X(\operatorname {scal}) = \operatorname {tr}_g(\nabla _X \operatorname {Ric})\) (mvfderiv_scalarCurvatureAt_eq_sum_covBilin), taking \(B\) to be the Ricci form of Definition 16. The scalar curvature is the frame sum at every point of the frame’s base set, so the two sides are germ-equal at \(x\) and the trace lemma applies verbatim. Its one remaining hypothesis is genuine regularity — \(y \mapsto \operatorname {Ric}(e_i,e_i)(y)\) must be differentiable, which asks the connection for one derivative more than \(\texttt{ContMDiffCovariantDerivative}\ 1\) gives.
Expanding the definition of \(\nabla _X B\), the claim is that the \(2n^2\) correction terms cancel:
Write \(\nabla _X e_i = \sum _j a_{ij} e_j\) with \(a_{ij} = \langle \nabla _X e_i, e_j \rangle \). Because \(\langle e_i, e_j \rangle \) is constant near \(x\), its derivative along \(X\) vanishes, and metric compatibility \(X\langle e_i, e_j\rangle = \langle \nabla _X e_i, e_j\rangle + \langle e_i, \nabla _X e_j\rangle \) forces \(a_{ij} = -a_{ji}\). The sum above is then \(\sum _{i,j} a_{ij}\big[B(e_j,e_i) + B(e_i,e_j)\big]\), in which the bracket is symmetric under \(i \leftrightarrow j\) while \(a\) is antisymmetric; swapping the two summation indices shows the sum is its own negative. Differentiating the trace term by term needs \(\mathrm{d}\) of a finite sum (mvfderiv_fun_sum), and the vanishing of the derivative of a locally constant function needs that \(\mathrm{d}\) depends only on the germ (Filter.EventuallyEq.mvfderiv_eq); both are missing from Mathlib and are proved here.
At a local minimum \(x_0\) of a \(C^2\) function \(f\) on a boundaryless manifold, \(\nabla f(x_0) = 0\), \(\nabla ^2 f(X,X)(x_0) \ge 0\) for every vector field \(X\) differentiable at \(x_0\), and \(\Delta f(x_0) \ge 0\); for any covariant derivative, not only the Levi-Civita connection.
Proved, first on the model space (hessianFun_nonneg_of_isLocalMin_model), then on a manifold by transport through extChartAt (hessianFun_nonneg_of_isLocalMin), since at a critical point the Hessian is connection-independent. With it, the abstract maximum principle 77 becomes the classical one for \(\partial _t u = \Delta u + F(u)\).
On the line: if \(g'' (t_0) {\lt} 0\) at a local minimum with \(g'(t_0) = 0\), then \(g' {\lt} 0\) just to the right of \(t_0\) and the mean value theorem gives \(g(t_1) {\lt} g(t_0)\) there (deriv2_nonneg_of_isLocalMin). In a normed space, restrict to the line \(x_0 + tv\) to get \(D^2 f(x_0)(v,v) \ge 0\) (fderiv2_nonneg_of_isLocalMin). For the Hessian, \(\nabla ^2 f(X,X) = X(Xf) - (\nabla _X X) f\); the product rule gives \(X(Xf) = D^2f(X,X) + Df(DX\cdot X)\), and \(Df(x_0) = 0\) kills both the second term and the connection term (fderiv_fderiv_apply_nonneg_of_isLocalMin). On a manifold, write \(g = f \circ (\mathrm{extChartAt}\, x_0)^{-1}\): \(g\) has a local minimum at the chart image of \(x_0\) since the inverse chart is continuous, so \(Dg = 0\) there; \(X(Xf)\) at \(x_0\) is the chart-side expression \(D(Dg \cdot \tilde X)(\tilde X)\) with \(\tilde X\) the pullback of \(X\) (the same transport as Lemma 5), and the vector-space case applies. Boundarylessness is what makes \(g\) genuinely \(C^2\) at an interior point of the model rather than \(C^2\) within its range. The Laplacian is a sum of such terms over an orthonormal basis, each extended to a differentiable section.
Along a family of metrics \(g(t)\) with \(\partial _t g= h\), the Levi-Civita connections \(\nabla ^t\) satisfy
with \(\nabla = \nabla ^{t_0}\) on the right and \((\nabla _X h)(Y,Z) = X(h(Y,Z)) - h(\nabla _X Y, Z) - h(Y, \nabla _X Z)\) (CovariantDerivative.covBilin).
Proved, including the differentiability of \(t \mapsto \nabla ^t_X Y(x)\), with one hypothesis stated in exactly the form used: the space derivatives \(X(g(Y,Z))\) commute with \(\partial _t\) for every test field \(Z\) differentiable at \(x\) (three permuted forms), a joint-regularity statement about \((t,x) \mapsto g(t)(x)\) which the pointwise-in-\(t\) Definition 39 does not impose. Differentiability of \(t \mapsto \nabla ^t_X Y(x)\) comes from the musical isomorphism: \(\nabla ^t_X Y = (g_t)^{\sharp \, -1}(K_t)\) with \(K_t = g_t(\nabla ^t_X Y, \cdot )\) the Koszul functional; \((g_t)^\sharp \) is invertible by positive definiteness (isInvertible_innerE), \(K_t\) is differentiable coordinatewise by the differentiated Koszul formula, and ContinuousLinearMap.inverse is smooth at invertible points (exists_hasDerivAt_leviCivitaOfMetricE). The scalar form (hasDerivAt_inner_leviCivitaOfMetric) needs only the commutation hypothesis for the one field \(Z\) at hand.
By the Koszul formula, \(g(\nabla _X Y, Z)\) is an explicit expression in the metric alone, so \(\partial _t\) of it is the same expression in \(h\) (hasDerivAt_inner_leviCivitaOfMetric). The Koszul combination of a symmetric bilinear form \(h\), rewritten through a torsion-free connection, is \((\nabla _X h)(Y,Z) + (\nabla _Y h)(Z,X) - (\nabla _Z h)(X,Y) + 2h(\nabla _X Y, Z)\) (koszul_bilin_eq: for \(h = g\) and \(\nabla \) compatible the first three terms vanish and this is Koszul itself). The product rule \(\partial _t[g(\nabla _X Y, Z)] = h(\nabla _X Y, Z) + g(\partial _t \nabla _X Y, Z)\) absorbs the last term.
Time derivatives of the metric are typed on the model space \(E = T_xM\): TangentSpace carries no norm of its own (the norm comes from the metric), so HasDerivAt into \(T_xM \to T_xM \to \mathbb {R}\) cannot be stated, while into \(E \to E \to \mathbb {R}\) it can, and in finite dimensions the notion does not depend on the norm.
Along a family of metrics \(g(t)\) with \(\partial _t g= h\), the curvature tensors \(\operatorname {Rm}^t\) of the Levi-Civita connections satisfy
with \(\nabla = \nabla ^{t_0}\) and \(\dot A = \partial _t \nabla \) the tensor of Lemma 61, \(g(\dot A(v,w), Z) = \tfrac 12[(\nabla _v h)(w,Z) + (\nabla _w h)(Z,v) - (\nabla _Z h)(v,w)]\) (inner_derivDifferenceE_eq). With \(h = -2\operatorname {Ric}\) this is \(\partial _t \operatorname {Rm}\) under the flow, before the second Bianchi identity turns \(\nabla ^2 \operatorname {Ric}\) into \(\Delta \operatorname {Rm}+ Q(\operatorname {Rm})\) (Lemma 66).
Proved, in two layers. The algebraic layer (curvature_eq_add_covEnd) is for any two connections \(\nabla ' = \nabla + A\) with \(\nabla \) torsion-free:
The analytic layer (hasDerivAt_curvatureE) differentiates this along a family \(\nabla ^t = \nabla + A^t\) with \(A^{t_0} = 0\): the quadratic terms have zero derivative at \(t_0\). Two hypotheses are stated in the form used: the commutation of Lemma 61, now for all fields differentiable at the point (CommutesWithMvfderiv), and the commutation of \(\partial _t\) with \(\nabla _X\) on the sections \(A^t(Y,Z)\) and \(A^t(X,Z)\) at \(x\). Both are joint regularity in \((t,x)\).
The difference of two connections is a tensor, Mathlib’s CovariantDerivative.difference; expanding \(\nabla '_X \nabla '_Y Z - \nabla '_Y \nabla '_X Z - \nabla '_{[X,Y]} Z\) with \(\nabla ' = \nabla + A\) and collecting, the terms \(A(\nabla _X Y, Z) - A(\nabla _Y X, Z)\) combine with \(-A([X,Y], Z)\) by torsion-freeness, and what remains is the displayed identity. Along the family, \(t \mapsto A^t(y)\) is differentiable as a bilinear map because it is differentiable on every pair of vectors (exists_hasDerivAt_clm_of_apply, finite dimensions) and each value \(A^t(v,w)(y) = \nabla ^t_v \tilde w - \nabla _v \tilde w\) is differentiable by Lemma 61, \(\tilde w\) the extension of \(w\) constant in a trivialisation. The derivative \(\dot A\) is deriv, so the statement carries no existential.
For a metric \(g\) on \(T_xM\) and a bilinear form \(B\), write \(\operatorname {tr}_gB = \sum _i B(e_i,e_i)\) over a \(g\)-orthonormal basis, equivalently the trace of the endomorphism \(g^{\sharp \, -1} B^\flat \). Along a family of metrics with \(\partial _t g= h\) and a family of forms with \(\partial _t B = \dot B\),
This is what turns Lemma 62 into the variations of \(\operatorname {Ric}= \operatorname {tr}_g\operatorname {Rm}\) and \(R = \operatorname {tr}_g\operatorname {Ric}\); under the flow \(h = -2\operatorname {Ric}\), and the correction term is the \(2|\operatorname {Ric}|^2\) of \(\partial _t R = \Delta R + 2|\operatorname {Ric}|^2\).
Proved, at a point, on the model space \(E = T_xM\) (MetricTrace.lean). The trace is defined as \(\operatorname {tr}(g^{\sharp \, -1} \circ B^\flat )\) (metricTraceE) and shown equal to the sum over any orthonormal basis (metricTraceE_eq_sum); the pairing is the trace of \(g^{\sharp \, -1} h^\flat g^{\sharp \, -1} B^\flat \) (metricTraceE_comp_sharpE_eq_sum).
The inverse of the metric is differentiable, since inversion of continuous linear maps is smooth at invertible points, and its derivative is found by differentiating \(g^\sharp \circ g^{\sharp \, -1} = \mathrm{id}\): \(\partial _t g^{\sharp \, -1} = -g^{\sharp \, -1} h^\flat g^{\sharp \, -1}\) (hasDerivAt_inverse_innerE). The product rule for \(g^{\sharp \, -1} \circ B^\flat \) and linearity of the trace give the formula.
Along a family of metrics \(g(t)\) with \(\partial _t g= h\),
and under the Ricci flow \(h = -2\operatorname {Ric}\), so \(\partial _t R = \operatorname {tr}_g(\partial _t \operatorname {Ric}) + 2|\operatorname {Ric}|^2\).
Proved (RicciVariation.lean). Ricci is the trace of the endomorphism \(v \mapsto \operatorname {Rm}(v,X)Y\) of \(T_xM\), so its variation is the trace of the variation of Lemma 62 and no term from the metric appears; this is on any manifold. Scalar curvature is the metric trace of the Ricci form, and Lemma 63 supplies the correction \(-\langle h, \operatorname {Ric}\rangle _g\), which is \(2|\operatorname {Ric}|^2_g= 2\sum _{i,j} \operatorname {Ric}(e_i,e_j)\operatorname {Ric}(e_j,e_i)\) under the flow.
The scalar statement now holds on any manifold. It used to be confined to the model space \(M = E\), because it was phrased through ricciE, the Ricci form built on constant fields, and those are global sections only when \(M = E\). The restriction is removed by working with the tensors of Definition 16 instead: ricciFormOfMetric is the Ricci form of \(g\) on any manifold — Definition 16 for the Levi-Civita connection of \(g\), built on the global \(C^2\) extensions of Lemma 10 — and scalarCurvatureOfMetricAt is \(\operatorname {scal}\) likewise. Three things then transfer verbatim. innerE_deriv_eq_of_isRicciFlowAt’ carries the flow equation \(\partial _t g= -2\operatorname {Ric}\) across, by instantiating the flow on those extensions and using uniqueness of derivatives; hasDerivAt_ricciFormOfMetric differentiates the Ricci form coordinatewise, each value \(\operatorname {Ric}_t(v,w)(x)\) being \(\operatorname {Ric}_t(V,W)(x)\) for any \(C^2\) fields with \(V(x) = v\), \(W(x) = w\); and scalarCurvatureOfMetricAt_eq_metricTraceE identifies \(\operatorname {scal}\) with \(\operatorname {tr}_g\operatorname {Ric}\), so Lemma 63 applies unchanged. The conclusions are hasDerivAt_scalarCurvatureOfMetricAt and, under the flow, hasDerivAt_scalarCurvatureOfMetricAt_of_isRicciFlowAt. The model-space statements are kept: they are the same theorems where Definition 22 was first phrased, and they need no extension lemma.
The one ingredient this left, \(\operatorname {tr}_g(\partial _t\operatorname {Ric}) = \Delta R\), is now proved as well: it rests on the contracted second Bianchi identity in both contractions (Theorems 53 and 54) together with Lemma 58, and the resulting evolution equation is Theorem 65.
\(\operatorname {Ric}_t(X,Y)(x) = \operatorname {tr} T_t\) with \(T_t v = \operatorname {Rm}_t(\bar v, X)Y(x)\), \(\bar v\) the extension of \(v\) constant in a trivialisation; \(t \mapsto T_t\) is differentiable as a linear map because each \(T_t v\) is, by Lemma 62 on the field \(\bar v\), and the trace is linear. On the model space the Ricci form \(\operatorname {Ric}_t(v,w) = \operatorname {Ric}_t(\bar v, \bar w)(x)\) is bilinear by tensoriality in both slots (the second slot from the curvature’s third), differentiable in \(t\) coordinatewise, and \(R_t = \operatorname {tr}_{g_t} \operatorname {Ric}_t\); Lemma 63 differentiates the trace. Under the flow, \(\partial _t g(v,w) = -2\operatorname {Ric}(v,w)\) by definition of the flow and uniqueness of derivatives, and \(\langle -2\operatorname {Ric}, \operatorname {Ric}\rangle _g= -2|\operatorname {Ric}|^2_g\).
Under the Ricci flow, on any manifold,
Proved (ScalarFlow.lean). This is the join of the two halves built separately above, and the first evolution equation of the flow to be formalised here in full.
The analytic half is Lemma 58: for the actual flow, \(\partial _t\nabla \) is Koszul for \(h = \partial _tg\), \(\partial _t \operatorname {Rm}\) is the associated \(\operatorname {Rm}_A\), and the double trace of that is
with no curvature terms — they cancel at the Koszul step, before any Bianchi identity is used.
The geometric half is Definition 57 evaluated at \(h = -2\operatorname {Ric}\) (the flow equation, carried across by innerE_deriv_eq_of_isRicciFlowAt’): the first double trace is \(-2\cdot \tfrac 12\Delta R = -\Delta R\) by the second contraction of the second Bianchi identity differentiated once more, the second is \(\Delta (\operatorname {tr}_gh) = -2\Delta R\), and the difference is \(\Delta R\). That is metricTraceE_derivRicciFormOfMetric_eq_laplacian.
Composing with \(\partial _t R = \operatorname {tr}_g(\partial _t\operatorname {Ric}) + 2|\operatorname {Ric}|^2\) from Lemma 64 gives the statement.
Under the flow, \(\partial _t \operatorname {Rm}= \Delta \operatorname {Rm}+ Q(\operatorname {Rm})\), where \(Q\) is quadratic in the curvature operator.
Obtained cleanly in an evolving orthonormal frame (Uhlenbeck’s trick), which removes the terms coming from the time-dependence of the metric on the bundle. Formally this is a computation, not an estimate, but it is a long one and it is what every subsequent estimate is applied to.
Proved, in the precise form of Theorem 75, which names \(Q\): pairing against the metric frozen at the time of differentiation, \(\partial _t\langle \operatorname {Rm}(X,Y)Z,W\rangle = \langle \Delta \operatorname {Rm}(X,Y)Z,W\rangle + Q_1 + Q_2 + \operatorname {Ric}(R(X,Y)Z,W) + \operatorname {Ric}(Z,R(X,Y)W)\), every term on the right being either \(\Delta \operatorname {Rm}\) or quadratic in the curvature. Uhlenbeck’s trick is not used and is not needed for the identity — the paragraph above overstates what the computation requires. What the trick buys is not the equation but the tensor maximum principle applied to it, where the fibre metric of the bundle moves with \(t\); the identity itself is proved with the pairing frozen, so no time-dependence of the bundle metric ever enters.
This node is kept, rather than merged into Theorem 75, because the downstream estimates reference it by name in fifteen places. Read it as an alias.
For a bilinear form field \(h\) and a torsion-free connection,
Proved (RicciIdentity.lean). Commuting the two derivatives of \(\nabla ^2 h\) costs exactly one curvature term per slot of \(h\) — against none for a function, whose Hessian is symmetric, and one for a section. It is the commutation rule Lemma 66 needs: with \(h = -2\operatorname {Ric}\), turning \(\nabla ^2\operatorname {Ric}\) into \(\Delta \operatorname {Rm}\) plus quadratic terms is a matter of moving derivatives past each other.
The content is one expansion (cov2Bilin_eq_hessianFun): \(\nabla ^2 h\) is the Hessian of the scalar \(h(Y,Z)\), plus terms that are either \(\nabla h\) in one slot or \(h\) applied to a second derivative of one of the fields. The first derivative of the scalar cancels between the leading term and the \(\nabla _{\nabla _W X}\) correction — which is why no first-order term survives.
Antisymmetrising then does three things: the leading Hessian dies because a function has a symmetric Hessian (torsion-freeness, used the first time); the \(\nabla h\) terms and the cross terms \(h(\nabla _X Y, \nabla _W Z)\) cancel outright; and what is left is \(h(\nabla _{[W,X]}Y - \nabla _W\nabla _X Y + \nabla _X\nabla _W Y,\, Z)\), which is \(-h(R(W,X)Y,Z)\) by the definition of the curvature — torsion-freeness used the second time, to turn \(\nabla _W X - \nabla _X W\) into \([W,X]\).
The same expansion one level up is cov2Curvature_eq_hessian, and it is the engine of Lemma 68.
For a torsion-free connection,
Proved (RicciIdentity.lean). One curvature term per slot of \(\operatorname {Rm}\): three for the inputs, one for the vector output. This is what lets the differentiated second Bianchi identity be antisymmetrised, and so is the step from Lemma 4 towards Lemma 66.
The expansion (cov2Curvature_eq_hessian) is the bilinear one one level up: \(\nabla ^2\operatorname {Rm}\) against the Hessian of the section \(\operatorname {Rm}(A,B)C\), with the same cancellation of the section’s first derivative between the leading term and the \(\nabla _{\nabla _X Y}\) correction. It needs no regularity of the connection at all — where the bilinear case had to differentiate a scalar, and so needed mvfderiv to be additive on differentiable functions, here the only splitting is \(\nabla \) over a difference of sections, which is an axiom. What it does need, differentiability of the four sections \(\nabla \operatorname {Rm}\) is built from, is what contMDiff_covCurvature already supplies.
Antisymmetrising then needs four facts, and everything else cancels in pairs — the \(\nabla \operatorname {Rm}\) terms because each appears in both orders, and the cross terms \(\operatorname {Rm}(\nabla _Y A, \nabla _X B)C\) because swapping \(X\) and \(Y\) maps the pair to itself. The output term is Lemma 45, the Ricci identity for sections: this is exactly where a section’s Hessian differs from a function’s, and so where the bilinear case had nothing. The three input terms are one lemma each.
The third slot is the expensive one, as everywhere in this tower. Slots one and two combine their four second-derivative terms using only additivity and pointwiseness at the point (tensorialAt_curvature_fst and _snd); the third needs curvature_add_right and curvature_congr_third, which want their sections globally \(C^2\) — and, because curvature_congr_third argues through an orthonormal frame, a metric. That is the same asymmetry that forced RicciSymm.lean to build curvatureEndoAt by hand rather than off a TensorialAt.
With \(A = \partial _t\nabla \) Koszul for \(h = \partial _t g\),
where \(P_1 = (\nabla ^2_{X,Z}h)(W,Y) - (\nabla ^2_{Y,Z}h)(W,X)\) and \(P_2 = (\nabla ^2_{X,W}h)(Y,Z) - (\nabla ^2_{Y,W}h)(X,Z)\).
Proved (CurvatureFlow.lean). Pairing \(\partial _t\operatorname {Rm}(X,Y)Z = (\nabla _X A)(Y,Z) - (\nabla _Y A)(X,Z)\) against \(W\) and applying Lemma 58 twice gives three antisymmetrised pairs of \(\nabla ^2 h\).
The three pairs are not alike, and the whole evolution equation is that asymmetry. Only the first is antisymmetrised in \(\nabla ^2h\)’s two derivative slots, so only it is a commutator: Lemma 67 evaluates it, and it loses its derivatives entirely, becoming \(h\) applied to \(\operatorname {Rm}\) — under the flow, with \(h = -2\operatorname {Ric}\), exactly the terms quadratic in the curvature. The other two antisymmetrise a derivative slot against an argument slot, so no commutation rule applies to them at all; they keep their derivatives and are what the trace step of Lemma 76 turns into \(\Delta \operatorname {Rm}\).
And the two halves join (inner_derivCurvature_eq_curvatureLaplacian_add):
with \(Q_1,Q_2\) the two commutator sums of Lemma 76. Every term on the right is either \(\Delta \operatorname {Rm}\) or quadratic in the curvature, and the two sources of quadratic terms are different: \(Q_1+Q_2\) is what reordering the derivative slots of \(\nabla ^2\operatorname {Rm}\) cost, while the two \(\operatorname {Ric}\)-against-\(\operatorname {Rm}\) terms are what commuting the derivative slots of \(\nabla ^2h\) cost. Neither is bolted on; each is a commutator defect.
The join needs one bridge, covDivCurvature_eq_cov2Bilin: the trace step speaks \(\operatorname {covRicci}\) (what the contracted second Bianchi identity produces) and the flow side speaks \(\nabla ^2\) of \(\operatorname {ricciForm}\), and the three corrections regroup — not termwise — one group per differentiated slot. Four \(\nabla ^2\operatorname {Ric}\) terms then cancel in pairs, by symmetry of \(\operatorname {Ric}\) alone: the flow side produces \((\nabla ^2_{X,W}\operatorname {Ric})(Y,Z)\) where the trace step produces \((\nabla ^2_{X,W}\operatorname {Ric})(Z,Y)\). That is the last thing the derivation needs, and it is free.
Let \(g\) be a Ricci flow on \([0,T]\) on a closed manifold. If \(R \ge C\) everywhere at time \(0\), then \(R \ge C\) everywhere for every \(t \in [0,T]\).
Proved (ScalarPreservation.lean). This is the first inequality of Hamilton’s pinching set \(K\), proved on the manifold rather than for the ODE.
It needs no Uhlenbeck trick, and that is why it is worth isolating. What forces Hamilton’s trick is that the tensor maximum principle is applied to a section of a bundle whose fibre metric moves with \(t\), so the bundle has to be trivialised first. The scalar equation has no fibre at all: the only thing that moves is the Laplacian, and the maximum principle never looks at the Laplacian except to ask that it be \(\ge 0\) at a spatial minimum — which Lemma 60 gives for each metric separately. So the abstract principle 77 applies directly, and the metric is introduced only inside the proof, one time at a time.
The reaction term is nonnegative because \(|\operatorname {Ric}|^2_g\) is a sum of squares over any \(g\)-orthonormal basis (metricTraceE_comp_sharpE_self_nonneg, using symmetry of \(\operatorname {Ric}\)), so the comparison ODE is \(\varphi ' = 0\) and the constant \(C\) is a subsolution.
The hypothesis is the evolution equation of Theorem 65, asked for at each time separately. That it really is that theorem’s conclusion — the two differ only by the letI introducing the metric’s instance — is itself checked, by a bridge lemma proved by := h; so the statement is not vacuous.
Sharpening it is Theorem 71, which keeps the reaction term instead of discarding it.
Let \(g\) be a Ricci flow on \([0,T]\) on a closed \(n\)-manifold and let \(C {\lt} 0\). If \(R \ge C\) everywhere at time \(0\), then for every \(t \in [0,T]\)
which increases from \(C\) towards \(0\).
Proved (ScalarLowerBound.lean). Theorem 70 threw the reaction term away; keeping it gives the estimate. By Cauchy–Schwarz \(R^2 \le n|\operatorname {Ric}|^2_g\) (sq_metricTraceE_le_card_mul at \(B = \operatorname {Ric}\)), so \(2|\operatorname {Ric}|^2 \ge \tfrac {2}{n}R^2\) and \(R\) obeys \(\partial _t R \ge \Delta R + \tfrac {2}{n}R^2\), whose comparison ODE \(\varphi ' = \tfrac {2}{n}\varphi ^2\) has solution \(C/(1 - \tfrac {2}{n}Ct)\).
The obstruction was that \(r \mapsto \tfrac {2}{n}r^2\) is not Lipschitz, while Theorem 77 asks for a Lipschitz reaction. Truncating it at level \(-C\) costs nothing, and no bound on \(R\) has to be assumed: the truncation lies below \(\tfrac {2}{n}r^2\) at every \(r\) — clamping only moves \(|r|\) down — so the hypothesis at spatial minima survives untouched, while along the comparison solution the truncation is invisible, that solution never leaving \([C,0]\). An earlier plan truncated at a bound for \(R\) read off compactness; that is unnecessary.
As in Theorem 70 the Laplacian and the norm both move with \(t\), and the maximum principle does not mind.
For a continuous family of bounded operators \(A : \mathbb {R}\to \mathcal{L}(F)\) with \(\| A(s)\| \le C\), the Picard iterates for \(\Phi ' = A(t)\Phi \), \(\Phi (0) = 1\) — \(I_0 = 1\) and \(I_{n+1}(t) = \int _0^t A(s) I_n(s)\, ds\) — are continuous and satisfy
Proved (LinearODE.lean). This is scaffolding for the ODE that Uhlenbeck’s trick needs: the trivialising family solves \(\partial _t \iota = \operatorname {Ric}\circ \iota \), which is linear in \(\iota \).
Why it is built rather than taken from Mathlib. Analysis/ODE/PicardLindelof.lean does prove existence on a whole interval, but gated on its field mul_max_le: \(L \cdot \max (t_{\max } - t_0, t_0 - t_{\min }) \le a - r\), where \(L\) bounds the vector field on a ball of radius \(a\) about \(x_0\). For a linear field the best available bound is \(L = C(\| x_0\| + a)\), so on \([0,T]\) with \(r = 0\) the condition reads \(a(1 - CT) \ge C\| x_0\| T\) — that is, \(C \cdot T {\lt} 1\). Past that one must continue the solution across a chain of short intervals, and Mathlib has no maximal-solution or continuation theory.
The factorial is what removes the smallness hypothesis. It beats the power at every \(t\), so \(\sum _n I_n(t)\) converges however large \(C\cdot T\) is, and no continuation is needed. The cruder bound \(\| I_n(t)\| \le (Ct)^n\) — what one gets by estimating the integrand by its endpoint value — is useless past \(C \cdot t = 1\), which is precisely the regime where mul_max_le also gives out. The factorial comes from integrating \(s^n\) rather than bounding it.
Let \(A : \mathbb {R}\to \mathcal{L}(F)\) be continuous with \(\| A(s)\| \le C\), \(F\) a Banach space. Then \(\Phi (t) := \sum _{n\ge 0} I_n(t)\) converges for every \(t \in \mathbb {R}\) and
Moreover any two solutions of \(\dot x = A(t)x\) defined on all of \(\mathbb {R}\) and agreeing at \(0\) are equal, so every global solution is \(x(t) = \Phi (t)x(0)\).
Proved (LinearODE.lean). No smallness hypothesis and no continuation argument appears, which is what Lemma 72 explains.
The series is differentiated termwise, not swapped with the integral. Mathlib’s hasDerivAt_tsum_of_isPreconnected asks for a summable bound on the derivatives, uniform on an open preconnected set; here the derivatives are \(A(y)I_n(y)\), bounded by \(C(CR)^n/n!\) on \((-R,R)\), and the factorial makes that summable. Swapping \(\sum \) with \(\int _0^t\) instead would have meant dominated convergence for no gain. The index is shifted first — the derivative of \(I_{n+1}\) is \(A I_n\), so summing over \(I_{n+1}\) is what makes the bound’s index match the term’s, and the zeroth iterate is the constant \(1\), which contributes nothing.
Uniqueness, by contrast, is Mathlib’s verbatim. A linear field is globally Lipschitz with a constant uniform in \(t\) (namely \(C\)), so ODE_solution_unique_univ applies with no work; it is only existence on a long interval that Mathlib cannot supply.
\(\Phi (t)\) is invertible, and both halves come from uniqueness alone — no second series, no adjoint. Injective: if \(\Phi (t)v = 0\) then \(s \mapsto \Phi (s)v\) and the zero solution agree at \(t\), hence everywhere, so \(v = 0\); this is backward uniqueness, and it is exactly what an arbitrary base time in the uniqueness statement buys. Surjective: the propagator \(U(\cdot ,t)\) — the Dyson sum of the time-shifted family — gives a global solution taking the value \(w\) at \(t\), and every global solution is \(\Phi (s)\) applied to its own value at \(0\). The open mapping theorem then makes \(\Phi (t)\) a linear homeomorphism. This matters because Uhlenbeck’s trivialising family must be a bundle isomorphism, not merely a bundle map.
What this is for. Uhlenbeck’s trick trivialises the bundle along a family \(\iota (t)\) solving \(\partial _t \iota = \operatorname {Ric}_{g_t}\circ \iota \), \(\iota (0) = \mathrm{id}\), on all of \([0,T]\) — a linear equation in \(\iota \). What is still missing after this theorem is \(C^k\) dependence of \(\Phi \) on a parameter, since the pulled-back curvature has to be a differentiable section; see the discussion at 78.
Let the family depend on a parameter: \(A : H \times \mathbb {R}\to \mathcal{L}(F)\) with \(H\) a normed space, \(A(x,\cdot )\) continuous, \(\| A(x,s)\| \le C\), and \(x \mapsto A(x,s)\) differentiable with \(\| D_xA(x,s)\| \le C'\), both bounds uniform. Then
where \(J_0 = 0\) and \(J_{n+1}(x,t) = \int _0^t A(x,s)J_n(x,s) + (D_xA(x,s)\, \cdot \, )I_n(x,s)\, ds\) — the recursion for \(I_n\) differentiated under the integral sign.
Proved (LinearODE.lean). Mathlib has this in no form: its local flow is built by choose behind a dite, so as constructed it is not even continuous in the initial point, and only Lipschitz and continuous dependence on the initial condition are available. Both open lines of the roadmap are gated on exactly this — Uhlenbeck’s trivialising family must be a differentiable section, and the regularity of \(\exp \) runs through the variational equation, which is linear.
The derivative bound is the factorial bound with one power of \(|t|\) traded in. \(\| J_{n+1}(x,t)\| \le C'|t|(C|t|)^n/n!\), summing to \(C'|t|e^{C|t|}\): the Leibniz term contributes \(D_xA\) exactly once along the recursion, so one factor of \(C\) becomes \(C'\) and one power of \(|t|\) is gained. The induction closes with equality, not slack — \(1/(n+2)! + 1/((n+2)n!) = 1/(n+1)!\).
Two design points carry the proof. The bounds are global in \(x\), so the dominating function for differentiation under the integral sign is uniform and the parameter set is all of \(H\): no neighbourhood bookkeeping appears anywhere. And \(J_n\) is defined with its two terms in Mathlib’s order rather than the natural one, because HasFDerivAt.clm_comp states the product rule for \(y \mapsto c(y)\circ d(y)\) that way; matching it makes the differentiation step that lemma verbatim instead of an add_comm at every step of the induction.
The variational equation is proved too (hasDerivAt_dysonDerivSum):
i.e. differentiation in the parameter and in time commute for this equation — proved, not assumed. The argument is the termwise one again, one level up: the terms differentiate to \(A\circ J_n + (D_xA\, \cdot )\circ I_n\), dominated uniformly on \((-R,R)\) by a summable bound.
This is what makes the route to \(C^k\) a checked claim rather than an aspiration. With it the pair \((\Phi , D_x\Phi )\) solves the linear block-triangular system \(\partial _t(u,v) = (Au,\ (D_xA\, \cdot )u + Av)\) on \(\mathcal{L}(F) \times \mathcal{L}(H,\mathcal{L}(F))\), whose operator is bounded, continuous in \(t\), and one derivative less regular in the parameter than \(A\). So \(C^k\) follows from the \(C^1\) theorem applied to the augmented system, by induction on \(k\), with no second-order differentiation under the integral sign anywhere. That induction is not yet carried out.
Under the Ricci flow, on any manifold,
the pairing being against the metric frozen at the time of differentiation, so that the left-hand side is the time derivative of the \((1,3)\)-tensor \(\operatorname {Rm}\) and carries no \(\partial _tg\) term of its own.
Proved (CurvatureEvolution.lean). Lemma 69 proves the identity for any \((1,2)\)-tensor \(A\) Koszul for \(h = -2\operatorname {Ric}\); this specialises it to a genuine Ricci flow, where \(A = \partial _t\nabla \) and \(h = \partial _tg\). Both hypotheses it needs are then theorems rather than assumptions: \(\partial _t\nabla \) is Koszul for \(\partial _tg\) (isKoszulOf_derivDifference), and \(\partial _tg= -2\operatorname {Ric}\) under the flow (innerE_deriv_eq_of_isRicciFlowAt’). Composing with the first variation of the curvature, which delivers \(\partial _t\operatorname {Rm}\) as the \(\operatorname {Rm}_A\) of \(\partial _t\nabla \), turns the identity into a statement about a derivative in \(t\).
What the specialisation costs is bookkeeping, not mathematics, and the same bookkeeping Theorem 65 paid: every hypothesis is written under the two-step letI that introduces the metric’s RiemannianBundle instance and the \(C^1\) regularity of its Levi-Civita connection, and the levels the curvature tower consumes — a \(C^3\) metric and a \(C^3\) connection — are carried as explicit hypotheses, a \(C^2\) metric giving only a \(C^1\) connection.
For a torsion-free connection the cyclic identity of Lemma 4 survives one more derivative:
Proved (BianchiDeriv.lean). This is what the trace step of Lemma 66 consumes: summed over \(Y = e_i\) with \(X = e_i\) it turns \(\Delta \operatorname {Rm}\) into two traces of \(\nabla ^2\operatorname {Rm}\) whose derivative slots are in the wrong order, which Lemma 68 then reorders at the cost of terms quadratic in \(\operatorname {Rm}\).
Nothing is differentiated twice by hand. \(\nabla ^2\operatorname {Rm}\) is \(\nabla \operatorname {Rm}\) differentiated once with one correction per slot, so the cyclic sum splits into a leading part and four correction groups, and every one of the five vanishes by the undifferentiated identity. The leading parts combine, by additivity of \(\nabla \) on sections, into \(\nabla _X\) of the section \(u \mapsto (\nabla _Y\operatorname {Rm})(A,B)C + (\nabla _A\operatorname {Rm})(B,Y)C + (\nabla _B\operatorname {Rm})(Y,A)C\), which Lemma 4 says is the zero section; and each correction group is the cyclic sum with one field replaced by its covariant derivative, so is that lemma again. So the proof is five applications of bianchi_second and one \(\nabla 0 = 0\).
The corrections cancel three at a time, not in pairs — one group per differentiated field, \(\nabla _X Y\), \(\nabla _X A\), \(\nabla _X B\), \(\nabla _X C\). That regrouping is what carries the content. Regularity is one derivative above Lemma 4 throughout, and the last slot stays the expensive one: \(C\) is asked for four derivatives so that \(\nabla _X C\) still has the three that the spectator slot wants. No metric is needed, exactly as for Lemma 4 itself — which is worth knowing before the trace step, where a metric first becomes unavoidable.
The trace is taken (curvatureLaplacian_eq_neg_sum). Summing over \(X = Y = e_i\) puts the first term of the cyclic sum on the diagonal, where it is \(\Delta \operatorname {Rm}\), and leaves the other two:
This is where the metric enters, and it is also what forces Lemma 68: in both surviving sums the traced index sits in the outer derivative slot, while the divergence lemmas of Theorem 53 trace the slot \(\nabla \operatorname {Rm}\) is pointwise in. Reordering the two derivative slots is what produces the terms quadratic in \(\operatorname {Rm}\).
The reordering is done (curvatureLaplacian_eq_swapped). Applying Lemma 68 to each summand moves the traced index out of the outer derivative slot and into the inner one, at the cost of one commutator apiece:
where \(\mathcal{C}\) is curvatureCommutator, the right-hand side of Lemma 68. This is Lemma 66 in outline: the first two sums are \(\nabla \) of a divergence of \(\operatorname {Rm}\) and so become second derivatives of \(\operatorname {Ric}\) by Theorem 53; the last two are \(Q\), and they are quadratic in \(\operatorname {Rm}\) because \(\mathcal{C}\) is \(\operatorname {Rm}\) applied to \(\operatorname {Rm}\). Nothing else will appear — \(Q\) is not bolted on at the end, it is precisely what the reordering costs.
The twenty-five differentiability hypotheses of Lemma 68 all follow from uniform \(C^3\) fields with \(C\) at \(C^4\), which is the regularity the trace already carries; that wrapper (cov2Curvature_sub_swap’) is what makes the identity usable inside a frame sum.
The undifferentiated divergence is identified (sum_inner_covCurvature_snd_eq):
Theorem 53 traces the derivative index against \(\operatorname {Rm}\)’s output, whereas the trace step produces it against \(\operatorname {Rm}\)’s second input. Pair symmetry of \(\nabla \operatorname {Rm}\) exchanges the two: it moves the pair \((B,e_i)\) past \((C,D)\) and so puts \(e_i\) back in the output slot, where \(\operatorname {div}\operatorname {Rm}\) lives. This needs only a \(C^2\) connection. What remains on this line is to move \(\nabla _A\) outside the trace, which is the trace commutes with \(\nabla \) argument of Lemma 59 one level up, with the two frame-derivative corrections cancelling against each other by sum_bilin_of_antisymm — whose statement is already the symmetrised form \(\sum _i (B(D_i,e_i) + B(e_i,D_i)) = 0\) that this produces.
And \(\nabla _A\) does move outside the trace (sum_inner_cov2Curvature_snd_eq_mvfderiv). Expanding \(\operatorname {Rm}\)’s second covariant derivative on the diagonal and pairing with \(D\) leaves five groups: metric compatibility turns the leading one into a derivative of the frame sum minus a term in \(\nabla _A D\); the two in which \(\nabla _A\) landed on the frame cancel each other; the remaining two are the sum with \(B\) or \(C\) differentiated. No curvature term survives — the frame’s non-parallelism is absorbed entirely by the antisymmetry argument, exactly as one level down in Lemma 59.
The cancellation (sum_inner_covCurvature_frame_deriv_eq_zero) is where pair symmetry earns its keep a second time: it puts both frame terms into the same bilinear form covCurvatureBilinDir, one with the arguments in each order, so sum_bilin_of_antisymm applies verbatim. That form is \(\operatorname {innerSL}\) composed with covCurvatureEndo, so bilinearity holds by construction. The frame is asked for \(C^4\): pair symmetry wants \(C^3\) in the slot \(\nabla _A e_i\) occupies.
The trace step closes (inner_curvatureLaplacian_eq):
where \(Q\) is the two commutator sums and \((\nabla _A\operatorname {div}\operatorname {Rm})(C,D,B)\) is covDivCurvature, the covariant derivative of the \((0,3)\)-tensor \(\operatorname {div}\operatorname {Rm}(C,D,B) = (\nabla _C\operatorname {Ric})(D,B) - (\nabla _D\operatorname {Ric})(C,B)\) of Theorem 53. Every term is accounted for: the first two are second derivatives of \(\operatorname {Ric}\), the last two are quadratic in \(\operatorname {Rm}\), being \(\operatorname {Rm}\) applied to \(\operatorname {Rm}\).
One brick was missing for this: the second sum carries the traced index in \(\operatorname {Rm}\)’s first slot rather than its second, so cov2Curvature_antisymm — \(\nabla ^2\operatorname {Rm}\) inheriting \(\operatorname {Rm}\)’s antisymmetry, each of the five terms flipping by covCurvature_antisymm, with the two corrections in \(\nabla _X A\) and \(\nabla _X B\) swapping with each other — turns it round. That is where the sign flip between the two divergence terms comes from.
A solution of \(\partial _t u = \Delta u + \langle X, \nabla u\rangle + F(u)\) on a closed manifold, with \(F\) Lipschitz, is bounded below by the solution of the associated ODE \(\dot\phi = F(\phi )\) with \(\phi (0) \le \min u(0,\cdot )\); and above by it when \(\phi (0) \ge \max u(0,\cdot )\).
Proved, abstractly. The Laplacian enters the classical proof at one point only: at a spatial minimum \(x_0\) of \(u(t,\cdot )\), \(\nabla u = 0\) and \(\Delta u \ge 0\), hence \(\partial _t u(t,x_0) \ge F(u(t,x_0))\). The formalised statement takes exactly that as its hypothesis, on an arbitrary compact space: if at every spatial minimum \(x_0\) of \(u(t,\cdot )\) one has \(F(u(t,x_0)) \le \partial _t u(t,x_0)\), then \(\phi \le u\). No Laplacian and no manifold appear; the classical statement is this theorem plus the second-derivative test at a minimum, and that is the manifold version below.
And on a manifold. With the Laplacian of Definition 46 and the second-derivative test (Lemma 60), the hypothesis at a minimum is discharged: le_of_laplacian is the statement for \(\partial _t u = \Delta u + F(u)\) on a closed Riemannian manifold with \(u(t,\cdot )\) of class \(C^2\), for any connection. The gradient term \(\langle X, \nabla u\rangle \) is not yet included: it needs \(\nabla u = 0\) at a minimum, which is the first-derivative test on a manifold.
Perturb to \(\psi _\epsilon = \phi - \epsilon e^{(2K+1)t}\), a strict subsolution by the Lipschitz bound: \(\dot\psi _\epsilon {\lt} F(\psi _\epsilon )\). If \(u \ge \psi _\epsilon \) failed, the set of times at which it fails is closed (it is the projection of a compact subset of \([0,T] \times M\)), so there is a first time \(t_0 {\gt} 0\) and a point \(x_0\) with \(u(t_0,x_0) = \psi _\epsilon (t_0)\). Then \(x_0\) is a spatial minimum of \(u(t_0,\cdot )\), the left derivative of \(u(\cdot ,x_0) - \psi _\epsilon \) at \(t_0\) is \(\le 0\), but the differential inequality makes it \(\ge \epsilon (K+1) e^{(2K+1)t_0} {\gt} 0\). Let \(\epsilon \to 0\). The upper bound is the same argument applied to \(-u\).
Hamilton’s maximum principle for symmetric tensors: a closed convex subset of the bundle preserved by the ODE \(\dot{\operatorname {Rm}} = Q(\operatorname {Rm})\) is preserved by the PDE.
This is the workhorse. Every curvature-positivity statement in the subject is an instance of it, including the one Hamilton needs in dimension three.
Proved, abstractly. Let \(V\) be a complete real inner product space, \(K \subseteq V\) closed, convex and nonempty, \(M\) compact, \(u : [0,T] \times M \to V\) jointly continuous with time derivative \(\partial _t u\), and \(F\) Lipschitz. Two hypotheses are taken in exactly the form the classical proof uses them. First, at every spatial maximum \(x_0\) of \(x \mapsto \langle n, u(t,x)\rangle \) one has \(\langle n, \partial _t u\rangle \le \langle n, F(u)\rangle \) at \((t,x_0)\); on a manifold this is \(\partial _t u = \Delta u + F(u)\) together with \(\Delta \langle n, u\rangle \le 0\) at a maximum. Second, \(K\) is preserved by the ODE in Nagumo’s form: \(\langle n, F(p)\rangle \le 0\) for every \(p \in K\) and every outward normal \(n\) at \(p\), which subtangential_of_invariant derives from invariance along solution curves (the easy direction of Nagumo’s theorem). Then \(u(0,\cdot ) \in K\) implies \(u(t,\cdot ) \in K\) for all \(t \in [0,T]\). No manifold, no Laplacian and no tensor bundle appear; the trivial bundle with fibre \(V\) is the case Hamilton uses in dimension three, and the general vector-bundle version is the same argument in a parallel frame.
And on a manifold. mem_of_laplacian is the statement on a closed Riemannian manifold for the trivial bundle \(M \times V\), the equation \(\partial _t u = \Delta u + F(u)\) taken componentwise, \(\langle n, \partial _t u\rangle = \Delta \langle n, u\rangle + \langle n, F(u)\rangle \) for every fixed \(n \in V\), with \(u(t,\cdot )\) of class \(C^2\). A maximum of \(\langle n, u\rangle \) is a minimum of \(\langle -n, u\rangle \), so the second-derivative test applies unchanged. Hamilton’s setting, a bundle with an evolving fibre metric, needs the Laplacian on sections together with Uhlenbeck’s trick.
The reaction may depend on time (mem_of_deriv_le_at_max_time, and mem_of_laplacian_time on the manifold). \(F\) enters the proof at exactly three points — the hypothesis at the touching point, the Lipschitz comparison against the nearest point of \(K\), and subtangentiality — and all three happen at the single touching time, so nothing in the argument notices that \(F\) moves. Only the Lipschitz constant must be uniform in \(t\).
This is the generality a moving background geometry needs. Hamilton 1982 §9 applies the principle on a bundle whose fibre metric evolves, which makes the reaction non-autonomous; Uhlenbeck’s trick instead freezes the fibre metric, at the cost of an ODE for the trivialising family. What the generalisation does not buy is a moving inner product on \(V\) itself: \(\operatorname {dist}(\cdot , K)\) and the nearest-point projection are taken in \(V\)’s own metric at every time, and the first-touching-time argument compares them across times. That is the real content of Uhlenbeck’s trick and it is untouched. The time-dependent set \(K_t\) is done, in the monotone case, by Theorem 85 — and that turns out not to be the separate, \(\log (1+t)\)-only generalisation it was filed as here: a moving inner product reduces to a moving set.
Let \(g_t\) be a family of metrics on a closed manifold \(M\), \(V\) a fixed complete real inner product space, and \(u : [0,T] \times M \to V\) a solution of
read componentwise against each \(n \in V\). If \(K \subseteq V\) is closed, convex, nonempty and preserved by the ODE \(\dot v = F_t(v)\) in Nagumo’s form, then \(u(0,\cdot ) \in K\) gives \(u(t,\cdot ) \in K\) for all \(t \in [0,T]\). The scalar statement is the same with \(V = \mathbb {R}\) and a comparison solution \(\varphi ' = F_t(\varphi )\).
Proved (TensorPreservation.lean). A moving Laplacian costs nothing. The maximum principle never inspects \(\Delta \) except to ask that \(\Delta \langle n, u(t,\cdot )\rangle \ge 0\) at a spatial minimum, and Lemma 60 supplies that for each metric separately. So the abstract principle applies with the metric’s instance introduced inside the proof, one time at a time — the manoeuvre Theorem 70 makes inline one level down.
What is still not bought here is a moving inner product on \(V\), and that is the distinction that matters: the fibre is a fixed vector space with a fixed metric and only the base geometry evolves. Hamilton’s curvature operator lives in \(\Lambda ^2T_xM\), whose inner product moves with \(g_t\). Theorem 85 is the next step towards it.
Same skeleton as the proof of 77, with a supporting half-space of the convex set in place of the half-line \([\phi (t),\infty )\). The principle itself does not depend on the evolution equation 66; that enters only when it is applied, in Lemma 90. Perturb: the claim is \(\operatorname {dist}(u(t,x), K) {\lt} \epsilon e^{(2L+1)t}\). If it fails, the set of times where it fails is closed, so there is a first time \(t_0 {\gt} 0\) and a point \(x_0\) where it does; let \(p\) be the nearest point of \(K\) to \(u_0 = u(t_0,x_0)\) and \(n = u_0 - p\). Since \(K\) lies in the half-space \(\langle n, \cdot - p\rangle \le 0\), the function \(\langle n, u(t,\cdot ) - p\rangle \) is bounded by \(|n| \cdot \operatorname {dist}(u(t,\cdot ), K)\), so \(x_0\) is a spatial maximum of it at time \(t_0\), and \(t \mapsto \langle n, u(t,x_0) - p\rangle - |n| \epsilon e^{(2L+1)t}\) is negative before \(t_0\) and zero at \(t_0\), whence its left derivative is \(\ge 0\). The two inequalities give \((2L+1)|n|^2 \le \langle n, F(u_0)\rangle \le \langle n, F(p)\rangle + L|n|^2 \le L|n|^2\), absurd. Let \(\epsilon \to 0\) and use closedness of \(K\).
For every \(v \in T_xM\) there is a global \(C^k\) section \(N\) with \(N(x) = v\) and \(\nabla N(x) = 0\).
Proved (NormalSection.lean). Why the maximum principle needs this. Theorem 78 and everything over it take \(u\) valued in a fixed inner product space — the trivial bundle \(M\times V\). Its touching-point hypothesis quantifies over a direction \(n \in V\) and speaks of the function \(x \mapsto \langle n, u(t,x)\rangle \), which only makes sense because \(n\) is the same vector at every point. On a genuine bundle the direction lives in one fibre, \(n \in V_{x_0}\), and \(\langle n, u(t,x)\rangle \) is meaningless for \(x \ne x_0\). Hamilton’s fix is to spread \(n\) into a section; the Laplacian of \(x \mapsto \langle n(x), u(t,x)\rangle \) then acquires corrections in \(\nabla n\) and \(\Delta n\), and the argument closes exactly when both vanish at \(x_0\).
No parallel transport, and no exponential map. The textbook construction transports \(n\) along radial geodesics, which would put this behind the regularity of \(\exp \) — an open ODE-theory gap. It is not needed: only first-order agreement at a single point is wanted, and that is linear algebra. Take any extension \(\tilde N\), set \(A = \nabla \tilde N(x)\), and subtract \(\sum _i f_i \cdot W_i\) where the \(W_i\) are global sections through an orthonormal basis of \(T_xM\) and \(f_i(x) = 0\) with \(df_i(x)\) the matching component of \(-A\). Leibniz then leaves \(\nabla (f_i W_i)(x) = df_i(x) \otimes W_i(x)\).
An orthonormal basis is what makes it cheap. Against a local frame the components of \(A\) would have to be produced as continuous functionals by inverting a basis; against an orthonormal basis they are \(u \mapsto \langle b_i, Au\rangle \), a CLM by construction. So no frame, no trivialisation, no exists_frame_on_open: Lemma 10 applied to each \(b_i\) is all the geometry used.
The enabling step is exists_contMDiff_fun_mvfderiv_eq: a global \(C^k\) function vanishing at \(x\) with prescribed differential there. The chart supplies the one fact needed — its differential at the base point is invertible — so composing a functional with that inverse solves for the model-space covector, and a bump globalises without touching the germ.
The second-order bricks are proved too, and they are the analytic content of \(\Delta N(x) = 0\): hessian_smul_of_vanishing says that at a point where \(f\) and \(df\) both vanish, \(\nabla ^2(f\cdot W) = (\nabla ^2 f)\cdot W\) — Leibniz produces three corrections beyond the leading term and each carries a factor \(f(x)\) or \(df(x)\), so all three die, and by the same token \(\nabla (f\cdot W)(x) = 0\), which is what lets a second-order correction be added without disturbing the first-order condition already arranged above. And hessianFun_half_sq computes the Hessian of a half-square: \(\nabla ^2(\tfrac 12 a g^2)(x) = a\, dg \otimes dg\) at a zero of \(g\). A half-square is the cheapest function with value \(0\), differential \(0\) and a prescribed second derivative — both first-order conditions hold automatically since every term of \(d(g^2) = 2g\, dg\) carries a factor \(g\) — and its second derivative is rank one. Tracing against an orthonormal basis with \(dg = \langle b_i,\cdot \rangle \) gives \(\Delta = a\), because \(\sum _j \langle b_i, b_j\rangle ^2 = 1\): no chart-side second-derivative transport appears anywhere in the construction, which is what keeps this step the same size as the first-order one.
And the full statement is assembled (exists_contMDiff_section_normal): for every \(v \in T_xM\) there is a global \(C^2\) section \(N\) with \(N(x) = v\), \(\nabla N(x) = 0\) and \(\Delta N(x) = 0\). The two stages do not interact. Take \(N_1\) from the first-order statement, then add \(\sum _i (a_i/2)\, g_i^2 \cdot W_i\) with \(dg_i(x) = \langle b_i,\cdot \rangle \) and \(a_i = -\langle b_i, \Delta N_1(x)\rangle \); each summand vanishes to second order at \(x\), so it disturbs neither the value nor the covariant derivative already arranged, while contributing \(a_i\, \langle b_i,\cdot \rangle ^{\otimes 2}\cdot b_i\) to the Hessian. Tracing collapses \(\sum _j \langle b_i,b_j\rangle ^2\) to \(1\), so the correction’s Laplacian is \(\sum _i a_i b_i = -\Delta N_1(x)\) by \(\mathtt{sum\_ repr'}\).
The frame is the same family \(W_i\) used for the correction, globalised through Lemma 10 rather than taken as FiberBundle.extend: the latter is regular only near \(x\), while contMDiff_cov_apply — which supplies every differentiability hypothesis in the proof — is a global statement. Reusing the correction’s own sections as the frame is what makes that free.
Supporting: cov_sum_section_apply (\(\nabla \) over a finite sum, from the \(\nabla \)-Leibniz rule at unit coefficients), hessian_add_section and hessian_sum_section (\(\nabla ^2\) additive in its section slot). In those the \(Y\) slot is touched only at \(x\), so its hypotheses are pointwise; the sections need \(\forall y\), because the inner section \(y \mapsto \nabla _Y Z(y)\) has to be split as a function before \(\nabla \) is applied to it.
So the obstruction before Lemma 90 is no longer a missing primitive. What is left is to run the touching-point argument of Theorem 78 against a section rather than a constant vector, which this lemma is exactly what makes possible.
For a connection \(\nabla \) on a vector bundle \(V \to M\) and a connection \(\nabla ^{T}\) on \(TM\), the second covariant derivative of a section \(\sigma \) of \(V\) is \(\nabla ^2_{X,Y}\sigma = \nabla _X(\nabla _Y \sigma ) - \nabla _{\nabla ^T_X Y}\sigma \); it is tensorial in \(X\) and in \(Y\), hence a bilinear map \(T_xM\times T_xM\to V_x\), and its metric trace over an orthonormal basis of \(T_xM\) is the rough Laplacian \(\Delta \sigma (x) \in V_x\), independent of the basis.
Proved (BundleHessian.lean). The proofs are those of Hessian.lean with the section slot moved off \(TM\); the only new brick is mdiffAt_cov_apply_section, which is the observation that \(y \mapsto \nabla \sigma (y)\) is a section of \(\mathrm{Hom}(TM, V)\) — precisely what the class ContMDiffCovariantDerivative asserts to be \(C^1\).
Two connections appear and they are genuinely different: \(\nabla \) on \(V\), which is what gets differentiated, and \(\nabla ^T\) on \(TM\), which supplies the correction \(-\nabla _{\nabla ^T_X Y}\sigma \). Tensoriality in \(Y\) is the cancellation between the two Leibniz rules — \(\nabla _X(f\, \nabla _Y\sigma )\) against \(\nabla _{\nabla ^T_X(fY)}\sigma \) — and needs both.
Nothing here asks \(V\) for a norm, and that is what makes \(TM\) a case of it. The fibres carry only mathlib’s standard general-bundle binders, and \(\mathrm{hessianSection}\), its bilinear packaging and \(\Delta \) all agree with Hessian.lean’s by rfl. The trace survives the loss of the norm because OrthonormalBasis.sum_apply_self_eq needs nothing metric in its codomain — it is an algebraic rearrangement of a finite sum, with no estimate anywhere — so only the slot being traced, \(T_xM\), needs an inner product, and that one is unambiguous.
A fibre norm would have broken the specialisation, and not for a plumbing reason. \(T_xM\) reduces to the model space \(E\), so \(E\)’s own norm typechecks as a fibre norm while instance search returns the Riemannian metric’s, and those are genuinely different norms on one type. (Mathlib’s scoped priority-\(80\) RiemannianBundle instances exist precisely to keep them apart.) Dropping the norm removes the choice rather than resolving it; where a fibre metric is genuinely needed — Lemmas 82 and 83 — it is taken as a RiemannianBundle instance, which at \(V = TM\) is the very instance the tangent-bundle files use, so the specialisation survives there too.
For a metric connection \(\nabla \) on \(V\) and any connection \(\nabla ^T\) on \(TM\),
hence \(\Delta |\sigma |^2 \ge 2\langle \Delta \sigma ,\sigma \rangle \).
Proved (BundleBochner.lean), with no change to the argument: metric compatibility twice, the Hessian’s correction \(-(\nabla ^T_X Y)\langle \sigma ,\tau \rangle \) expanding into exactly the two corrections that turn the iterated derivatives into \(\nabla ^2\sigma \) and \(\nabla ^2\tau \). Mathlib’s IsMetricCompatible.mvfderiv_inner_eq is already general, and the (V := …) annotations Theorem 47 needs against lean4#14949 are unnecessary here: the fibre instances are binders, so there is nothing to see through. \(\nabla ^T\) is required to be neither metric nor torsion-free.
\(TM\) is a case of it, and that is a check rather than a tidiness. Until the bridge existed the general identity had no instantiations at all, and an unfalsified general theorem is a liability: nothing tested that it says what it is meant to say. laplacianFun_inner_eq_of_bundle derives Theorem 47 from this one, and a one-line rfl forces the two constants’ types to be definitionally equal, so "the same statement" is checked and not asserted.
What it is for. The maximum principle tests the scalar \(y \mapsto \langle N(y), u(t,y)\rangle \) for a section \(N\) spreading the direction \(n\). At a normal \(N\) — \(\nabla N(x) = 0\) and \(\Delta N(x) = 0\) — this identity collapses to \(\langle N(x), \Delta u(x)\rangle \), which is the whole reason Lemma 83 is wanted.
For every \(v \in V_x\) there is a global \(C^2\) section \(N\) of \(V\) with \(N(x) = v\), \(\nabla N(x) = 0\) and \(\Delta N(x) = 0\).
Proved (BundleNormalSection.lean). The construction is that of Lemma 80 one bundle up, and still uses no parallel transport and no exponential map.
One thing changes, and the general case is the simpler one. In the tangent case the family \(W_i\) of correction sections and the frame the Laplacian is traced over are the same family, and the second-order step reads \(\sum _j \langle b_i,b_j\rangle ^2 = 1\) off orthonormality of that one basis. Here they live in different bundles: the corrections run through an orthonormal basis of \(V_x\), the trace over one of \(T_xM\). What replaces the identity is that a single function \(g\) suffices — tracing \(\nabla ^2(\tfrac 12 a g^2)(x) = a\, dg\otimes dg\) gives \(a\sum _j dg(E_j)^2\), which is \(a\) as soon as \(dg(x)\) is a unit covector on \(T_xM\) — so taking \(dg(x) = \langle E_{j_0},\cdot \rangle \) for any one frame vector corrects every component at once, with one \(g\) rather than a family.
That leaves an edge case the tangent version never had: when \(T_xM\) is zero there is no unit covector. But then \(\Delta \) is an empty sum, so \(\Delta N_1(x) = 0\) already and \(N_1\) itself is the answer.
Lemma 80 is a case of this one, with the same rfl type check as in Lemma 82, and for the same reason.
What remains before Lemma 90 is no longer a missing primitive on the geometry side, and the touching-point step itself is now Lemma 84. What is left is the cross-fibre half of the first-touching-time argument: on a bundle the target is a family \(K_x \subseteq V_x\) of convex sets, and the argument compares \(\mathrm{dist}(u(t,x), K_x)\) across different fibres. Making that comparison is what a trivialisation — Uhlenbeck’s trick, or Hamilton’s moving fibre metric — is for, and it is the one thing none of the machinery above supplies.
Let \(u\) be a \(C^2\) section of \(V\) and \(x \in M\). For every direction \(n \in V_x\) there is a global \(C^2\) section \(N\) of \(V\) with \(N(x) = n\) such that
consequently, if \(x\) is a spatial maximum of \(y \mapsto \langle N(y), u(y)\rangle \) then \(\langle n, \Delta u(x)\rangle \le 0\).
Proved (BundleMaximumPrinciple.lean). This is the step at which the tensor maximum principle inspects the Laplacian, transposed from a trivial bundle — where the tested direction is literally the same vector at every point — to a bundle where \(n\) lives in one fibre only.
Both correction terms die on \(\nabla N(x) = 0\), which is why the second-order condition \(\Delta N(x) = 0\) of Lemma 83 is not a luxury: in the Bochner expansion of Lemma 82 the gradient pairing \(2\sum _i\langle \nabla _{e_i}N,\nabla _{e_i}u\rangle \) vanishes term by term on the first-order condition, and \(\langle \Delta N, u\rangle \) vanishes on the second. What is left is a statement about the scalar \(\langle N, u\rangle \), and the second-derivative test of Lemma 60 closes it — in the maximum form \(\Delta f(x_0) \le 0\), which is the minimum form applied to \(-f\).
No parallel transport and no exponential map appear, and that is the point of routing through Lemma 83: only the first- and second-order behaviour of \(N\) at the single point \(x\) matters. The radial-transport construction of a normal frame would have put this step behind the regularity of \(\exp \), which is an open gap in ODE theory.
Boundarylessness of the model enters exactly once, in the second-derivative test; the connection \(\nabla ^T\) on \(TM\) need be neither metric nor torsion-free.
Let \(K_t \subseteq V\) be a family of closed convex nonempty sets that is monotone, \(s \le t \Rightarrow K_s \subseteq K_t\), and varies continuously in the sense that \((t,v) \mapsto \operatorname {dist}(v, K_t)\) is jointly continuous. If \(u\) solves \(\partial _t u = \Delta _{g_t} u + F_t(u)\) and each \(K_t\) is preserved by \(\dot v = F_t(v)\) in Nagumo’s form, then \(u(0,\cdot ) \in K_0\) gives \(u(t,\cdot ) \in K_t\) for all \(t \in [0,T]\).
Proved (TensorMaximumPrinciple.lean, ManifoldMaximumPrinciple.lean, TensorPreservation.lean), abstractly, on a closed manifold, and with the metric moving as well.
Monotonicity is the whole cost, and it is felt in exactly one place. The nearest point and the outward normal are taken in \(K_{t_0}\), at the single first-touching time, so every step at \(t_0\) is the fixed-set argument verbatim. What is new is that the earlier times are controlled against \(K_t\) rather than \(K_{t_0}\), so the two must be compared — and \(K_t \subseteq K_{t_0}\) for \(t \le t_0\) gives \(\operatorname {dist}(v,K_{t_0}) \le \operatorname {dist}(v,K_t)\) for free. The continuity hypothesis is stated directly on \(\operatorname {dist}(v, K_t)\), which is the form the proof consumes, rather than as a Hausdorff-distance condition whose \(\mathtt{ENNReal}\) API would have to be unpacked again.
The other direction is genuinely not free. A shrinking family needs a quantitative bound on how fast \(K_t\) retreats, coupled to \(F\): a set closing in faster than the reaction pushes points inward is simply not preserved, so no hypothesis-free statement exists there. Hamilton 1999’s \(\log (1+t)\) improvement is of that kind.
Why this is more than the \(\log (1+t)\) improvement it was filed under. A moving inner product on \(V\) reduces to a moving set. If \(\langle v,w\rangle _t = \langle P_t v, w\rangle \) with \(P_t\) positive self-adjoint and \(S_t = P_t^{1/2}\), then \(S_t\) is an isometry from \((V, \langle \cdot ,\cdot \rangle _t)\) to \((V, \langle \cdot ,\cdot \rangle )\), and \(u(t,x) \in K\) is \(S_t u(t,x) \in S_t(K)\) — a fixed-metric problem with a moving set. Uhlenbeck’s trick is precisely the choice of \(S_t\) that makes \(S_t(K)\) constant. So this theorem and Uhlenbeck’s trick are two ways of paying the same bill, and the monotone case is the part of it that costs nothing.
What this does not close. The obstruction before the curvature operator is now not the principle but its input: \(u\) takes values in a fixed inner product space, i.e. a trivial bundle \(M \times V\), whereas the curvature operator is a section of \(\mathrm{Sym}^2(\Lambda ^2 TM)\). The maximum principle for sections of a non-trivial bundle is not in this repo at all, and is a prerequisite for either route.
A bound on \(|\operatorname {Rm}|\) on a parabolic cylinder gives interior bounds on every covariant derivative \(|\nabla ^k \operatorname {Rm}|\), with constants depending only on \(k\), the dimension, and the geometry of the cylinder.
The flow extends past \(T\) if and only if \(|\operatorname {Rm}|\) stays bounded on \([0,T)\). Singularities are exactly curvature blow-ups.
The flow recast as a single geometric object: a space-time with a time function and a horizontal metric satisfying the flow equation, rather than a one-parameter family of metrics on a fixed manifold. (Morgan–Tian 3.8.)
Introduced long before surgery and load-bearing for it. Because the time-slices are allowed to change topology, surgery becomes an equation on one object rather than a procedure applied between objects — which is exactly what makes it a plausible formalization target at all.