Euclidean-building harmonic-map order interfaces

import Mathlib

/-!
# Canonical foundations for harmonic maps into Euclidean buildings

The definitions in this file contain no user-supplied Sobolev predicate,
energy density, volume measure, boundary measure, or frequency function.
The source is a one-dimensional complex manifold, the Coxeter groups act by
concrete affine/linear isometries, and the analytic quantities are fixed by a
normalized Korevaar--Schoen difference-quotient construction in complex
coordinates.

The normalization `4 / (pi * epsilon^4)` is the two-dimensional normalization:
for a smooth Euclidean-valued map the approximate density converges to the
usual squared Hilbert--Schmidt norm of its derivative.
-/

namespace HarmonicBuilding

open MeasureTheory
open scoped ENNReal Manifold

/-! ## Riemann surfaces -/

/-- A domain in a Riemann surface.  The ambient instances say that `S` is a
Hausdorff, second-countable, one-complex-dimensional smooth manifold. -/
structure RiemannSurfaceDomain (S : Type*) [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S] where
  carrier : Set S
  isOpen_carrier : IsOpen carrier
  isConnected_carrier : IsConnected carrier

/-- Points of a Riemann-surface domain. -/
abbrev RiemannSurfaceDomain.Point {S : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (D : RiemannSurfaceDomain S) := D.carrier

/-- The whole complex plane is an explicit inhabited example of the source
geometry; the domain interface is therefore not empty by construction. -/
def complexPlaneDomain : RiemannSurfaceDomain ℂ where
  carrier := Set.univ
  isOpen_carrier := isOpen_univ
  isConnected_carrier := isConnected_univ

/-- A map is genuinely nonconstant on the specified domain. -/
def NonconstantOn {S X : Type*} (u : S → X) (D : Set S) : Prop :=
  ∃ x ∈ D, ∃ y ∈ D, u x ≠ u y

/-! ## Concrete Euclidean Coxeter data -/

/-- The model apartment `E^N`. -/
abbrev ModelEuclideanSpace (N : ℕ) := EuclideanSpace ℝ (Fin N)

/-- The full group of affine isometries of the model apartment. -/
abbrev EuclideanIsometryGroup (N : ℕ) :=
  ModelEuclideanSpace N ≃ᵃⁱ[ℝ] ModelEuclideanSpace N

/-- The full orthogonal group of the translation vector space. -/
abbrev OrthogonalGroup (N : ℕ) :=
  ModelEuclideanSpace N ≃ₗᵢ[ℝ] ModelEuclideanSpace N

/-- A linear isometry is reflection in the hyperplane perpendicular to a
nonzero normal vector. -/
def IsLinearReflection {N : ℕ} (g : OrthogonalGroup N) : Prop :=
  ∃ n : ModelEuclideanSpace N, n ≠ 0 ∧
    ∀ x : ModelEuclideanSpace N,
      g x = x - (2 * (inner ℝ x n / inner ℝ n n)) • n

/-- An affine isometry is a reflection when it has a fixed point and its
linear part is a hyperplane reflection. -/
def IsAffineReflection {N : ℕ} (g : EuclideanIsometryGroup N) : Prop :=
  (∃ p : ModelEuclideanSpace N, g p = p) ∧
    IsLinearReflection g.linearIsometryEquiv

/-- A Euclidean Coxeter complex represented inside the actual affine and
orthogonal isometry groups of `E^N`.  Surjectivity together with
`rotationalPart_value` makes `weyl` exactly the rotational image; it cannot be
an unrelated finite group.  The affine group is required to be generated by a
nonempty set of genuine affine reflections. -/
structure EuclideanCoxeterData (N : ℕ) where
  positive_rank : 0 < N
  affineWeyl : Subgroup (EuclideanIsometryGroup N)
  weyl : Subgroup (OrthogonalGroup N)
  instFintypeWeyl : Fintype weyl
  rotationalPart : affineWeyl →* weyl
  rotationalPart_value : ∀ g : affineWeyl,
    ((rotationalPart g : weyl) : OrthogonalGroup N) =
      (g : EuclideanIsometryGroup N).linearIsometryEquiv
  rotationalPart_surjective : Function.Surjective rotationalPart
  simpleReflections : Set affineWeyl
  simpleReflections_nonempty : simpleReflections.Nonempty
  simple_are_affine_reflections : ∀ g ∈ simpleReflections,
    IsAffineReflection (g : EuclideanIsometryGroup N)
  simple_generates : Subgroup.closure simpleReflections = ⊤

attribute [instance] EuclideanCoxeterData.instFintypeWeyl

/-! ## Metric Euclidean buildings -/

/-- An apartment chart is an isometric embedding of the model apartment. -/
structure ApartmentChart (E X : Type*) [PseudoMetricSpace E]
    [PseudoMetricSpace X] where
  toFun : E → X
  isometry : Isometry toFun

instance {E X : Type*} [PseudoMetricSpace E] [PseudoMetricSpace X] :
    CoeFun (ApartmentChart E X) (fun _ ↦ E → X) :=
  ⟨ApartmentChart.toFun⟩

/-- A unit-interval constant-speed geodesic segment. -/
def IsConstantSpeedSegment {X : Type*} [PseudoMetricSpace X]
    (gamma : ℝ → X) (x y : X) : Prop :=
  gamma 0 = x ∧ gamma 1 = y ∧
    ∀ s ∈ Set.Icc (0 : ℝ) 1, ∀ t ∈ Set.Icc (0 : ℝ) 1,
      dist (gamma s) (gamma t) = |s - t| * dist x y

/-- An isometrically parametrized geodesic line. -/
def IsGeodesicLine {X : Type*} [PseudoMetricSpace X] (gamma : ℝ → X) : Prop :=
  ∀ s t : ℝ, dist (gamma s) (gamma t) = |s - t|

/-- An isometrically parametrized geodesic ray on nonnegative times. -/
def IsGeodesicRay {X : Type*} [PseudoMetricSpace X] (gamma : ℝ → X) : Prop :=
  ∀ s t : ℝ, 0 ≤ s → 0 ≤ t →
    dist (gamma s) (gamma t) = |s - t|

/-- The CAT(0) CN inequality, together with geodesic existence. -/
def IsCATZero (X : Type*) [PseudoMetricSpace X] : Prop :=
  (∀ x y : X, ∃ gamma : ℝ → X, IsConstantSpeedSegment gamma x y) ∧
  ∀ x y z : X, ∀ gamma : ℝ → X,
    IsConstantSpeedSegment gamma x y →
      ∀ t ∈ Set.Icc (0 : ℝ) 1,
        dist (gamma t) z ^ 2 ≤
          (1 - t) * dist x z ^ 2 + t * dist y z ^ 2 -
            t * (1 - t) * dist x y ^ 2

/-- Two apartment charts have a transition map in the concrete affine Weyl
group on their entire overlap. -/
def ChartsCompatible {n : ℕ} {X : Type*} [PseudoMetricSpace X]
    (C : EuclideanCoxeterData n)
    (c₁ c₂ : ApartmentChart (ModelEuclideanSpace n) X) : Prop :=
  ∃ w : C.affineWeyl, ∀ p q : ModelEuclideanSpace n,
    c₁ p = c₂ q → (w : EuclideanIsometryGroup n) q = p

/-- A Kleiner--Leeb style metric Euclidean building realization.  Besides
CAT(0), pair coverage and Weyl-compatible overlaps, rays and lines lie in
apartments and the atlas is maximal among compatible charts. -/
structure EuclideanBuildingData (N : ℕ) (C : EuclideanCoxeterData N)
    (X : Type*) [MetricSpace X] [CompleteSpace X] where
  atlas : Set (ApartmentChart (ModelEuclideanSpace N) X)
  pair_mem_apartment : ∀ x y : X,
    ∃ chart ∈ atlas, x ∈ Set.range chart.toFun ∧ y ∈ Set.range chart.toFun
  ray_mem_apartment : ∀ gamma : ℝ → X, IsGeodesicRay gamma →
    ∃ chart ∈ atlas,
      gamma '' Set.Ici (0 : ℝ) ⊆ Set.range chart.toFun
  line_mem_apartment : ∀ gamma : ℝ → X, IsGeodesicLine gamma →
    ∃ chart ∈ atlas, Set.range gamma ⊆ Set.range chart.toFun
  overlap_compatible : ∀ c₁ ∈ atlas, ∀ c₂ ∈ atlas,
    ChartsCompatible C c₁ c₂
  maximal_atlas : ∀ c : ApartmentChart (ModelEuclideanSpace N) X,
    (∀ a ∈ atlas, ChartsCompatible C c a) → c ∈ atlas
  catZeroComparison : IsCATZero X

/-! ## Canonical two-dimensional Korevaar--Schoen energy -/

/-- The normalized two-dimensional metric difference-quotient density. -/
noncomputable def ksApproxEnergyDensity {X : Type*} [PseudoMetricSpace X]
    (Omega : Set ℂ) (u : ℂ → X) (epsilon : ℝ) (z : ℂ) : ENNReal :=
  ENNReal.ofReal (4 / (Real.pi * epsilon ^ 4)) *
    ∫⁻ w in Omega ∩ Metric.ball z epsilon,
      ENNReal.ofReal (dist (u w) (u z) ^ 2)

/-- Approximate energy on `U`, using the fixed Lebesgue area on `ℂ`. -/
noncomputable def ksApproxEnergy {X : Type*} [PseudoMetricSpace X]
    (Omega U : Set ℂ) (u : ℂ → X) (epsilon : ℝ) : ENNReal :=
  ∫⁻ z in U ∩ Omega,
    ksApproxEnergyDensity (U ∩ Omega) u epsilon z

/-- The Korevaar--Schoen energy is the lower small-scale envelope of the
normalized approximate energies. -/
noncomputable def ksEnergy {X : Type*} [PseudoMetricSpace X]
    (Omega U : Set ℂ) (u : ℂ → X) : ENNReal :=
  Filter.liminf (fun epsilon : ℝ ↦ ksApproxEnergy Omega U u epsilon)
    (nhdsWithin 0 (Set.Ioi 0))

/-- Canonical local metric `W^{1,2}` membership: Borel measurability on the
coordinate domain, metric-valued `L²` integrability, and finite normalized KS
energy on `U`.  The existential point is only the standard base point used to
define metric-valued `L²`; changing it does not change the condition. -/
def IsKSSobolevOn {X : Type*} [PseudoMetricSpace X] [MeasurableSpace X]
    (Omega U : Set ℂ) (u : ℂ → X) : Prop :=
  AEMeasurable u (volume.restrict Omega) ∧
    (∃ q : X,
      (∫⁻ z in U ∩ Omega, ENNReal.ofReal (dist (u z) q ^ 2)) < ⊤) ∧
    ksEnergy Omega U u < ⊤

/-- The standard angular parametrization of a Euclidean coordinate circle. -/
noncomputable def circlePoint (z : ℂ) (r theta : ℝ) : ℂ :=
  z + (r : ℂ) * Complex.exp ((theta : ℂ) * Complex.I)

/-- Normalized squared distance in an interior collar of a circle.  Unlike a
pointwise restriction, this is unchanged by altering Sobolev representatives
on an area-null set. -/
noncomputable def annularTraceDistance {X : Type*} [PseudoMetricSpace X]
    (u v : ℂ → X) (z : ℂ) (R delta : ℝ) : ENNReal :=
  ENNReal.ofReal (1 / delta) *
    ∫⁻ w in {w : ℂ | R - delta < dist w z ∧ dist w z < R},
      ENNReal.ofReal (dist (u w) (v w) ^ 2)

/-- Equality of Sobolev traces on a coordinate circle, defined canonically by
vanishing normalized `L²` distance in shrinking interior collars. -/
def SameKSTraceOnCircle {X : Type*} [PseudoMetricSpace X]
    (u v : ℂ → X) (z : ℂ) (R : ℝ) : Prop :=
  Filter.Tendsto (fun delta : ℝ ↦ annularTraceDistance u v z R delta)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

/-- Energy minimization on one relatively compact coordinate ball. -/
def IsPlanarKSHarmonicAt {X : Type*} [PseudoMetricSpace X]
    [MeasurableSpace X] (Omega : Set ℂ) (u : ℂ → X) (z : ℂ) : Prop :=
  z ∈ Omega ∧ ∃ R : ℝ, 0 < R ∧ Metric.closedBall z R ⊆ Omega ∧
    IsKSSobolevOn Omega (Metric.ball z R) u ∧
    ∀ v : ℂ → X,
      IsKSSobolevOn Omega (Metric.ball z R) v →
      SameKSTraceOnCircle u v z R →
      ksEnergy Omega (Metric.ball z R) u ≤
        ksEnergy Omega (Metric.ball z R) v

/-! ## Pullback to canonical complex coordinates -/

/-- The part of a Riemann-surface domain seen in the preferred extended chart
at `x`. -/
noncomputable def coordinateDomainAt {S : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (D : RiemannSurfaceDomain S) (x : S) : Set ℂ :=
  extChartAt (modelWithCornersSelf ℂ ℂ) x ''
    (D.carrier ∩ (extChartAt (modelWithCornersSelf ℂ ℂ) x).source)

/-- A map written in the preferred complex chart at `x`. -/
noncomputable def coordinateMapAt {S X : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    (u : S → X) (x : S) : ℂ → X :=
  fun z ↦ u ((extChartAt (modelWithCornersSelf ℂ ℂ) x).symm z)

/-- The coordinate of the distinguished surface point. -/
noncomputable def coordinateCenter {S : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] (x : S) : ℂ :=
  extChartAt (modelWithCornersSelf ℂ ℂ) x x

/-- A KS-energy-minimizing harmonic map on a Riemann-surface domain.  The
quantification over every point makes this independent of any caller-selected
energy or Sobolev predicate. -/
def IsKSHarmonic {S X : Type*} [TopologicalSpace S] [ChartedSpace ℂ S]
    [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    [PseudoMetricSpace X] [MeasurableSpace X]
    (D : RiemannSurfaceDomain S) (u : S → X) : Prop :=
  ContinuousOn u D.carrier ∧
    ∀ x ∈ D.carrier,
      IsPlanarKSHarmonicAt (coordinateDomainAt D x) (coordinateMapAt u x)
        (coordinateCenter x)

/-- Canonical boundary moment, with the factor `r` giving arclength measure. -/
noncomputable def boundaryMoment {X : Type*} [PseudoMetricSpace X]
    (u : ℂ → X) (z : ℂ) (r : ℝ) : ENNReal :=
  ENNReal.ofReal r *
    ∫⁻ theta in Set.Icc (0 : ℝ) (2 * Real.pi),
      ENNReal.ofReal
        (dist (u (circlePoint z r theta)) (u z) ^ 2)

/-- Scale energy on a coordinate ball, converted to a real after finiteness. -/
noncomputable def scaleEnergy {X : Type*} [PseudoMetricSpace X]
    (Omega : Set ℂ) (u : ℂ → X) (z : ℂ) (r : ℝ) : ℝ :=
  (ksEnergy Omega (Metric.ball z r) u).toReal

/-- The canonical frequency quotient `r E_u(z,r) / I_u(z,r)`. -/
noncomputable def frequencyQuotient {X : Type*} [PseudoMetricSpace X]
    (Omega : Set ℂ) (u : ℂ → X) (z : ℂ) (r : ℝ) : ℝ :=
  r * scaleEnergy Omega u z r / (boundaryMoment u z r).toReal

/-- The surface frequency in the preferred complex coordinate at `x`. -/
noncomputable def surfaceFrequency {S X : Type*} [TopologicalSpace S]
    [ChartedSpace ℂ S] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    [PseudoMetricSpace X] (D : RiemannSurfaceDomain S) (u : S → X)
    (x : S) (r : ℝ) : ℝ :=
  frequencyQuotient (coordinateDomainAt D x) (coordinateMapAt u x)
    (coordinateCenter x) r

/-- The order of `u` at `x` is `alpha` precisely when the canonical frequency
has that limit through positive radii. -/
def HasOrderAt {S X : Type*} [TopologicalSpace S] [ChartedSpace ℂ S]
    [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    [PseudoMetricSpace X] (D : RiemannSurfaceDomain S) (u : S → X)
    (x : S) (alpha : ℝ) : Prop :=
  Filter.Tendsto (surfaceFrequency D u x)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds alpha)

/-- At sufficiently small positive scales the coordinate ball stays in the
domain, its KS energy is finite, and the canonical circle moment is positive.
This is a conclusion to be proved for nonconstant harmonic maps, not an input
energy-interface hypothesis. -/
def OrderDefinedAt {S X : Type*} [TopologicalSpace S] [ChartedSpace ℂ S]
    [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ S]
    [PseudoMetricSpace X] (D : RiemannSurfaceDomain S) (u : S → X)
    (x : S) : Prop :=
  ∃ r₀ : ℝ, 0 < r₀ ∧ ∀ r : ℝ, 0 < r → r < r₀ →
    Metric.closedBall (coordinateCenter x) r ⊆ coordinateDomainAt D x ∧
    ksEnergy (coordinateDomainAt D x) (Metric.ball (coordinateCenter x) r)
      (coordinateMapAt u x) < ⊤ ∧
    0 < (boundaryMoment (coordinateMapAt u x) (coordinateCenter x) r).toReal

/-- Rank one means apartment dimension one. -/
def IsRankOne (N : ℕ) : Prop := N = 1

/-- The complete source proposition, separated from the open theorem so it can
be published first as a Prove2me definition item.  The paper's tangent-map
reduction is stated for nonconstant maps; this hypothesis is made explicit so
that the constant-map `0 / 0` frequency is not silently assigned an order.
The existence of the order and positivity of its small-scale denominator are
part of the conclusion, rather than assumptions supplied to the solver. -/
def PossibleOrdersProblem
    {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) : Prop :=
  IsKSHarmonic D u →
  NonconstantOn u D.carrier →
    OrderDefinedAt D u x₀ ∧
      (∃ m k : ℕ, 0 < m ∧ 0 < k ∧ k ≤ m ∧
        k ∣ Fintype.card C.weyl ∧
        HasOrderAt D u x₀ ((m : ℝ) / (k : ℝ))) ∧
      (IsRankOne N →
        ∃ m : ℕ, 2 ≤ m ∧
          HasOrderAt D u x₀ ((m : ℝ) / 2))

end HarmonicBuilding