Almost-everywhere energy and moment variation for building-valued harmonic maps

Open

HarmonicBuilding.weakFirstVariationData

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

first-variationfrequency-functionharmonic-mapskorevaar-schoen

Let $u$ be a continuous, nonconstant Korevaar-Schoen energy-minimizing map from a connected Riemann-surface domain to a complete Euclidean building. Fix a point where the canonical small-radius energy is finite and the boundary moment is positive. In the preferred complex coordinate, let $E(r)$ be the energy in the radius- $r$ ball and $I(r)$ the arclength integral of the squared distance from the central value.

There is $r_0>0$ , and real functions $J,F$ on the radii, such that $E$ and $I$ are absolutely continuous on every compact subinterval of $(0,r_0)$ and, for almost every such radius,

I'(r)=\frac{I(r)}r+2J(r),\qquad E'(r)=2F(r),\qquad E(r)\leq J(r),\qquad J(r)^2\leq I(r)F(r).

Here $J$ and $F$ encode the boundary radial flux and radial energy. These data supply the analytic input for the two-dimensional frequency monotonicity formula.

Formalization Note. The energy and boundary moment are the canonical functions already defined in the harmonic-building interface. No differentiability at exceptional radii is asserted.

Preamble

import Definitions.Def_frame_2026_harmonic_building_interfaces

open HarmonicBuilding Set MeasureTheory Filter
open scoped Manifold
set_option autoImplicit false

Formal statement

theorem HarmonicBuilding.weakFirstVariationData
    {N : ℕ} (C : EuclideanCoxeterData N)
    {X S : Type*}
    [MetricSpace X] [CompleteSpace X] [MeasurableSpace X] [BorelSpace X]
    [TopologicalSpace S] [T2Space S] [SecondCountableTopology S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (B : EuclideanBuildingData N C X)
    (D : RiemannSurfaceDomain S) (u : S → X) (x₀ : D.Point)
    (hu : IsKSHarmonic D u) (hnc : NonconstantOn u D.carrier)
    (hdef : OrderDefinedAt D u x₀) :
    let E : ℝ → ℝ := fun r => scaleEnergy (coordinateDomainAt D (x₀ : S))
      (coordinateMapAt u (x₀ : S)) (coordinateCenter (x₀ : S)) r
    let I : ℝ → ℝ := fun r => (boundaryMoment (coordinateMapAt u (x₀ : S))
      (coordinateCenter (x₀ : S)) r).toReal
    ∃ r₀ : ℝ, 0 < r₀ ∧ ∃ J F : ℝ → ℝ,
      (∀ a b : ℝ, 0 < a → a ≤ b → b < r₀ →
        AbsolutelyContinuousOnInterval E a b ∧ AbsolutelyContinuousOnInterval I a b) ∧
      ∀ᵐ r : ℝ, r ∈ Set.Ioo (0 : ℝ) r₀ →
        HasDerivAt I (I r / r + 2 * J r) r ∧
        HasDerivAt E (2 * F r) r ∧ E r ≤ J r ∧ J r ^ 2 ≤ I r * F r := by sorry

Source

Gromov and Schoen, Harmonic maps into singular spaces and p-adic superrigidity for lattices in groups of rank one, IHES Publ. Math. 76 (1992), Section 2, Proposition 2.2 and equations (2.2)-(2.5), printed pp. 191-194: https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/785.pdf. The calculus statement below is the two-dimensional scalar consequence, with the radial flux retained as a separate function. For the Euclidean-building setting and the canonical frequency, see Breiner and Ben K. Dees, On the Possible Orders of Harmonic Maps into Euclidean Buildings, arXiv:2604.16608v1, Sections 2.3-2.4: https://arxiv.org/html/2604.16608v1. This statement packages the weak variation data, rather than an everywhere differentiable identity.

View graph