5.8. Mathlib candidates: symmetric spaces and the Helgason--Fourier transform🔗

The Helgason--Fourier transform on a noncompact symmetric space X = G/K: an abstract layer that carries the geometry — the composite distance, the constant ϱ, the invariant and boundary measures, and the Harish-Chandra c-function — as data, so that the inversion formula is a definite proposition rather than an axiom; and the two concrete models the layer is instantiated at, the Poincaré ball model of real hyperbolic space and the manifold of positive definite matrices in Terras' coordinates.

The abstract layer, with the geometry as data

Theorem5.8.1

uses 0

Used by 5

Reverse dependency previews

Preview

Theorem 5.8.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Helgason--Fourier transform, with the geometry as data. On a noncompact symmetric space X=G/K the plane wave e^{-i\langle\lambda,x\rangle} of \mathbb R^m is replaced by e^{(-i\lambda+\varrho)(A(x,b))}, where A(x,b)\in\mathfrak a\cong\mathbb R^r is the composite distance from the origin to the horosphere through x with normal b\in B=K/M, and \varrho is the half-sum of the positive restricted roots. Mathlib has none of the group theory behind this — no Iwasawa decomposition, no spherical functions, no Harish-Chandra c-function — so the composite distance and \varrho enter as data, and the identities the geometry does satisfy stay hypotheses of the theorems that need them rather than fields of a structure.

Lean code for Theorem5.8.1●15 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

def SymmetricSpace.horosphericalCharacter.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (rho lam v : E) : ℂ

def SymmetricSpace.horosphericalCharacter.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (rho lam v : E) : ℂ

Implementation after :=

:=
  Complex.exp (Complex.I * ((inner ℝ lam v : ℝ) : ℂ) + ((inner ℝ rho v : ℝ) : ℂ))

The character `v ↦ e^{(iλ+ϱ)(v)}` of `𝔞`, with the functional written through the inner
product: `ϱ` and `λ` are vectors of `E ≅ 𝔞* ≅ 𝔞`.

Taking `ϱ = 0` gives the plane wave `e^{i⟪λ,v⟫}` of Euclidean Fourier analysis, and taking `λ = 0`
gives the weight `e^{ϱ(v)}` that the layer of a network on `G/K` carries.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.horosphericalCharacter_zero_right.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (rho lam : E) :
  SymmetricSpace.horosphericalCharacter rho lam 0 = 1

theorem SymmetricSpace.horosphericalCharacter_zero_right.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (rho lam : E) :
  SymmetricSpace.horosphericalCharacter
      rho lam 0 =
    1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.horosphericalCharacter_zero_rho.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam v : E) :
  SymmetricSpace.horosphericalCharacter 0 lam v =
    Complex.exp (Complex.I * ↑(inner ℝ lam v))

theorem SymmetricSpace.horosphericalCharacter_zero_rho.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (lam v : E) :
  SymmetricSpace.horosphericalCharacter 0
      lam v =
    Complex.exp
      (Complex.I * ↑(inner ℝ lam v))

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.norm_horosphericalCharacter.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (rho lam v : E) :
  ‖SymmetricSpace.horosphericalCharacter rho lam v‖ =
    Real.exp (inner ℝ rho v)

theorem SymmetricSpace.norm_horosphericalCharacter.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (rho lam v : E) :
  ‖SymmetricSpace.horosphericalCharacter
        rho lam v‖ =
    Real.exp (inner ℝ rho v)

The modulus of the character is the weight `e^{ϱ(v)}`: the frequency contributes nothing.
This is why the growth of `e^{(-iλ+ϱ)(A(x,b))}` is governed by `ϱ` alone, uniformly in `λ`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.horosphericalCharacter_ne_zero.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (rho lam v : E) :
  SymmetricSpace.horosphericalCharacter rho lam v ≠ 0

theorem SymmetricSpace.horosphericalCharacter_ne_zero.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (rho lam v : E) :
  SymmetricSpace.horosphericalCharacter
      rho lam v ≠
    0

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.horosphericalCharacter_add.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (rho lam v w : E) :
  SymmetricSpace.horosphericalCharacter rho lam (v + w) =
    SymmetricSpace.horosphericalCharacter rho lam v *
      SymmetricSpace.horosphericalCharacter rho lam w

theorem SymmetricSpace.horosphericalCharacter_add.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (rho lam v w : E) :
  SymmetricSpace.horosphericalCharacter
      rho lam (v + w) =
    SymmetricSpace.horosphericalCharacter
        rho lam v *
      SymmetricSpace.horosphericalCharacter
        rho lam w

The character is multiplicative in the `𝔞`-variable. Together with the cocycle relation
`A(g·x, g·b) = A(x,b) + A(g·o, g·b)` this is what turns the `G`-action on `X` into a multiplier on
the Helgason--Fourier kernel.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.horosphericalCharacter_eq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (rho lam v : E) :
  SymmetricSpace.horosphericalCharacter rho lam v =
    Complex.exp (Complex.I * ↑(inner ℝ lam v)) *
      ↑(Real.exp (inner ℝ rho v))

theorem SymmetricSpace.horosphericalCharacter_eq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (rho lam v : E) :
  SymmetricSpace.horosphericalCharacter
      rho lam v =
    Complex.exp
        (Complex.I * ↑(inner ℝ lam v)) *
      ↑(Real.exp (inner ℝ rho v))

The character splits into a unimodular phase and a real weight,
`e^{(iλ+ϱ)(v)} = e^{iλ(v)} \cdot e^{ϱ(v)}`. This is the form in which the Helgason--Fourier
transform is read as a Euclidean Fourier transform of a weighted transform: the phase is the plane
wave and the weight belongs to the function being transformed.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.horosphericalCharacter_neg.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (rho lam v : E) :
  SymmetricSpace.horosphericalCharacter rho (-lam) v =
    Complex.exp (-(Complex.I * ↑(inner ℝ lam v))) *
      ↑(Real.exp (inner ℝ rho v))

theorem SymmetricSpace.horosphericalCharacter_neg.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  (rho lam v : E) :
  SymmetricSpace.horosphericalCharacter
      rho (-lam) v =
    Complex.exp
        (-(Complex.I *
            ↑(inner ℝ lam v))) *
      ↑(Real.exp (inner ℝ rho v))

Reflecting the frequency conjugates the phase and leaves the weight alone.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

def SymmetricSpace.helgasonFourier.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
  (A : X → B → E) (rho : E) (f : X → ℂ) (lam : E) (b : B) : ℂ

def SymmetricSpace.helgasonFourier.{u_1, u_2,
    u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  (μ : MeasureTheory.Measure X)
  (A : X → B → E) (rho : E) (f : X → ℂ)
  (lam : E) (b : B) : ℂ

Implementation after :=

:=
  ∫ x : X, f x * horosphericalCharacter rho (-lam) (A x b) ∂μ

**The Helgason--Fourier transform** `f̂(λ,b) = ∫_X f(x) e^{(-iλ+ϱ)(A(x,b))} dμ(x)`
(Helgason, *Geometric Analysis on Symmetric Spaces*, Ch. III §1, definition (4)).

The composite distance `A`, the constant `ϱ` and the invariant measure `μ` are data.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

def SymmetricSpace.sphericalFunction.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B] (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho lam : E) (x : X) : ℂ

def SymmetricSpace.sphericalFunction.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B]
  (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho lam : E) (x : X) :
  ℂ

Implementation after :=

:=
  ∫ b : B, horosphericalCharacter rho lam (A x b) ∂nu

**The spherical function** `φ_λ(x) = ∫_B e^{(iλ+ϱ)(A(x,b))} db`, the average of the
Helgason--Fourier kernel over the boundary.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

def SymmetricSpace.helgasonInversionIntegral.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace E] [MeasurableSpace B]
  (mua : MeasureTheory.Measure E) (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho : E) (F : E → B → ℂ) (kappa : E → ℝ) (x : X) : ℂ

def SymmetricSpace.helgasonInversionIntegral.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace E]
  [MeasurableSpace B]
  (mua : MeasureTheory.Measure E)
  (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho : E)
  (F : E → B → ℂ) (kappa : E → ℝ)
  (x : X) : ℂ

Implementation after :=

:=
  ∫ lam : E, (∫ b : B, F lam b * ((kappa lam : ℝ) : ℂ) *
    horosphericalCharacter rho lam (A x b) ∂nu) ∂mua

The integral that the inversion formula asserts to be `f(x)`:
`∫_{𝔞*} ∫_B F(λ,b) κ(λ) e^{(iλ+ϱ)(A(x,b))} db dλ`.

The Plancherel density `κ` is data; on a symmetric space it is `|W|^{-1}|c(λ)|^{-2}`, built from
the order of the Weyl group and the Harish-Chandra `c`-function.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.helgasonFourier_zero.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
  (A : X → B → E) (rho lam : E) (b : B) :
  SymmetricSpace.helgasonFourier μ A rho (fun x ↦ 0) lam b = 0

theorem SymmetricSpace.helgasonFourier_zero.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  (μ : MeasureTheory.Measure X)
  (A : X → B → E) (rho lam : E) (b : B) :
  SymmetricSpace.helgasonFourier μ A rho
      (fun x ↦ 0) lam b =
    0

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.helgasonFourier_const_mul.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X] (μ : MeasureTheory.Measure X)
  (A : X → B → E) (rho : E) (c : ℂ) (f : X → ℂ) (lam : E) (b : B) :
  SymmetricSpace.helgasonFourier μ A rho (fun x ↦ c * f x) lam b =
    c * SymmetricSpace.helgasonFourier μ A rho f lam b

theorem SymmetricSpace.helgasonFourier_const_mul.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  (μ : MeasureTheory.Measure X)
  (A : X → B → E) (rho : E) (c : ℂ)
  (f : X → ℂ) (lam : E) (b : B) :
  SymmetricSpace.helgasonFourier μ A rho
      (fun x ↦ c * f x) lam b =
    c *
      SymmetricSpace.helgasonFourier μ A
        rho f lam b

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.sphericalFunction_eq_one.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B] (nu : MeasureTheory.Measure B)
  [MeasureTheory.IsProbabilityMeasure nu] (A : X → B → E) (rho lam : E)
  {x : X} (hx : ∀ (b : B), A x b = 0) :
  SymmetricSpace.sphericalFunction nu A rho lam x = 1

theorem SymmetricSpace.sphericalFunction_eq_one.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B]
  (nu : MeasureTheory.Measure B)
  [MeasureTheory.IsProbabilityMeasure nu]
  (A : X → B → E) (rho lam : E) {x : X}
  (hx : ∀ (b : B), A x b = 0) :
  SymmetricSpace.sphericalFunction nu A
      rho lam x =
    1

At a point whose composite distance to every boundary normal vanishes — the origin of the
symmetric space — the spherical function is `1`, the boundary measure being a probability
measure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Defs.lean

complete

theorem SymmetricSpace.integral_helgasonFourier_eq.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {X : Type u_2} {B : Type u_3} [MeasurableSpace X] [MeasurableSpace B]
  (μ : MeasureTheory.Measure X) (nu : MeasureTheory.Measure B)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite nu] (A : X → B → E)
  (rho : E) (f : X → ℂ) (lam : E)
  (hint :
    MeasureTheory.Integrable
      (fun p ↦
        f p.1 *
          SymmetricSpace.horosphericalCharacter rho (-lam) (A p.1 p.2))
      (μ.prod nu)) :
  ∫ (b : B), SymmetricSpace.helgasonFourier μ A rho f lam b ∂nu =
    ∫ (x : X),
      f x * SymmetricSpace.sphericalFunction nu A rho (-lam) x ∂μ

theorem SymmetricSpace.integral_helgasonFourier_eq.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  [MeasurableSpace B]
  (μ : MeasureTheory.Measure X)
  (nu : MeasureTheory.Measure B)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite nu]
  (A : X → B → E) (rho : E) (f : X → ℂ)
  (lam : E)
  (hint :
    MeasureTheory.Integrable
      (fun p ↦
        f p.1 *
          SymmetricSpace.horosphericalCharacter
            rho (-lam) (A p.1 p.2))
      (μ.prod nu)) :
  ∫ (b : B),
      SymmetricSpace.helgasonFourier μ A
        rho f lam b ∂nu =
    ∫ (x : X),
      f x *
        SymmetricSpace.sphericalFunction
          nu A rho (-lam) x ∂μ

Averaging the Helgason--Fourier transform over the boundary pairs the function against the
spherical function at the reflected frequency:
`∫_B f̂(λ,b) db = ∫_X f(x) φ_{-λ}(x) dμ(x)`.

This is the measure-theoretic content of Helgason's remark that the Helgason--Fourier transform
extends the spherical transform: when `f` is `K`-invariant its transform does not depend on `b`, so
the left-hand side is `f̂(λ,b)` itself and the right-hand side is the spherical transform of `f`
(*Geometric Analysis on Symmetric Spaces*, Ch. III §1). The proof is Fubini, so the joint
integrability hypothesis is the whole of it.

Everything is built from one function, the character v\mapsto e^{(i\lambda+\varrho)(v)} of \mathfrak a. It is the exponential of a linear functional, hence multiplicative in v; that single fact is what turns the cocycle relation for A into a product formula for the kernels, and it is why \varrho=0 returns the Euclidean plane wave while \lambda=0 returns the weight e^{\varrho(v)} that a layer of a network on G/K carries. Its modulus is e^{\varrho(v)}, so the growth of the kernel is governed by \varrho alone, uniformly in the frequency.

The one theorem here is the measure-theoretic core of Helgason's remark that the transform extends the spherical transform: averaging \hat f(\lambda,b) over the boundary pairs f against the spherical function \varphi_{-\lambda}. When f is K-invariant its transform does not depend on b, so the left side is the transform itself and the right side is the spherical transform. The proof is Fubini, so the joint integrability hypothesis is the whole of it.

Theorem5.8.2

uses 1used by 0✓L∃∀N

The transformation law of the composite distance, and what it does to the transform. A(g\cdot x,g\cdot b)=A(x,b)+A(g\cdot o,g\cdot b): moving both arguments by the same element of G shifts the composite distance by a quantity depending on the boundary point alone. Abstractly this is the predicate IsCompositeCocycle T S A shift; under it, and with T preserving the measure of X, the Helgason--Fourier transform at the moved boundary point is the transform of the moved function times the character at the shift.

Lean code for Theorem5.8.2●7 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Cocycle.lean

complete

def SymmetricSpace.IsCompositeCocycle.{u_1, u_2, u_3} {E : Type u_1}
  [AddMonoid E] {X : Type u_2} {B : Type u_3} (T : X → X) (S : B → B)
  (A : X → B → E) (shift : B → E) : Prop

def SymmetricSpace.IsCompositeCocycle.{u_1,
    u_2, u_3}
  {E : Type u_1} [AddMonoid E]
  {X : Type u_2} {B : Type u_3}
  (T : X → X) (S : B → B) (A : X → B → E)
  (shift : B → E) : Prop

Implementation after :=

:=
  ∀ x b, A (T x) (S b) = A x b + shift b

The transformation law of the composite distance under a pair of maps: `T` moves the points of
`X`, `S` moves the boundary normals of `B`, and `A` is displaced by a vector `shift b` of `𝔞` that
does not depend on the point.

On `X = G/K` this is the identity `⟨g·x, g·b⟩ = ⟨x,b⟩ + ⟨g·o, g·b⟩` for the composite distance,
with `T = (g · ·)` on `X`, `S = (g · ·)` on `B`, and `shift b = ⟨g·o, g·b⟩` the value at the base
point `o = eK` (Helgason, *Groups and Geometric Analysis*, Ch. II §1 No. 3). The displacement is
therefore not extra data in a concrete model: it is the composite distance of the moved base
point.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Cocycle.lean

complete

theorem SymmetricSpace.isCompositeCocycle_id.{u_1, u_2, u_3} {E : Type u_1}
  [AddMonoid E] {X : Type u_2} {B : Type u_3} (A : X → B → E) :
  SymmetricSpace.IsCompositeCocycle id id A 0

theorem SymmetricSpace.isCompositeCocycle_id.{u_1,
    u_2, u_3}
  {E : Type u_1} [AddMonoid E]
  {X : Type u_2} {B : Type u_3}
  (A : X → B → E) :
  SymmetricSpace.IsCompositeCocycle id id
    A 0

The identity pair of maps displaces the composite distance by nothing: the case `g = e`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Cocycle.lean

complete

theorem SymmetricSpace.IsCompositeCocycle.comp.{u_1, u_2, u_3} {E : Type u_1}
  [AddMonoid E] {X : Type u_2} {B : Type u_3} {T₁ T₂ : X → X}
  {S₁ S₂ : B → B} {A : X → B → E} {shift₁ shift₂ : B → E}
  (hc₁ : SymmetricSpace.IsCompositeCocycle T₁ S₁ A shift₁)
  (hc₂ : SymmetricSpace.IsCompositeCocycle T₂ S₂ A shift₂) :
  SymmetricSpace.IsCompositeCocycle (T₂ ∘ T₁) (S₂ ∘ S₁) A fun b ↦
    shift₁ b + shift₂ (S₁ b)

theorem SymmetricSpace.IsCompositeCocycle.comp.{u_1,
    u_2, u_3}
  {E : Type u_1} [AddMonoid E]
  {X : Type u_2} {B : Type u_3}
  {T₁ T₂ : X → X} {S₁ S₂ : B → B}
  {A : X → B → E} {shift₁ shift₂ : B → E}
  (hc₁ :
    SymmetricSpace.IsCompositeCocycle T₁
      S₁ A shift₁)
  (hc₂ :
    SymmetricSpace.IsCompositeCocycle T₂
      S₂ A shift₂) :
  SymmetricSpace.IsCompositeCocycle
    (T₂ ∘ T₁) (S₂ ∘ S₁) A fun b ↦
    shift₁ b + shift₂ (S₁ b)

**The cocycle identity.** Composing two pairs of maps composes the cocycles: the displacement
of `(T₂ ∘ T₁, S₂ ∘ S₁)` is the displacement of the first pair plus the displacement of the second
pair *read at the boundary point already moved by the first*.

On `X = G/K` with `T_i = (g_i · ·)` this is the familiar
`⟨(g₂g₁)·o, (g₂g₁)·b⟩ = ⟨g₁·o, g₁·b⟩ + ⟨g₂·o, g₂·(g₁·b)⟩`, that is, the Iwasawa `A`-component is a
cocycle on `G × B` rather than a homomorphism. The transport by `S₁` is the whole content: without
it the displacement would be additive in the group element, which it is not.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Cocycle.lean

complete

theorem SymmetricSpace.IsCompositeCocycle.helgasonFourier_apply.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {X : Type u_2} {B : Type u_3} [MeasurableSpace X] {T : X → X}
  {S : B → B} {A : X → B → E} {shift : B → E}
  (hc : SymmetricSpace.IsCompositeCocycle T S A shift)
  {μ : MeasureTheory.Measure X}
  (hT : MeasureTheory.MeasurePreserving T μ μ)
  (hTm : MeasurableEmbedding T) (rho : E) (f : X → ℂ) (lam : E)
  (b : B) :
  SymmetricSpace.helgasonFourier μ A rho f lam (S b) =
    SymmetricSpace.horosphericalCharacter rho (-lam) (shift b) *
      SymmetricSpace.helgasonFourier μ A rho (f ∘ T) lam b

theorem SymmetricSpace.IsCompositeCocycle.helgasonFourier_apply.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  {T : X → X} {S : B → B} {A : X → B → E}
  {shift : B → E}
  (hc :
    SymmetricSpace.IsCompositeCocycle T S
      A shift)
  {μ : MeasureTheory.Measure X}
  (hT :
    MeasureTheory.MeasurePreserving T μ μ)
  (hTm : MeasurableEmbedding T) (rho : E)
  (f : X → ℂ) (lam : E) (b : B) :
  SymmetricSpace.helgasonFourier μ A rho f
      lam (S b) =
    SymmetricSpace.horosphericalCharacter
        rho (-lam) (shift b) *
      SymmetricSpace.helgasonFourier μ A
        rho (f ∘ T) lam b

**The transformation law of the Helgason--Fourier transform.** If `(T, S)` displaces the
composite distance by `shift` and `T` preserves the invariant measure, then

`f̂(λ, S b) = e^{(-iλ+ϱ)(shift b)} \cdot \widehat{f ∘ T}(λ, b)`.

This is the symmetric-space form of the elementary identity `\widehat{f(· - a)}(λ) = e^{-iλa}
f̂(λ)` of Euclidean Fourier analysis (Helgason, *Groups and Geometric Analysis*, Ch. III §1). Two
facts and nothing else go into it: the character is multiplicative, so the additive displacement of
`A` factors out of the kernel, and `T` preserves `μ`, so the change of variables is free.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Cocycle.lean

complete

theorem SymmetricSpace.IsCompositeCocycle.norm_helgasonFourier_apply.{u_1, u_2,
    u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {X : Type u_2} {B : Type u_3} [MeasurableSpace X] {T : X → X}
  {S : B → B} {A : X → B → E} {shift : B → E}
  (hc : SymmetricSpace.IsCompositeCocycle T S A shift)
  {μ : MeasureTheory.Measure X}
  (hT : MeasureTheory.MeasurePreserving T μ μ)
  (hTm : MeasurableEmbedding T) (rho : E) (f : X → ℂ) (lam : E)
  (b : B) :
  ‖SymmetricSpace.helgasonFourier μ A rho f lam (S b)‖ =
    Real.exp (inner ℝ rho (shift b)) *
      ‖SymmetricSpace.helgasonFourier μ A rho (f ∘ T) lam b‖

theorem SymmetricSpace.IsCompositeCocycle.norm_helgasonFourier_apply.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  {T : X → X} {S : B → B} {A : X → B → E}
  {shift : B → E}
  (hc :
    SymmetricSpace.IsCompositeCocycle T S
      A shift)
  {μ : MeasureTheory.Measure X}
  (hT :
    MeasureTheory.MeasurePreserving T μ μ)
  (hTm : MeasurableEmbedding T) (rho : E)
  (f : X → ℂ) (lam : E) (b : B) :
  ‖SymmetricSpace.helgasonFourier μ A rho
        f lam (S b)‖ =
    Real.exp (inner ℝ rho (shift b)) *
      ‖SymmetricSpace.helgasonFourier μ A
          rho (f ∘ T) lam b‖

The modulus of the transformation law: the factor is the real weight `e^{ϱ(shift b)}`, the
frequency contributing nothing. In particular the multiplier is bounded uniformly in `λ`, which is
what lets the transform be estimated on a whole `λ`-family at once.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Cocycle.lean

complete

theorem SymmetricSpace.IsCompositeCocycle.sphericalFunction_apply.{u_1, u_2,
    u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {X : Type u_2} {B : Type u_3} [MeasurableSpace B] {T : X → X}
  {S : B → B} {A : X → B → E} {shift : B → E}
  (hc : SymmetricSpace.IsCompositeCocycle T S A shift)
  {nu : MeasureTheory.Measure B}
  (hS : MeasureTheory.MeasurePreserving S nu nu)
  (hSm : MeasurableEmbedding S) (rho lam : E) (x : X) :
  SymmetricSpace.sphericalFunction nu A rho lam (T x) =
    ∫ (b : B),
      SymmetricSpace.horosphericalCharacter rho lam (A x b) *
        SymmetricSpace.horosphericalCharacter rho lam (shift b) ∂nu

theorem SymmetricSpace.IsCompositeCocycle.sphericalFunction_apply.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B]
  {T : X → X} {S : B → B} {A : X → B → E}
  {shift : B → E}
  (hc :
    SymmetricSpace.IsCompositeCocycle T S
      A shift)
  {nu : MeasureTheory.Measure B}
  (hS :
    MeasureTheory.MeasurePreserving S nu
      nu)
  (hSm : MeasurableEmbedding S)
  (rho lam : E) (x : X) :
  SymmetricSpace.sphericalFunction nu A
      rho lam (T x) =
    ∫ (b : B),
      SymmetricSpace.horosphericalCharacter
          rho lam (A x b) *
        SymmetricSpace.horosphericalCharacter
          rho lam (shift b) ∂nu

The spherical function at a moved point. If `(T, S)` displaces the composite distance by
`shift` and `S` preserves the boundary measure, then `φ_λ(T x)` is the boundary integral of the
character at `x` weighted by `e^{(iλ+ϱ)(shift b)}`.

Only the weighted form is true in this generality: the displacement depends on `b`, so it does not
come out of the boundary integral, and `φ_λ(T x)` is genuinely a different integral from `φ_λ(x)`.
The invariance statement is
`SymmetricSpace.IsCompositeCocycle.sphericalFunction_apply_of_shift_eq_zero` below, under the
hypothesis that the displacement vanishes.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Cocycle.lean

complete

theorem SymmetricSpace.IsCompositeCocycle.sphericalFunction_apply_of_shift_eq_zero.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {X : Type u_2} {B : Type u_3} [MeasurableSpace B] {T : X → X}
  {S : B → B} {A : X → B → E} {shift : B → E}
  (hc : SymmetricSpace.IsCompositeCocycle T S A shift)
  {nu : MeasureTheory.Measure B}
  (hS : MeasureTheory.MeasurePreserving S nu nu)
  (hSm : MeasurableEmbedding S) (hshift : shift = 0) (rho lam : E)
  (x : X) :
  SymmetricSpace.sphericalFunction nu A rho lam (T x) =
    SymmetricSpace.sphericalFunction nu A rho lam x

theorem SymmetricSpace.IsCompositeCocycle.sphericalFunction_apply_of_shift_eq_zero.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B]
  {T : X → X} {S : B → B} {A : X → B → E}
  {shift : B → E}
  (hc :
    SymmetricSpace.IsCompositeCocycle T S
      A shift)
  {nu : MeasureTheory.Measure B}
  (hS :
    MeasureTheory.MeasurePreserving S nu
      nu)
  (hSm : MeasurableEmbedding S)
  (hshift : shift = 0) (rho lam : E)
  (x : X) :
  SymmetricSpace.sphericalFunction nu A
      rho lam (T x) =
    SymmetricSpace.sphericalFunction nu A
      rho lam x

The spherical function is invariant under a pair of maps with vanishing displacement.

The hypothesis `shift = 0` is what singles out an isometry fixing the base point, `g ∈ K`, since
the displacement is the composite distance of the moved base point; for a general `g` the spherical
function is *not* invariant and only the weighted formula
`SymmetricSpace.IsCompositeCocycle.sphericalFunction_apply` holds. Under that hypothesis this is
the `K`-invariance of `φ_λ`, the reason it descends to a function of the geodesic distance
(Helgason, *Groups and Geometric Analysis*, Ch. IV §2).

The displacement is read at S_1b and not at b when two motions are composed, which is what makes this a cocycle rather than a homomorphism, and it is the whole of the bookkeeping. Everything else follows from the multiplicativity of the character: the shift leaves the integral over X as a constant factor, so the modulus of the transform picks up exactly e^{\varrho(\text{shift})} and nothing depending on the frequency.

The spherical function does not simplify as cleanly, and the statement here says so rather than pretending otherwise. Its boundary integral acquires a factor e^{(i\lambda+\varrho)(\text{shift}(b))} that depends on b, so it cannot be pulled out; what does come out is the genuine invariance \varphi_\lambda(T x)=\varphi_\lambda(x), and only when the shift vanishes — the case of a motion fixing the base point, that is of an element of K, which is the classical statement that spherical functions are K-invariant.

Theorem5.8.3

uses 1used by 1✓L∃∀N

The Fourier slice theorem on a symmetric space. On \mathbb R^m the Fourier transform is the one-dimensional Fourier transform of the Radon transform. Helgason opens Ch. III of Geometric Analysis on Symmetric Spaces by observing that the same holds on X=G/K with horospheres in place of hyperplanes, and that is proved here: \hat f(\lambda,b)=\int_{\mathfrak a}e^{(-i\lambda+\varrho)(t)}Rf(b,t)\,\mathrm dt, where Rf(b,t) is the integral of f over the horosphere at composite distance t with normal b.

Lean code for Theorem5.8.3●6 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/HorocycleRadon.lean

complete

def SymmetricSpace.horocycleRadon.{u_1, u_2, u_3} {E : Type u_1}
  {X : Type u_2} {B : Type u_3} [MeasurableSpace X]
  (kap : B → E → MeasureTheory.Measure X) (f : X → ℂ) (b : B) (t : E) :
  ℂ

def SymmetricSpace.horocycleRadon.{u_1, u_2,
    u_3}
  {E : Type u_1} {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  (kap : B → E → MeasureTheory.Measure X)
  (f : X → ℂ) (b : B) (t : E) : ℂ

Implementation after :=

:=
  ∫ x : X, f x ∂(kap b t)

The horocycle Radon transform `Rf(b,t) = ∫_{ξ(t,b)} f`, the integral of `f` over the horosphere
at composite distance `t` from the origin with normal `b`.

The horosphere is presented by a measure `κ b t` concentrated on it. Mathlib has no Riemannian
measure, so this family is data; the hypotheses that tie it to the composite distance and to the
invariant measure appear in the theorems below.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/HorocycleRadon.lean

complete

def SymmetricSpace.dualHorocycle.{u_1, u_2, u_3} {E : Type u_1}
  {X : Type u_2} {B : Type u_3} [MeasurableSpace B]
  (nu : MeasureTheory.Measure B) (A : X → B → E) (phi : E → B → ℂ)
  (x : X) : ℂ

def SymmetricSpace.dualHorocycle.{u_1, u_2,
    u_3}
  {E : Type u_1} {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B]
  (nu : MeasureTheory.Measure B)
  (A : X → B → E) (phi : E → B → ℂ)
  (x : X) : ℂ

Implementation after :=

:=
  ∫ b : B, phi (A x b) b ∂nu

The dual horocycle transform `φ^∨(x) = ∫_B φ(A(x,b), b) db`: the average of a function on the
space of horospheres over the horospheres passing through `x`. Together with `horocycleRadon` it is
the dual pair `(X, Ξ) = (G/K, G/MN)` of Helgason's duality.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/HorocycleRadon.lean

complete

theorem SymmetricSpace.sphericalFunction_eq_dualHorocycle.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {X : Type u_2} {B : Type u_3} [MeasurableSpace B]
  (nu : MeasureTheory.Measure B) (A : X → B → E) (rho lam : E) :
  SymmetricSpace.sphericalFunction nu A rho lam =
    SymmetricSpace.dualHorocycle nu A fun t x ↦
      SymmetricSpace.horosphericalCharacter rho lam t

theorem SymmetricSpace.sphericalFunction_eq_dualHorocycle.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B]
  (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho lam : E) :
  SymmetricSpace.sphericalFunction nu A
      rho lam =
    SymmetricSpace.dualHorocycle nu A
      fun t x ↦
      SymmetricSpace.horosphericalCharacter
        rho lam t

The spherical function is the dual transform of the character: `φ_λ = (e^{(iλ+ϱ)})^∨`. Since
the character depends only on the `𝔞`-variable, the spherical function is the dual transform of a
function that is constant along the boundary.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/HorocycleRadon.lean

complete

theorem SymmetricSpace.helgasonFourier_eq_integral_horocycleRadon.{u_1, u_2,
    u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2} {B : Type u_3} [MeasurableSpace X]
  (μ : MeasureTheory.Measure X) (mua : MeasureTheory.Measure E)
  (A : X → B → E) (rho : E) (f : X → ℂ) (lam : E) (b : B)
  (kap : B → E → MeasureTheory.Measure X)
  (hsupp : ∀ (t : E), ∀ᵐ (x : X) ∂kap b t, A x b = t)
  (hdis :
    ∫ (x : X),
        f x *
          SymmetricSpace.horosphericalCharacter rho (-lam) (A x b) ∂μ =
      ∫ (t : E),
        ∫ (x : X),
          f x *
            SymmetricSpace.horosphericalCharacter rho (-lam)
              (A x b) ∂kap b t ∂mua) :
  SymmetricSpace.helgasonFourier μ A rho f lam b =
    ∫ (t : E),
      SymmetricSpace.horosphericalCharacter rho (-lam) t *
        SymmetricSpace.horocycleRadon kap f b t ∂mua

theorem SymmetricSpace.helgasonFourier_eq_integral_horocycleRadon.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  (μ : MeasureTheory.Measure X)
  (mua : MeasureTheory.Measure E)
  (A : X → B → E) (rho : E) (f : X → ℂ)
  (lam : E) (b : B)
  (kap : B → E → MeasureTheory.Measure X)
  (hsupp :
    ∀ (t : E),
      ∀ᵐ (x : X) ∂kap b t, A x b = t)
  (hdis :
    ∫ (x : X),
        f x *
          SymmetricSpace.horosphericalCharacter
            rho (-lam) (A x b) ∂μ =
      ∫ (t : E),
        ∫ (x : X),
          f x *
            SymmetricSpace.horosphericalCharacter
              rho (-lam)
              (A x b) ∂kap b t ∂mua) :
  SymmetricSpace.helgasonFourier μ A rho f
      lam b =
    ∫ (t : E),
      SymmetricSpace.horosphericalCharacter
          rho (-lam) t *
        SymmetricSpace.horocycleRadon kap
          f b t ∂mua

**The Fourier slice theorem on a noncompact symmetric space.** The Helgason--Fourier transform
at a boundary normal `b` is the integral over `𝔞` of the horocycle Radon transform against the
character:
`f̂(λ,b) = ∫_𝔞 e^{(-iλ+ϱ)(t)} Rf(b,t) dt`.

This is the symmetric-space form of "the Fourier transform is the one-dimensional Fourier transform
of the Radon transform" (Helgason, *Geometric Analysis on Symmetric Spaces*, Ch. III, opening
remark (ii) and §5 No. 3).

The two hypotheses are exactly the two things a concrete model has to supply. `hsupp` says the
kernel really is carried by the horosphere — on the fibre the composite distance is the constant
`t` — and `hdis` is the horospherical change of variables for the integrand at hand, which is
where the normalization of `dt` on `𝔞` is fixed. Given them the proof is one rewriting: a constant
comes out of the fibre integral.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/HorocycleRadon.lean

complete

theorem SymmetricSpace.helgasonFourier_eq_fourier_weightedHorocycleRadon.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2} {B : Type u_3} [MeasurableSpace X]
  (μ : MeasureTheory.Measure X) (mua : MeasureTheory.Measure E)
  (A : X → B → E) (rho : E) (f : X → ℂ) (lam : E) (b : B)
  (kap : B → E → MeasureTheory.Measure X)
  (hsupp : ∀ (t : E), ∀ᵐ (x : X) ∂kap b t, A x b = t)
  (hdis :
    ∫ (x : X),
        f x *
          SymmetricSpace.horosphericalCharacter rho (-lam) (A x b) ∂μ =
      ∫ (t : E),
        ∫ (x : X),
          f x *
            SymmetricSpace.horosphericalCharacter rho (-lam)
              (A x b) ∂kap b t ∂mua) :
  SymmetricSpace.helgasonFourier μ A rho f lam b =
    ∫ (t : E),
      Complex.exp (-(Complex.I * ↑(inner ℝ lam t))) *
        (↑(Real.exp (inner ℝ rho t)) *
          SymmetricSpace.horocycleRadon kap f b t) ∂mua

theorem SymmetricSpace.helgasonFourier_eq_fourier_weightedHorocycleRadon.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  (μ : MeasureTheory.Measure X)
  (mua : MeasureTheory.Measure E)
  (A : X → B → E) (rho : E) (f : X → ℂ)
  (lam : E) (b : B)
  (kap : B → E → MeasureTheory.Measure X)
  (hsupp :
    ∀ (t : E),
      ∀ᵐ (x : X) ∂kap b t, A x b = t)
  (hdis :
    ∫ (x : X),
        f x *
          SymmetricSpace.horosphericalCharacter
            rho (-lam) (A x b) ∂μ =
      ∫ (t : E),
        ∫ (x : X),
          f x *
            SymmetricSpace.horosphericalCharacter
              rho (-lam)
              (A x b) ∂kap b t ∂mua) :
  SymmetricSpace.helgasonFourier μ A rho f
      lam b =
    ∫ (t : E),
      Complex.exp
          (-(Complex.I *
              ↑(inner ℝ lam t))) *
        (↑(Real.exp (inner ℝ rho t)) *
          SymmetricSpace.horocycleRadon
            kap f b t) ∂mua

The Fourier slice theorem with the character split into its phase and its weight, so that the
right-hand side is visibly the Euclidean Fourier transform on `𝔞` of the *weighted* horocycle Radon
transform `t ↦ e^{ϱ(t)} Rf(b,t)`.

Read this way, the Helgason--Fourier transform of `X` is nothing but the Fourier transform of
`\mathbb R^r`, applied to a function on `𝔞` obtained from `f` by integrating over horospheres. It
is why the inversion formula on `X` reduces to a Euclidean Fourier inversion together with an
inversion of the Radon transform, and why the density `|c(λ)|^{-2}` appears as a Fourier multiplier
rather than as a geometric factor.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/HorocycleRadon.lean

complete

theorem SymmetricSpace.helgasonInversionIntegral_eq_integral_dualHorocycle.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2} {B : Type u_3} [MeasurableSpace B]
  (mua : MeasureTheory.Measure E) (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho : E) (F : E → B → ℂ) (kappa : E → ℝ) (x : X) :
  SymmetricSpace.helgasonInversionIntegral mua nu A rho F kappa x =
    ∫ (lam : E),
      SymmetricSpace.dualHorocycle nu A
        (fun t b ↦
          F lam b * ↑(kappa lam) *
            SymmetricSpace.horosphericalCharacter rho lam t)
        x ∂mua

theorem SymmetricSpace.helgasonInversionIntegral_eq_integral_dualHorocycle.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace B]
  (mua : MeasureTheory.Measure E)
  (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho : E)
  (F : E → B → ℂ) (kappa : E → ℝ)
  (x : X) :
  SymmetricSpace.helgasonInversionIntegral
      mua nu A rho F kappa x =
    ∫ (lam : E),
      SymmetricSpace.dualHorocycle nu A
        (fun t b ↦
          F lam b * ↑(kappa lam) *
            SymmetricSpace.horosphericalCharacter
              rho lam t)
        x ∂mua

The inversion integral is the `𝔞`-integral of dual horocycle transforms. Helgason's inversion
of the Radon transform has the shape `f = w^{-1}(\Lambda\Lambda f^\wedge)^\vee` (*Geometric
Analysis on Symmetric Spaces*, Ch. II, Thm 3.13), a Fourier multiplier applied to the Radon
transform and then averaged back by the dual transform; this records that the right-hand side of
the Helgason--Fourier inversion formula has that shape, the multiplier being the Plancherel density
`κ` together with the character.

The horospheres with a fixed normal are the level sets of the composite distance, so a horosphere integral is a fibre integral. Mathlib has no Riemannian measure to build one from, and on a general X there is no reason for one to exist, so the family of fibre measures is data: a kernel carried by the horosphere, plus the hypothesis that integrating against the invariant measure is integrating over a fibre and then over \mathfrak a. In a concrete model that hypothesis is the horospherical change of variables, and it is where the normalization of \mathrm dt is fixed — which is where the constant of the inversion formula comes from, so it is better in the open than buried in a definition. Given the kernel the proof is one rewriting: on a fibre the kernel e^{(-i\lambda+\varrho)(A(x,b))} is the constant e^{(-i\lambda+\varrho)(t)}, so it leaves the fibre integral.

Splitting the character into its phase and its weight puts the right-hand side in the form of a genuine Euclidean Fourier transform, of t\mapsto e^{\varrho(t)}Rf(b,t). That is the reason the inversion formula on X decomposes into a Euclidean Fourier inversion and an inversion of the Radon transform, and the reason the density |c(\lambda)|^{-2} appears as a Fourier multiplier rather than as a geometric factor. The dual transform is recorded alongside, together with two identifications it makes: the spherical function is the dual transform of the character, and the inversion integral is an \mathfrak a-integral of dual transforms — the shape f=w^{-1}(\Lambda\Lambda f^\wedge)^\vee of Helgason's inversion of the Radon transform.

Theorem5.8.4

Statement uses 2

Statement dependency previews

Preview

Theorem 5.8.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 5

Reverse dependency previews

Preview

Theorem 3.1.12

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The c-function, the Plancherel density, and the inversion formula as a proposition. The inversion formula f=|W|^{-1}\int_{\mathfrak a^*\times B}\hat f(\lambda,b)e^{(i\lambda+\varrho)(A(x,b))}|c(\lambda)|^{-2} is stated here as a predicate on the data — never an axiom, a structure field or a sorry — so that a concrete model has a definite statement to prove. With the geometry left free it is not even a well-posed claim.

Lean code for Theorem5.8.4●9 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/CFunction.lean

complete

def SymmetricSpace.plancherelDensity.{u_1} {E : Type u_1} (W : ℝ)
  (c : E → ℂ) (lam : E) : ℝ

def SymmetricSpace.plancherelDensity.{u_1}
  {E : Type u_1} (W : ℝ) (c : E → ℂ)
  (lam : E) : ℝ

Implementation after :=

:= (W * ‖c lam‖ ^ 2)⁻¹

The density `κ(λ) = (|W| ‖c(λ)‖²)^{-1}` of the Helgason--Fourier inversion formula
(Helgason, *Geometric Analysis on Symmetric Spaces*, Ch. III, Thm 1.3), built from the order `W` of
the Weyl group and the `c`-function.

The two ingredients are kept as separate arguments because the split between them is a convention:
`|W|` can be absorbed into `c`, and different sources do. What is invariant is the product.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/CFunction.lean

complete

theorem SymmetricSpace.plancherelDensity_eq.{u_1} {E : Type u_1} (W : ℝ)
  (c : E → ℂ) (lam : E) :
  SymmetricSpace.plancherelDensity W c lam = (W * ‖c lam‖ ^ 2)⁻¹

theorem SymmetricSpace.plancherelDensity_eq.{u_1}
  {E : Type u_1} (W : ℝ) (c : E → ℂ)
  (lam : E) :
  SymmetricSpace.plancherelDensity W c
      lam =
    (W * ‖c lam‖ ^ 2)⁻¹

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/CFunction.lean

complete

theorem SymmetricSpace.plancherelDensity_pos.{u_1} {E : Type u_1} {W : ℝ}
  (hW : 0 < W) (c : E → ℂ) {lam : E} (hc : c lam ≠ 0) :
  0 < SymmetricSpace.plancherelDensity W c lam

theorem SymmetricSpace.plancherelDensity_pos.{u_1}
  {E : Type u_1} {W : ℝ} (hW : 0 < W)
  (c : E → ℂ) {lam : E} (hc : c lam ≠ 0) :
  0 <
    SymmetricSpace.plancherelDensity W c
      lam

The density is positive wherever the `c`-function does not vanish. Its zeros and poles are what
the Paley--Wiener theory of the transform is about; positivity away from them is all the inversion
formula needs in order to be read as a measure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/CFunction.lean

complete

theorem SymmetricSpace.plancherelDensity_congr.{u_1} {E : Type u_1} (W : ℝ)
  (c c' : E → ℂ) (lam : E) (h : ‖c' lam‖ = ‖c lam‖) :
  SymmetricSpace.plancherelDensity W c' lam =
    SymmetricSpace.plancherelDensity W c lam

theorem SymmetricSpace.plancherelDensity_congr.{u_1}
  {E : Type u_1} (W : ℝ) (c c' : E → ℂ)
  (lam : E) (h : ‖c' lam‖ = ‖c lam‖) :
  SymmetricSpace.plancherelDensity W c'
      lam =
    SymmetricSpace.plancherelDensity W c
      lam

Changing the `c`-function without changing its modulus does not change the density. This is the
precise sense in which the phase convention for `c` is free — and, read the other way, the reason a
discrepancy in a power of `π` between two sources cannot be a phase convention but must be a
normalization of the measures.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/CFunction.lean

complete

def SymmetricSpace.cFunctionIntegral.{u_1, u_2} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Y : Type u_2}
  [MeasurableSpace Y] (nbar : MeasureTheory.Measure Y) (H : Y → E)
  (rho lam : E) : ℂ

def SymmetricSpace.cFunctionIntegral.{u_1,
    u_2}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {Y : Type u_2}
  [MeasurableSpace Y]
  (nbar : MeasureTheory.Measure Y)
  (H : Y → E) (rho lam : E) : ℂ

Implementation after :=

:=
  ∫ n : Y, horosphericalCharacter (-rho) (-lam) (H n) ∂nbar

**Harish-Chandra's `c`-function**, `c(λ) = ∫_{N̄} e^{-(iλ+ϱ)(H(n̄))} dn̄`, where `H` is the
`𝔞`-component of the Iwasawa decomposition on the opposite nilpotent group `N̄`.

The integrand is `horosphericalCharacter (-ϱ) (-λ)`, the character of the exponent `-(iλ+ϱ)`. Both
`H` and the measure `dn̄` are data; fixing them is what fixes the normalization of the whole
inversion formula, so they are arguments rather than a global convention.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/CFunction.lean

complete

theorem SymmetricSpace.mul_neg_eq_normSq_of_conj.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] (c : E → ℂ) (lam : E)
  (h : c (-lam) = (starRingEnd ℂ) (c lam)) :
  c lam * c (-lam) = ↑(‖c lam‖ ^ 2)

theorem SymmetricSpace.mul_neg_eq_normSq_of_conj.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (c : E → ℂ) (lam : E)
  (h :
    c (-lam) = (starRingEnd ℂ) (c lam)) :
  c lam * c (-lam) = ↑(‖c lam‖ ^ 2)

On the real form `𝔞*` the `c`-function satisfies `c(-λ) = conj(c(λ))`, and then its squared
modulus is the product `c(λ)c(-λ)`. The reflection is a property of the defining integral in each
model, so it enters as a hypothesis.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Inversion.lean

complete

def SymmetricSpace.HasHelgasonInversion.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E]
  {X : Type u_2} {B : Type u_3} [MeasurableSpace X] [MeasurableSpace B]
  (μ : MeasureTheory.Measure X) (mua : MeasureTheory.Measure E)
  (nu : MeasureTheory.Measure B) (A : X → B → E) (rho : E) (W : ℝ)
  (c : E → ℂ) (f : X → ℂ) : Prop

def SymmetricSpace.HasHelgasonInversion.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  [MeasurableSpace B]
  (μ : MeasureTheory.Measure X)
  (mua : MeasureTheory.Measure E)
  (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho : E) (W : ℝ)
  (c : E → ℂ) (f : X → ℂ) : Prop

Implementation after :=

:=
  ∀ x : X, helgasonInversionIntegral mua nu A rho (helgasonFourier μ A rho f)
    (plancherelDensity W c) x = f x

**The Helgason--Fourier inversion formula** for `f`, as a proposition about the geometry:
the inversion integral of the Helgason--Fourier transform of `f`, against the density
`(|W| ‖c(λ)‖²)^{-1}`, returns `f`.

This is a `Prop` on data rather than an assumption object: a concrete model instantiates the data
and then has a definite statement to prove. With the geometry left free it is not even a
well-posed claim, which is why the constructions of a model have to come first.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Inversion.lean

complete

theorem SymmetricSpace.hasHelgasonInversion_iff.{u_1, u_2, u_3} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E]
  {X : Type u_2} {B : Type u_3} [MeasurableSpace X] [MeasurableSpace B]
  (μ : MeasureTheory.Measure X) (mua : MeasureTheory.Measure E)
  (nu : MeasureTheory.Measure B) (A : X → B → E) (rho : E) (W : ℝ)
  (c : E → ℂ) (f : X → ℂ) :
  SymmetricSpace.HasHelgasonInversion μ mua nu A rho W c f ↔
    ∀ (x : X),
      ∫ (lam : E),
          ∫ (b : B),
            SymmetricSpace.helgasonFourier μ A rho f lam b *
                ↑(SymmetricSpace.plancherelDensity W c lam) *
              SymmetricSpace.horosphericalCharacter rho lam
                (A x b) ∂nu ∂mua =
        f x

theorem SymmetricSpace.hasHelgasonInversion_iff.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  [MeasurableSpace B]
  (μ : MeasureTheory.Measure X)
  (mua : MeasureTheory.Measure E)
  (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho : E) (W : ℝ)
  (c : E → ℂ) (f : X → ℂ) :
  SymmetricSpace.HasHelgasonInversion μ
      mua nu A rho W c f ↔
    ∀ (x : X),
      ∫ (lam : E),
          ∫ (b : B),
            SymmetricSpace.helgasonFourier
                  μ A rho f lam b *
                ↑(SymmetricSpace.plancherelDensity
                    W c lam) *
              SymmetricSpace.horosphericalCharacter
                rho lam (A x b) ∂nu ∂mua =
        f x

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Symmetric/Inversion.lean

complete

theorem SymmetricSpace.hasHelgasonInversion_of_spherical.{u_1, u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2} {B : Type u_3} [MeasurableSpace X]
  [MeasurableSpace B] (μ : MeasureTheory.Measure X)
  (mua : MeasureTheory.Measure E) (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho : E) (W : ℝ) (c : E → ℂ) (f : X → ℂ)
  (conv : E → X → ℂ)
  (hconv :
    ∀ (lam : E) (x : X),
      ∫ (b : B),
          SymmetricSpace.helgasonFourier μ A rho f lam b *
            SymmetricSpace.horosphericalCharacter rho lam (A x b) ∂nu =
        conv lam x)
  (hsph :
    ∀ (x : X),
      ∫ (lam : E),
          ↑(SymmetricSpace.plancherelDensity W c lam) *
            conv lam x ∂mua =
        f x) :
  SymmetricSpace.HasHelgasonInversion μ mua nu A rho W c f

theorem SymmetricSpace.hasHelgasonInversion_of_spherical.{u_1,
    u_2, u_3}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] {X : Type u_2}
  {B : Type u_3} [MeasurableSpace X]
  [MeasurableSpace B]
  (μ : MeasureTheory.Measure X)
  (mua : MeasureTheory.Measure E)
  (nu : MeasureTheory.Measure B)
  (A : X → B → E) (rho : E) (W : ℝ)
  (c : E → ℂ) (f : X → ℂ)
  (conv : E → X → ℂ)
  (hconv :
    ∀ (lam : E) (x : X),
      ∫ (b : B),
          SymmetricSpace.helgasonFourier μ
              A rho f lam b *
            SymmetricSpace.horosphericalCharacter
              rho lam (A x b) ∂nu =
        conv lam x)
  (hsph :
    ∀ (x : X),
      ∫ (lam : E),
          ↑(SymmetricSpace.plancherelDensity
                W c lam) *
            conv lam x ∂mua =
        f x) :
  SymmetricSpace.HasHelgasonInversion μ
    mua nu A rho W c f

**The reduction of Helgason's proof.** The inversion formula holds as soon as

* `hconv`: the boundary integral `∫_B f̂(λ,b) e^{(iλ+ϱ)(A(x,b))} db` equals a function `conv λ x`
  — in the group setting the convolution `(f × φ_λ)(x)`, by Lemma 1.2 of
  *Geometric Analysis on Symmetric Spaces*, Ch. III §1, which is where the symmetry of the
  spherical function is used; and
* `hsph`: that function is inverted by the Plancherel density, `∫_{𝔞*} κ(λ) conv λ x dλ = f(x)`
  — Harish-Chandra's inversion formula for the spherical transform.

The proof is then only bookkeeping: the density does not depend on `b`, so it comes out of the
boundary integral. What the statement buys is the separation of the two inputs, and in particular
the isolation of the one deep analytic fact.

The c-function is taken to be the integral c(\lambda)=\int_{\bar N}e^{-(i\lambda+\varrho)(H(\bar n))}\,\mathrm d\bar n, not the Gindikin--Karpelevich product of Gamma factors, which is a theorem about that integral. The reason is normalization. Helgason normalizes c so that c(-i\varrho)=1 in the introduction to Groups and Geometric Analysis, and writes the inversion formula of Geometric Analysis on Symmetric Spaces Ch. III Thm 1.3 against a measure \mathrm d\lambda on \mathfrak a^* that is not Lebesgue measure; put together with Lebesgue \mathrm d\lambda the two disagree by a power of \pi. Keeping \mathrm d\bar n visible forces the constant to come out of a proof instead of being copied. Only the modulus of c ever enters, and changing c without changing its modulus does not change the density — so a discrepancy in a power of \pi cannot be a phase convention and must be a normalization of the measures.

The last declaration is the shape of Helgason's proof, and its value is that it says which input is deep. The inversion formula follows from two hypotheses: that the boundary integral is the convolution f\times\varphi_\lambda with the spherical function, which is Lemma 1.2 of Ch. III §1 and rests on the symmetry of the spherical function — a cocycle computation, nontrivial but formal; and Harish-Chandra's inversion formula for the spherical transform, which is the genuinely deep analytic fact. Neither hypothesis mentions a group, which is why the reduction can be stated before any of the Lie theory exists.

The Poincaré ball model of real hyperbolic space

Theorem5.8.5

uses 1

Used by 3

Reverse dependency previews

Preview

Definition 3.1.13

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Poincaré ball model of real hyperbolic space. Mathlib has the upper half plane with its hyperbolic metric, but only in dimension two, and no hyperbolic space of general dimension. The rank-one noncompact symmetric space \mathbb H^m=SO^+(1,m)/O(m) is built here in the ball model, with the composite distance \langle x,u\rangle=\log\bigl((1-\|x\|^2)/\|x-u\|^2\bigr) and \varrho=(m-1)/2.

Lean code for Theorem5.8.5●16 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

def HyperbolicSpace.poincareBall.{u_2} (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] : Set E

def HyperbolicSpace.poincareBall.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] : Set E

Implementation after :=

:=
  ball (0 : E) 1

The Poincaré ball model of real hyperbolic space: the open unit ball of a Euclidean space.
The dimension of the space is the dimension of `ℍ^m`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

def HyperbolicSpace.idealBoundary.{u_2} (E : Type u_2)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Set E

def HyperbolicSpace.idealBoundary.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] : Set E

Implementation after :=

:=
  sphere (0 : E) 1

The ideal boundary `∂ℍ^m = 𝕊^{m-1}`, the unit sphere.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.mem_poincareBall_iff.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} :
  x ∈ HyperbolicSpace.poincareBall E ↔ ‖x‖ < 1

theorem HyperbolicSpace.mem_poincareBall_iff.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x : E} :
  x ∈ HyperbolicSpace.poincareBall E ↔
    ‖x‖ < 1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.mem_idealBoundary_iff.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E} :
  u ∈ HyperbolicSpace.idealBoundary E ↔ ‖u‖ = 1

theorem HyperbolicSpace.mem_idealBoundary_iff.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u : E} :
  u ∈ HyperbolicSpace.idealBoundary E ↔
    ‖u‖ = 1

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

def HyperbolicSpace.poissonKernel.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] (x u : E) : ℝ

def HyperbolicSpace.poissonKernel.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (x u : E) : ℝ

Implementation after :=

:= (1 - ‖x‖ ^ 2) / ‖x - u‖ ^ 2

The Poisson kernel of the ball, `P(x,u) = (1 - ‖x‖²)/‖x - u‖²`.

Its logarithm is the composite distance and its `ϱ`-th power is the weight `e^{ϱ⟨x,u⟩}` that a
layer of a network on `ℍ^m` carries. For `m = 2` it is the classical Poisson kernel of the disk;
for `m > 2` the classical Euclidean one is `(1-‖x‖²)/‖x-u‖^m`, and the two differ because the
hyperbolic and the Euclidean Laplacians only share their harmonic functions in dimension two.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

def HyperbolicSpace.compositeDistance.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] (x u : E) : ℝ

def HyperbolicSpace.compositeDistance.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (x u : E) : ℝ

Implementation after :=

:= Real.log (poissonKernel x u)

The rank-one vector-valued composite distance `⟨x,u⟩ = log((1 - ‖x‖²)/‖x - u‖²)`, the signed
distance from the origin to the horosphere through `x` with normal `u`.

The rank of `ℍ^m` is one, so `𝔞 ≅ ℝ` and the "vector-valued" distance is a scalar.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

def HyperbolicSpace.rho.{u_2} (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] : ℝ

def HyperbolicSpace.rho.{u_2} (E : Type u_2)
  [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] : ℝ

Implementation after :=

:=
  ((Module.finrank ℝ E : ℝ) - 1) / 2

The half-sum of the positive restricted roots of `ℍ^m`, `ϱ = (m-1)/2`, as an element of
`𝔞* ≅ ℝ`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.ne_of_mem_ball_of_mem_sphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] {x u : E} (hx : ‖x‖ < 1) (hu : ‖u‖ = 1) : x ≠ u

theorem HyperbolicSpace.ne_of_mem_ball_of_mem_sphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {x u : E} (hx : ‖x‖ < 1)
  (hu : ‖u‖ = 1) : x ≠ u

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.one_sub_norm_sq_pos.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] {x : E} (hx : ‖x‖ < 1) : 0 < 1 - ‖x‖ ^ 2

theorem HyperbolicSpace.one_sub_norm_sq_pos.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {x : E} (hx : ‖x‖ < 1) : 0 < 1 - ‖x‖ ^ 2

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.poissonKernel_pos.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] {x u : E} (hx : ‖x‖ < 1) (hu : ‖u‖ = 1) :
  0 < HyperbolicSpace.poissonKernel x u

theorem HyperbolicSpace.poissonKernel_pos.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {x u : E} (hx : ‖x‖ < 1)
  (hu : ‖u‖ = 1) :
  0 < HyperbolicSpace.poissonKernel x u

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.poissonKernel_origin.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] {u : E} (hu : ‖u‖ = 1) :
  HyperbolicSpace.poissonKernel 0 u = 1

theorem HyperbolicSpace.poissonKernel_origin.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {u : E} (hu : ‖u‖ = 1) :
  HyperbolicSpace.poissonKernel 0 u = 1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.compositeDistance_origin.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] {u : E} (hu : ‖u‖ = 1) :
  HyperbolicSpace.compositeDistance 0 u = 0

theorem HyperbolicSpace.compositeDistance_origin.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {u : E} (hu : ‖u‖ = 1) :
  HyperbolicSpace.compositeDistance 0 u =
    0

The origin of the ball lies on every horosphere through it: the composite distance from the
origin to a boundary point vanishes. This is the normalization that makes `e^{(-iλ+ϱ)⟨x,u⟩}` the
analogue of a plane wave based at the origin.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.exp_compositeDistance.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] {x u : E} (hx : ‖x‖ < 1) (hu : ‖u‖ = 1) :
  Real.exp (HyperbolicSpace.compositeDistance x u) =
    HyperbolicSpace.poissonKernel x u

theorem HyperbolicSpace.exp_compositeDistance.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  {x u : E} (hx : ‖x‖ < 1)
  (hu : ‖u‖ = 1) :
  Real.exp
      (HyperbolicSpace.compositeDistance x
        u) =
    HyperbolicSpace.poissonKernel x u

Inside the ball the Poisson kernel is positive, so it is recovered from the composite
distance.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

def HyperbolicSpace.volumeDensity.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : ℝ

def HyperbolicSpace.volumeDensity.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (x : E) : ℝ

Implementation after :=

:= (2 / (1 - ‖x‖ ^ 2)) ^ (Module.finrank ℝ E)

The density of the `G`-invariant measure of `ℍ^m` against Lebesgue measure in the Poincaré ball
model, `(2/(1 - ‖x‖²))^m`. It is the Riemannian volume density of the metric
`4(1 - ‖x‖²)^{-2}∑ dx_i ⊗ dx_i`, but is taken here as a definition so that no manifold theory is
needed.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

theorem HyperbolicSpace.volumeDensity_pos.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {x : E} (hx : ‖x‖ < 1) : 0 < HyperbolicSpace.volumeDensity x

theorem HyperbolicSpace.volumeDensity_pos.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {x : E}
  (hx : ‖x‖ < 1) :
  0 < HyperbolicSpace.volumeDensity x

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BallModel.lean

complete

def HyperbolicSpace.invariantMeasure.{u_2} (E : Type u_2)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] : MeasureTheory.Measure E

def HyperbolicSpace.invariantMeasure.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] :
  MeasureTheory.Measure E

Implementation after :=

:=
  (volume.restrict (poincareBall E)).withDensity fun x => ENNReal.ofReal (volumeDensity x)

The `G`-invariant measure of `ℍ^m` in the Poincaré ball model. Its invariance under the Möbius
transformations of the ball is the content of a later file; here it is only defined.

It is a measure on the whole space rather than on the ball as a subtype, concentrated on the ball
by the restriction. That keeps `ℍ^m` a plain Euclidean space for every downstream construction and
avoids carrying a subtype through the Helgason--Fourier theory; nothing outside the ball is ever
seen, since the density is integrated against the restricted measure.

No Riemannian geometry is used, and none is available: Mathlib's manifold library has neither a volume measure nor a Laplace--Beltrami operator. The invariant measure is therefore defined as the weighted Lebesgue measure (2/(1-\|x\|^2))^m\,\mathrm dx on the open unit ball, and its agreement with the Riemannian volume of the metric 4(1-\|x\|^2)^{-2}\sum\mathrm dx_i\otimes\mathrm dx_i is a remark rather than a dependency. In the ball model the origin lies on every horosphere through it, so \langle 0,u\rangle=0 at every boundary point — that normalization is what makes e^{(-i\lambda+\varrho)\langle x,u\rangle} the analogue of a plane wave based at the origin.

Theorem5.8.6

uses 1

Used by 3

Reverse dependency previews

Preview

Definition 3.1.13

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Möbius transformations of the ball, and the cocycle of the composite distance. The isometries of \mathbb H^m that move the origin are the Möbius transformations. With Ahlfors' bracket [x,a]^2=1-2\langle x,a\rangle+\|x\|^2\|a\|^2 and \varphi_a(x)=\bigl((1-\|a\|^2)(x-a)-\|x-a\|^2a\bigr)/[x,a]^2, everything in this node follows from one polynomial identity, and the last declaration is the cocycle \langle\varphi_a x,\varphi_a u\rangle=\langle x,u\rangle-\langle a,u\rangle that the abstract layer asks a model to supply.

Lean code for Theorem5.8.6●21 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

def HyperbolicSpace.mobiusBracketSq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x a : E) : ℝ

def HyperbolicSpace.mobiusBracketSq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (x a : E) : ℝ

Implementation after :=

:= 1 - 2 * (inner ℝ x a : ℝ) + ‖x‖ ^ 2 * ‖a‖ ^ 2

Ahlfors' bracket, `[x,a]² = 1 - 2⟪x,a⟫ + ‖x‖²‖a‖²`, the denominator of the Möbius
transformation of the unit ball.

For a boundary point it is the squared Euclidean distance to `a`
(`mobiusBracketSq_of_norm_eq_one`), which is why the transformation law of the Poisson kernel comes
out as cleanly as it does.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobiusBracketSq_zero_right.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) :
  HyperbolicSpace.mobiusBracketSq x 0 = 1

theorem HyperbolicSpace.mobiusBracketSq_zero_right.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (x : E) :
  HyperbolicSpace.mobiusBracketSq x 0 = 1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobiusBracketSq_zero_left.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) :
  HyperbolicSpace.mobiusBracketSq 0 a = 1

theorem HyperbolicSpace.mobiusBracketSq_zero_left.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E) :
  HyperbolicSpace.mobiusBracketSq 0 a = 1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobiusBracketSq_of_norm_eq_one.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E} (hu : ‖u‖ = 1)
  (a : E) : HyperbolicSpace.mobiusBracketSq u a = ‖u - a‖ ^ 2

theorem HyperbolicSpace.mobiusBracketSq_of_norm_eq_one.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u : E}
  (hu : ‖u‖ = 1) (a : E) :
  HyperbolicSpace.mobiusBracketSq u a =
    ‖u - a‖ ^ 2

On the boundary the bracket is the squared Euclidean distance.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.one_sub_mul_sq_le_mobiusBracketSq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x a : E) :
  (1 - ‖x‖ * ‖a‖) ^ 2 ≤ HyperbolicSpace.mobiusBracketSq x a

theorem HyperbolicSpace.one_sub_mul_sq_le_mobiusBracketSq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (x a : E) :
  (1 - ‖x‖ * ‖a‖) ^ 2 ≤
    HyperbolicSpace.mobiusBracketSq x a

Cauchy--Schwarz bounds the bracket below by `(1 - ‖x‖‖a‖)²`. This is the only inequality in the
file, and it is what makes the bracket positive on the *closed* ball.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobiusBracketSq_pos.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  0 < HyperbolicSpace.mobiusBracketSq x a

theorem HyperbolicSpace.mobiusBracketSq_pos.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  0 < HyperbolicSpace.mobiusBracketSq x a

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobiusBracketSq_ne_zero.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobiusBracketSq x a ≠ 0

theorem HyperbolicSpace.mobiusBracketSq_ne_zero.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobiusBracketSq x a ≠ 0

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

def HyperbolicSpace.mobiusNum.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) : E

def HyperbolicSpace.mobiusNum.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) : E

Implementation after :=

:= (1 - ‖a‖ ^ 2) • (x - a) - ‖x - a‖ ^ 2 • a

The numerator of the Möbius transformation, `N_x = (1-‖a‖²)(x-a) - ‖x-a‖² a`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

def HyperbolicSpace.mobius.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) : E

def HyperbolicSpace.mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) : E

Implementation after :=

:= (mobiusBracketSq x a)⁻¹ • mobiusNum a x

**The Möbius transformation of the unit ball** carrying `a` to the origin,
`φ_a(x) = ((1-‖a‖²)(x-a) - ‖x-a‖² a)/[x,a]²`.

In one dimension this is `x ↦ (x-a)/(1-ax)`. It sends `a` to `0` and `0` to `-a`; the involution
that swaps them is its negative.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobius_self.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E) : HyperbolicSpace.mobius a a = 0

theorem HyperbolicSpace.mobius_self.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E) :
  HyperbolicSpace.mobius a a = 0

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobius_zero_left.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) :
  HyperbolicSpace.mobius 0 x = x

theorem HyperbolicSpace.mobius_zero_left.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (x : E) :
  HyperbolicSpace.mobius 0 x = x

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobius_zero_right.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) :
  HyperbolicSpace.mobius a 0 = -a

theorem HyperbolicSpace.mobius_zero_right.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E) :
  HyperbolicSpace.mobius a 0 = -a

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.mobiusNum_key.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a x y : E) :
  HyperbolicSpace.mobiusBracketSq y a * ‖x - a‖ ^ 2 +
        HyperbolicSpace.mobiusBracketSq x a * ‖y - a‖ ^ 2 -
      2 *
        inner ℝ (HyperbolicSpace.mobiusNum a x)
          (HyperbolicSpace.mobiusNum a y) =
    (1 - ‖a‖ ^ 2) ^ 2 * ‖x - y‖ ^ 2

theorem HyperbolicSpace.mobiusNum_key.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x y : E) :
  HyperbolicSpace.mobiusBracketSq y a *
          ‖x - a‖ ^ 2 +
        HyperbolicSpace.mobiusBracketSq x
            a *
          ‖y - a‖ ^ 2 -
      2 *
        inner ℝ
          (HyperbolicSpace.mobiusNum a x)
          (HyperbolicSpace.mobiusNum a
            y) =
    (1 - ‖a‖ ^ 2) ^ 2 * ‖x - y‖ ^ 2

**The identity the file rests on.** In terms of the numerators `N_x`, `N_y` and the brackets,

`[y,a]²‖x-a‖² + [x,a]²‖y-a‖² - 2⟪N_x,N_y⟫ = (1-‖a‖²)²‖x-y‖²`.

It is a polynomial identity in the six scalars, so `ring` proves it; no geometry enters.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.norm_sq_mobiusNum.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a x : E) :
  ‖HyperbolicSpace.mobiusNum a x‖ ^ 2 =
    ‖x - a‖ ^ 2 * HyperbolicSpace.mobiusBracketSq x a

theorem HyperbolicSpace.norm_sq_mobiusNum.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) :
  ‖HyperbolicSpace.mobiusNum a x‖ ^ 2 =
    ‖x - a‖ ^ 2 *
      HyperbolicSpace.mobiusBracketSq x a

The diagonal case: `‖N_x‖² = ‖x-a‖² [x,a]²`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.norm_sq_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a x‖ ^ 2 =
    ‖x - a‖ ^ 2 / HyperbolicSpace.mobiusBracketSq x a

theorem HyperbolicSpace.norm_sq_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a x‖ ^ 2 =
    ‖x - a‖ ^ 2 /
      HyperbolicSpace.mobiusBracketSq x a

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.one_sub_norm_sq_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  1 - ‖HyperbolicSpace.mobius a x‖ ^ 2 =
    (1 - ‖a‖ ^ 2) * (1 - ‖x‖ ^ 2) / HyperbolicSpace.mobiusBracketSq x a

theorem HyperbolicSpace.one_sub_norm_sq_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  1 - ‖HyperbolicSpace.mobius a x‖ ^ 2 =
    (1 - ‖a‖ ^ 2) * (1 - ‖x‖ ^ 2) /
      HyperbolicSpace.mobiusBracketSq x a

`1 - ‖φ_a(x)‖² = (1-‖a‖²)(1-‖x‖²)/[x,a]²`: the identity from which both the preservation of the
ball and the transformation law of the Poisson kernel follow.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.norm_mobius_lt_one.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) : ‖HyperbolicSpace.mobius a x‖ < 1

theorem HyperbolicSpace.norm_mobius_lt_one.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a x‖ < 1

The Möbius transformation maps the open ball into itself.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.norm_mobius_eq_one.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u a : E}
  (hu : ‖u‖ = 1) (ha : ‖a‖ < 1) : ‖HyperbolicSpace.mobius a u‖ = 1

theorem HyperbolicSpace.norm_mobius_eq_one.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u a : E}
  (hu : ‖u‖ = 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a u‖ = 1

The Möbius transformation maps the boundary sphere into itself.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.norm_sq_mobius_sub.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x y a : E}
  (hx : ‖x‖ ≤ 1) (hy : ‖y‖ ≤ 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a x - HyperbolicSpace.mobius a y‖ ^ 2 =
    (1 - ‖a‖ ^ 2) ^ 2 * ‖x - y‖ ^ 2 /
      (HyperbolicSpace.mobiusBracketSq x a *
        HyperbolicSpace.mobiusBracketSq y a)

theorem HyperbolicSpace.norm_sq_mobius_sub.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x y a : E}
  (hx : ‖x‖ ≤ 1) (hy : ‖y‖ ≤ 1)
  (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a x -
          HyperbolicSpace.mobius a y‖ ^
      2 =
    (1 - ‖a‖ ^ 2) ^ 2 * ‖x - y‖ ^ 2 /
      (HyperbolicSpace.mobiusBracketSq x
          a *
        HyperbolicSpace.mobiusBracketSq y
          a)

**The conformal distortion identity**,
`‖φ_a(x) - φ_a(y)‖² = (1-‖a‖²)²‖x-y‖²/([x,a]²[y,a]²)`.

The distortion depends on the two points only through the two brackets, which is conformality: in
the limit `y → x` it says the derivative of `φ_a` at `x` is `(1-‖a‖²)/[x,a]²` times a linear
isometry. That is what a later file will read the Jacobian of the invariant measure off.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.poissonKernel_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x u a : E}
  (hx : ‖x‖ < 1) (hu : ‖u‖ = 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.poissonKernel (HyperbolicSpace.mobius a x)
      (HyperbolicSpace.mobius a u) =
    HyperbolicSpace.poissonKernel x u /
      HyperbolicSpace.poissonKernel a u

theorem HyperbolicSpace.poissonKernel_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x u a : E}
  (hx : ‖x‖ < 1) (hu : ‖u‖ = 1)
  (ha : ‖a‖ < 1) :
  HyperbolicSpace.poissonKernel
      (HyperbolicSpace.mobius a x)
      (HyperbolicSpace.mobius a u) =
    HyperbolicSpace.poissonKernel x u /
      HyperbolicSpace.poissonKernel a u

**The transformation law of the Poisson kernel**, `P(φ_a x, φ_a u) = P(x,u)/P(a,u)`.

Dividing the two preceding identities cancels the brackets at `x` completely and leaves the bracket
at the boundary point, which is `‖u-a‖²` there — that is `P(a,u)^{-1}` up to `1-‖a‖²`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/Mobius.lean

complete

theorem HyperbolicSpace.compositeDistance_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x u a : E}
  (hx : ‖x‖ < 1) (hu : ‖u‖ = 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.compositeDistance (HyperbolicSpace.mobius a x)
      (HyperbolicSpace.mobius a u) =
    HyperbolicSpace.compositeDistance x u -
      HyperbolicSpace.compositeDistance a u

theorem HyperbolicSpace.compositeDistance_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x u a : E}
  (hx : ‖x‖ < 1) (hu : ‖u‖ = 1)
  (ha : ‖a‖ < 1) :
  HyperbolicSpace.compositeDistance
      (HyperbolicSpace.mobius a x)
      (HyperbolicSpace.mobius a u) =
    HyperbolicSpace.compositeDistance x
        u -
      HyperbolicSpace.compositeDistance a
        u

**The cocycle of the composite distance**, `⟨φ_a x, φ_a u⟩ = ⟨x,u⟩ - ⟨a,u⟩`.

This is the identity the abstract Helgason--Fourier layer asks of a model: it is what turns the
action of the isometry group on `ℍ^m` into a multiplier on the Helgason--Fourier kernel, since the
kernel is the exponential of a linear functional of the composite distance and so is multiplicative
in it.

The identity is this. Writing N_x for the numerator of \varphi_a(x), [y,a]^2\|x-a\|^2+[x,a]^2\|y-a\|^2-2\langle N_x,N_y\rangle=(1-\|a\|^2)^2\|x-y\|^2, which is a polynomial identity in the six scalars \langle x,y\rangle, \langle x,a\rangle, \langle y,a\rangle, \|x\|^2, \|y\|^2, \|a\|^2 — so ring proves it once the inner products are expanded, with no geometry entering at all. Everything else is division. On the diagonal it gives \|\varphi_a(x)\|^2=\|x-a\|^2/[x,a]^2 and hence 1-\|\varphi_a(x)\|^2=(1-\|a\|^2)(1-\|x\|^2)/[x,a]^2, from which the ball and its boundary sphere are preserved. Off the diagonal it gives the conformal distortion \|\varphi_a(x)-\varphi_a(y)\|^2=(1-\|a\|^2)^2\|x-y\|^2/([x,a]^2[y,a]^2), in which the two points enter only through their brackets. Dividing the two, and using that on the boundary the bracket is the squared Euclidean distance, gives P(\varphi_a x,\varphi_a u)=P(x,u)/P(a,u) — the cocycle, once logarithms are taken.

Positivity of the bracket is not a computation either: Cauchy--Schwarz gives (1-\|x\|\|a\|)^2\le[x,a]^2, which is positive as soon as \|x\|\le 1 and \|a\|<1, so the closed ball is covered and the boundary needs no separate argument.

What is not here is invariance of the volume measure, which needs the Jacobian and hence the derivative of \varphi_a. The conformal distortion identity is the statement that will be read off: a map whose difference quotients are a fixed scalar times an isometry has derivative a scalar times an isometry, and such a derivative has determinant of modulus \lambda^m — exactly the factor the density (2/(1-\|x\|^2))^m needs in order to be invariant.

Theorem5.8.7

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 3.1.13

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The invariant measure of hyperbolic space is Möbius invariant. The measure (2/(1-\|x\|^2))^m\,\mathrm dx on the unit ball is preserved by every \varphi_a. This completes the geometry of the model: the isometry group acts on ℍ^m preserving both the measure and, by the cocycle, the Helgason--Fourier kernel.

Lean code for Theorem5.8.7●21 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

def HyperbolicSpace.mobiusInvol.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) : E

def HyperbolicSpace.mobiusInvol.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) : E

Implementation after :=

:= -mobius a x

The involution of the unit ball swapping the origin and `a`,
`σ_a(x) = (‖x-a‖² a - (1-‖a‖²)(x-a))/[x,a]²`. It is the negative of `HyperbolicSpace.mobius`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

theorem HyperbolicSpace.mobiusInvol_eq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a y : E) :
  HyperbolicSpace.mobiusInvol a y =
    (HyperbolicSpace.mobiusBracketSq y a)⁻¹ •
      (‖y - a‖ ^ 2 • a - (1 - ‖a‖ ^ 2) • (y - a))

theorem HyperbolicSpace.mobiusInvol_eq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a y : E) :
  HyperbolicSpace.mobiusInvol a y =
    (HyperbolicSpace.mobiusBracketSq y
          a)⁻¹ •
      (‖y - a‖ ^ 2 • a -
        (1 - ‖a‖ ^ 2) • (y - a))

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

theorem HyperbolicSpace.mobiusBracketSq_eq_add.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (y a : E) :
  HyperbolicSpace.mobiusBracketSq y a =
    ‖y - a‖ ^ 2 + (1 - ‖y‖ ^ 2) * (1 - ‖a‖ ^ 2)

theorem HyperbolicSpace.mobiusBracketSq_eq_add.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (y a : E) :
  HyperbolicSpace.mobiusBracketSq y a =
    ‖y - a‖ ^ 2 +
      (1 - ‖y‖ ^ 2) * (1 - ‖a‖ ^ 2)

The bracket differs from the squared Euclidean distance by the product of the two "defects"
from the boundary: `[y,a]² = ‖y-a‖² + (1-‖y‖²)(1-‖a‖²)`.

This is the only relation between the bracket and the Poisson kernel that is needed, and it is what
makes the bracket of an image point computable from the image's norm.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

theorem HyperbolicSpace.mobiusInvol_sub_self.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hB : HyperbolicSpace.mobiusBracketSq x a ≠ 0) :
  HyperbolicSpace.mobiusInvol a x - a =
    -((1 - ‖a‖ ^ 2) / HyperbolicSpace.mobiusBracketSq x a) •
      (x - ‖x‖ ^ 2 • a)

theorem HyperbolicSpace.mobiusInvol_sub_self.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hB :
    HyperbolicSpace.mobiusBracketSq x a ≠
      0) :
  HyperbolicSpace.mobiusInvol a x - a =
    -((1 - ‖a‖ ^ 2) /
          HyperbolicSpace.mobiusBracketSq
            x a) •
      (x - ‖x‖ ^ 2 • a)

`σ_a(x) - a = -\frac{1-‖a‖²}{[x,a]²}(x - ‖x‖² a)`. Both sides are linear combinations of `x`
and `a`, so after the squared norms are expanded this is a scalar computation on each
coefficient.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

theorem HyperbolicSpace.norm_sq_mobiusInvol_sub_self.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobiusInvol a x - a‖ ^ 2 =
    (1 - ‖a‖ ^ 2) ^ 2 * ‖x‖ ^ 2 / HyperbolicSpace.mobiusBracketSq x a

theorem HyperbolicSpace.norm_sq_mobiusInvol_sub_self.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobiusInvol a x - a‖ ^
      2 =
    (1 - ‖a‖ ^ 2) ^ 2 * ‖x‖ ^ 2 /
      HyperbolicSpace.mobiusBracketSq x a

`‖σ_a(x) - a‖² = (1-‖a‖²)²‖x‖²/[x,a]²`, by taking norms in the previous identity and using
`‖x - ‖x‖² a‖² = ‖x‖² [x,a]²`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

theorem HyperbolicSpace.mobiusBracketSq_mobiusInvol.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobiusBracketSq (HyperbolicSpace.mobiusInvol a x) a =
    (1 - ‖a‖ ^ 2) ^ 2 / HyperbolicSpace.mobiusBracketSq x a

theorem HyperbolicSpace.mobiusBracketSq_mobiusInvol.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobiusBracketSq
      (HyperbolicSpace.mobiusInvol a x)
      a =
    (1 - ‖a‖ ^ 2) ^ 2 /
      HyperbolicSpace.mobiusBracketSq x a

`[σ_a(x),a]² = (1-‖a‖²)²/[x,a]²`. The two contributions to
`mobiusBracketSq_eq_add` at the image point are `(1-‖a‖²)²‖x‖²/[x,a]²` and
`(1-‖a‖²)²(1-‖x‖²)/[x,a]²`, and they add up with `‖x‖²` cancelling.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

theorem HyperbolicSpace.mobiusInvol_mobiusInvol.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobiusInvol a (HyperbolicSpace.mobiusInvol a x) = x

theorem HyperbolicSpace.mobiusInvol_mobiusInvol.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobiusInvol a
      (HyperbolicSpace.mobiusInvol a x) =
    x

**The involution property**, `σ_a(σ_a x) = x`. Substituting the three identities into the
definition of `σ_a` makes every bracket cancel.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

theorem HyperbolicSpace.injOn_mobius.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E} (ha : ‖a‖ < 1) :
  Set.InjOn (HyperbolicSpace.mobius a) (Metric.ball 0 1)

theorem HyperbolicSpace.injOn_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Set.InjOn (HyperbolicSpace.mobius a)
    (Metric.ball 0 1)

`φ_a` is injective on the ball: it is the negative of an involution.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusInverse.lean

complete

theorem HyperbolicSpace.image_mobius.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E} (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobius a '' Metric.ball 0 1 = Metric.ball 0 1

theorem HyperbolicSpace.image_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobius a ''
      Metric.ball 0 1 =
    Metric.ball 0 1

**`φ_a` maps the ball onto the ball.** Given `y` in the ball, `σ_a(-y)` is a preimage, because
`σ_a` is an involution of the ball and `φ_a = -σ_a`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.differentiable_mobiusBracketSq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) :
  Differentiable ℝ fun x ↦ HyperbolicSpace.mobiusBracketSq x a

theorem HyperbolicSpace.differentiable_mobiusBracketSq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E) :
  Differentiable ℝ fun x ↦
    HyperbolicSpace.mobiusBracketSq x a

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.differentiable_mobiusNum.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) :
  Differentiable ℝ (HyperbolicSpace.mobiusNum a)

theorem HyperbolicSpace.differentiable_mobiusNum.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E) :
  Differentiable ℝ
    (HyperbolicSpace.mobiusNum a)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.differentiableAt_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  DifferentiableAt ℝ (HyperbolicSpace.mobius a) x

theorem HyperbolicSpace.differentiableAt_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  DifferentiableAt ℝ
    (HyperbolicSpace.mobius a) x

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

def HyperbolicSpace.mobiusFactor.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) : ℝ

def HyperbolicSpace.mobiusFactor.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a x : E) : ℝ

Implementation after :=

:= (1 - ‖a‖ ^ 2) / mobiusBracketSq x a

The conformal factor of the Möbius transformation, `λ(x) = (1-‖a‖²)/[x,a]²`: the factor by
which `φ_a` scales lengths at `x`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.mobiusFactor_pos.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) : 0 < HyperbolicSpace.mobiusFactor a x

theorem HyperbolicSpace.mobiusFactor_pos.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ ≤ 1) (ha : ‖a‖ < 1) :
  0 < HyperbolicSpace.mobiusFactor a x

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.norm_sq_mobius_sub_eq_mul.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x y a : E}
  (hx : ‖x‖ ≤ 1) (hy : ‖y‖ ≤ 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a x - HyperbolicSpace.mobius a y‖ ^ 2 =
    HyperbolicSpace.mobiusFactor a x *
        HyperbolicSpace.mobiusFactor a y *
      ‖x - y‖ ^ 2

theorem HyperbolicSpace.norm_sq_mobius_sub_eq_mul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x y a : E}
  (hx : ‖x‖ ≤ 1) (hy : ‖y‖ ≤ 1)
  (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a x -
          HyperbolicSpace.mobius a y‖ ^
      2 =
    HyperbolicSpace.mobiusFactor a x *
        HyperbolicSpace.mobiusFactor a y *
      ‖x - y‖ ^ 2

The conformal distortion identity written with the factor: the squared distance between images
is `λ(x)λ(y)` times the squared distance between the points.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.norm_fderiv_mobius_apply.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) (v : E) :
  ‖(fderiv ℝ (HyperbolicSpace.mobius a) x) v‖ =
    HyperbolicSpace.mobiusFactor a x * ‖v‖

theorem HyperbolicSpace.norm_fderiv_mobius_apply.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) (v : E) :
  ‖(fderiv ℝ (HyperbolicSpace.mobius a) x)
        v‖ =
    HyperbolicSpace.mobiusFactor a x * ‖v‖

**`‖Dφ_a(x)v‖ = λ(x)‖v‖`.** The derivative is not computed: the slope of `φ_a` along the line
through `x` in direction `v` has squared norm `λ(x)λ(x+tv)‖v‖²` for every small `t ≠ 0`, by the
conformal distortion identity, and both sides converge as `t → 0`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.isConformalMap_fderiv_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) :
  IsConformalMap (fderiv ℝ (HyperbolicSpace.mobius a) x)

theorem HyperbolicSpace.isConformalMap_fderiv_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) :
  IsConformalMap
    (fderiv ℝ (HyperbolicSpace.mobius a)
      x)

The derivative of `φ_a` is a conformal linear map: it scales inner products by `λ(x)²`, which
follows from the norms by polarization.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.abs_det_fderiv_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [Nontrivial E] {x a : E} (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) :
  |(fderiv ℝ (HyperbolicSpace.mobius a) x).det| =
    HyperbolicSpace.mobiusFactor a x ^ Module.finrank ℝ E

theorem HyperbolicSpace.abs_det_fderiv_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  {x a : E} (hx : ‖x‖ < 1)
  (ha : ‖a‖ < 1) :
  |(fderiv ℝ (HyperbolicSpace.mobius a)
          x).det| =
    HyperbolicSpace.mobiusFactor a x ^
      Module.finrank ℝ E

**The Jacobian of the Möbius transformation**, `|det Dφ_a(x)| = λ(x)^m`.

The derivative is `λ(x)` times a linear isometry; a linear isometry has `normDet` one, and scaling
multiplies `normDet` by the `m`-th power of the modulus of the scalar.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.mobiusFactor_pow_mul_volumeDensity_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {x a : E} (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobiusFactor a x ^ Module.finrank ℝ E *
      HyperbolicSpace.volumeDensity (HyperbolicSpace.mobius a x) =
    HyperbolicSpace.volumeDensity x

theorem HyperbolicSpace.mobiusFactor_pow_mul_volumeDensity_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) :
  HyperbolicSpace.mobiusFactor a x ^
        Module.finrank ℝ E *
      HyperbolicSpace.volumeDensity
        (HyperbolicSpace.mobius a x) =
    HyperbolicSpace.volumeDensity x

The density of the invariant measure cancels the Jacobian:
`λ(x)^m (2/(1-‖φ_a(x)‖²))^m = (2/(1-‖x‖²))^m`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.measurable_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E]
  [BorelSpace E] [FiniteDimensional ℝ E] (a : E) :
  Measurable (HyperbolicSpace.mobius a)

theorem HyperbolicSpace.measurable_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (a : E) :
  Measurable (HyperbolicSpace.mobius a)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/MobiusMeasure.lean

complete

theorem HyperbolicSpace.lintegral_invariantMeasure_comp_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E] [MeasurableSpace E]
  [BorelSpace E] {a : E} (ha : ‖a‖ < 1) {g : E → ENNReal}
  (hg : Measurable g) :
  ∫⁻ (x : E),
      g
        (HyperbolicSpace.mobius a
          x) ∂HyperbolicSpace.invariantMeasure E =
    ∫⁻ (x : E), g x ∂HyperbolicSpace.invariantMeasure E

theorem HyperbolicSpace.lintegral_invariantMeasure_comp_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E]
  {a : E} (ha : ‖a‖ < 1) {g : E → ENNReal}
  (hg : Measurable g) :
  ∫⁻ (x : E),
      g
        (HyperbolicSpace.mobius a
          x) ∂HyperbolicSpace.invariantMeasure
        E =
    ∫⁻ (x : E),
      g
        x ∂HyperbolicSpace.invariantMeasure
        E

**The invariant measure of `ℍ^m` is Möbius invariant.**

The change of variables along `φ_a` needs three inputs and no more: differentiability, injectivity
on the ball, and that the image of the ball is the ball. The density then cancels the Jacobian
pointwise, and what is left is the same integral.

The derivative of \varphi_a is never computed. Differentiating a rational map of a vector and evaluating a determinant would be a long calculation; the conformal distortion identity already contains the answer. Writing \lambda(x)=(1-\|a\|^2)/[x,a]^2, the identity reads \|\varphi_a(x)-\varphi_a(y)\|^2=\lambda(x)\lambda(y)\|x-y\|^2, so the slope of \varphi_a along a line through x in direction v has squared norm \lambda(x)\lambda(x+tv)\|v\|^2 for every small t\ne 0; letting t\to 0 gives \|D\varphi_a(x)v\|=\lambda(x)\|v\| whatever the derivative is. By polarization the derivative then scales inner products by \lambda(x)^2, so it is conformal, so it is \lambda(x) times a linear isometry, so |\det|=\lambda(x)^m — using that a linear isometry has normDet one and that scaling multiplies normDet by a power of the modulus. Only differentiability is taken from calculus.

Surjectivity onto the ball is the other input, and it comes from the involution \sigma_a=-\varphi_a, which swaps 0 and a. Proving \sigma_a\circ\sigma_a=\mathrm{id} by brute force would mean normalizing a large rational expression; instead it factors through three identities that are each one ring: \sigma_a(x)-a=-\lambda(x)(x-\|x\|^2a), then \|\sigma_a(x)-a\|^2=\lambda(x)^2[x,a]^2\|x\|^2 in the form (1-\|a\|^2)^2\|x\|^2/[x,a]^2, and then [\sigma_a(x),a]^2=(1-\|a\|^2)^2/[x,a]^2. Substituting the three makes every bracket cancel. Injectivity is then free, an involution being injective. The third identity is where the general relation [y,a]^2=\|y-a\|^2+(1-\|y\|^2)(1-\|a\|^2) between the bracket and the Poisson kernel is used.

With the Jacobian and the bijection the invariance is the change of variables of MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, and the density cancels the Jacobian pointwise: \lambda(x)^m(2/(1-\|\varphi_a(x)\|^2))^m=(2/(1-\|x\|^2))^m, because 1-\|\varphi_a(x)\|^2=(1-\|a\|^2)(1-\|x\|^2)/[x,a]^2. That is the same identity which made \varphi_a preserve the ball, so the invariance of the measure and the preservation of the ball are two readings of one computation.

Theorem5.8.8

Statement uses 4

Statement dependency previews

Preview

Theorem 5.7.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Definition 3.1.13

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Helgason--Fourier transform on hyperbolic space, and its inversion formula as a proposition. Feeding the ball model to the abstract layer turns the inversion formula from a schema into a definite claim about a definite space, which is what was missing while no model existed: HasInversion is a proposition one can be asked to prove.

Lean code for Theorem5.8.8●11 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

def HyperbolicSpace.boundaryMeasure.{u_2} (E : Type u_2)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] :
  MeasureTheory.Measure ↑(Metric.sphere 0 1)

def HyperbolicSpace.boundaryMeasure.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] :
  MeasureTheory.Measure
    ↑(Metric.sphere 0 1)

Implementation after :=

:=
  ((volume : Measure E).toSphere univ)⁻¹ • (volume : Measure E).toSphere

The uniform probability measure on the ideal boundary `∂ℍ^m = 𝕊^{m-1}`: Mathlib's surface
measure divided by its total mass.

Normalizing here rather than carrying the total mass through the theory is what makes the boundary
integral of the inversion formula an average, which is the form the Helgason--Fourier theory uses
(`∫ db = 1`).

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

theorem HyperbolicSpace.instIsProbabilityMeasureBoundaryMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] :
  MeasureTheory.IsProbabilityMeasure (HyperbolicSpace.boundaryMeasure E)

theorem HyperbolicSpace.instIsProbabilityMeasureBoundaryMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] :
  MeasureTheory.IsProbabilityMeasure
    (HyperbolicSpace.boundaryMeasure E)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

theorem HyperbolicSpace.boundaryMeasure_eq_sphereOrbitMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E] (v : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryMeasure E = MeasureTheory.sphereOrbitMeasure v

theorem HyperbolicSpace.boundaryMeasure_eq_sphereOrbitMeasure.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [Nontrivial E]
  (v : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryMeasure E =
    MeasureTheory.sphereOrbitMeasure v

The boundary measure is the rotation-invariant probability measure on the sphere: it is the
orbit measure of any unit vector under the orthogonal group. So the normalization chosen above is
not a choice at all — it is the only rotation-invariant one.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

def HyperbolicSpace.boundaryDistance.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] (x : E) (u : ↑(Metric.sphere 0 1)) : ℝ

def HyperbolicSpace.boundaryDistance.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (x : E) (u : ↑(Metric.sphere 0 1)) : ℝ

Implementation after :=

:= compositeDistance x (u : E)

The composite distance read as a function of a point of the boundary sphere, which is the form
the Helgason--Fourier theory consumes.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

theorem HyperbolicSpace.boundaryDistance_origin.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryDistance 0 u = 0

theorem HyperbolicSpace.boundaryDistance_origin.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryDistance 0 u = 0

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

theorem HyperbolicSpace.norm_horosphericalCharacter_compositeDistance.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] (t lam : ℝ) {x u : E}
  (hx : ‖x‖ < 1) (hu : ‖u‖ = 1) :
  ‖SymmetricSpace.horosphericalCharacter t lam
        (HyperbolicSpace.compositeDistance x u)‖ =
    HyperbolicSpace.poissonKernel x u ^ t

theorem HyperbolicSpace.norm_horosphericalCharacter_compositeDistance.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (t lam : ℝ) {x u : E} (hx : ‖x‖ < 1)
  (hu : ‖u‖ = 1) :
  ‖SymmetricSpace.horosphericalCharacter t
        lam
        (HyperbolicSpace.compositeDistance
          x u)‖ =
    HyperbolicSpace.poissonKernel x u ^ t

The modulus of the Helgason--Fourier kernel on `ℍ^m` is a real power of the Poisson kernel:
`|e^{(iλ+t)⟨x,u⟩}| = P(x,u)^t`, with no dependence on the frequency `λ`.

At `t = ϱ` this is the weight the layer of a network on `ℍ^m` carries, so the weight is
`P(x,u)^{(m-1)/2}` — the square root of the Euclidean Poisson kernel when `m = 2`, and in general
the half-density that makes the Helgason--Fourier transform an isometry.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

theorem HyperbolicSpace.horosphericalCharacter_compositeDistance_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  (t lam : ℝ) {x u a : E} (hx : ‖x‖ < 1) (hu : ‖u‖ = 1) (ha : ‖a‖ < 1) :
  SymmetricSpace.horosphericalCharacter t lam
      (HyperbolicSpace.compositeDistance (HyperbolicSpace.mobius a x)
        (HyperbolicSpace.mobius a u)) =
    SymmetricSpace.horosphericalCharacter t lam
        (HyperbolicSpace.compositeDistance x u) *
      SymmetricSpace.horosphericalCharacter t lam
        (-HyperbolicSpace.compositeDistance a u)

theorem HyperbolicSpace.horosphericalCharacter_compositeDistance_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (t lam : ℝ)
  {x u a : E} (hx : ‖x‖ < 1)
  (hu : ‖u‖ = 1) (ha : ‖a‖ < 1) :
  SymmetricSpace.horosphericalCharacter t
      lam
      (HyperbolicSpace.compositeDistance
        (HyperbolicSpace.mobius a x)
        (HyperbolicSpace.mobius a u)) =
    SymmetricSpace.horosphericalCharacter
        t lam
        (HyperbolicSpace.compositeDistance
          x u) *
      SymmetricSpace.horosphericalCharacter
        t lam
        (-HyperbolicSpace.compositeDistance
            a u)

**The Helgason--Fourier kernel is a cocycle for the Möbius action.** Moving the point and the
boundary normal together by the same Möbius transformation multiplies the kernel by a factor that
depends on the boundary normal alone:

`e^{(iλ+t)⟨φ_a x, φ_a u⟩} = e^{(iλ+t)⟨x,u⟩} · e^{-(iλ+t)⟨a,u⟩}`.

Two facts meet here and nothing else: the composite distance is a cocycle
(`compositeDistance_mobius`, an algebraic identity about the ball) and the kernel is the exponential
of a linear functional of it, hence multiplicative (`horosphericalCharacter_add`). This is the
mechanism by which the isometry group of `ℍ^m` acts on the Helgason--Fourier transform, and it is
what the abstract layer abstracts.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

def HyperbolicSpace.helgasonFourier.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (f : E → ℂ) (lam : ℝ)
  (u : ↑(Metric.sphere 0 1)) : ℂ

def HyperbolicSpace.helgasonFourier.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (f : E → ℂ) (lam : ℝ)
  (u : ↑(Metric.sphere 0 1)) : ℂ

Implementation after :=

:=
  SymmetricSpace.helgasonFourier (invariantMeasure E) boundaryDistance (rho E) f lam u

**The Helgason--Fourier transform on `ℍ^m`**,
`f̂(λ,u) = ∫ f(x) e^{(-iλ+ϱ)⟨x,u⟩} dμ(x) = ∫ f(x) P(x,u)^{ϱ-iλ} dμ(x)`,
with `μ` the invariant measure of the ball and `ϱ = (m-1)/2`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

theorem HyperbolicSpace.helgasonFourier_eq.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (f : E → ℂ) (lam : ℝ)
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.helgasonFourier f lam u =
    ∫ (x : E),
      f x *
        SymmetricSpace.horosphericalCharacter (HyperbolicSpace.rho E)
          (-lam)
          (HyperbolicSpace.boundaryDistance x
            u) ∂HyperbolicSpace.invariantMeasure E

theorem HyperbolicSpace.helgasonFourier_eq.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (f : E → ℂ) (lam : ℝ)
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.helgasonFourier f lam
      u =
    ∫ (x : E),
      f x *
        SymmetricSpace.horosphericalCharacter
          (HyperbolicSpace.rho E) (-lam)
          (HyperbolicSpace.boundaryDistance
            x
            u) ∂HyperbolicSpace.invariantMeasure
        E

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

def HyperbolicSpace.HasInversion.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] (W : ℝ) (c : ℝ → ℂ) (f : E → ℂ) : Prop

def HyperbolicSpace.HasInversion.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (W : ℝ) (c : ℝ → ℂ) (f : E → ℂ) : Prop

Implementation after :=

:=
  SymmetricSpace.HasHelgasonInversion (invariantMeasure E) (volume : Measure ℝ)
    (boundaryMeasure E) boundaryDistance (rho E) W c f

**The Helgason--Fourier inversion formula on real hyperbolic space**, as a proposition:

`f(x) = |W|^{-1} ∫_ℝ ∫_{𝕊^{m-1}} f̂(λ,u) e^{(iλ+ϱ)⟨x,u⟩} |c(λ)|^{-2} du dλ`.

Rank one, so the frequency variable is a real number and `dλ` is Lebesgue measure on `ℝ`. Fixing
`dλ` to be Lebesgue is deliberate: Helgason's inversion formula is written against a normalization
of `dλ` that is not Lebesgue measure, and the difference is exactly where the powers of `π` in the
constant live, so the constant has to be produced by a proof rather than quoted.

This is a statement, not a theorem. Proving it is the next stage; the route is through the Möbius
action of the ball, the Abel transform, and Harish-Chandra's inversion of the spherical transform,
and `SymmetricSpace.hasHelgasonInversion_of_spherical` is where those inputs meet.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/HelgasonFourier.lean

complete

theorem HyperbolicSpace.hasInversion_iff.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] (W : ℝ) (c : ℝ → ℂ) (f : E → ℂ) :
  HyperbolicSpace.HasInversion W c f ↔
    ∀ (x : E),
      ∫ (lam : ℝ),
          ∫ (u : ↑(Metric.sphere 0 1)),
            HyperbolicSpace.helgasonFourier f lam u *
                ↑(SymmetricSpace.plancherelDensity W c lam) *
              SymmetricSpace.horosphericalCharacter
                (HyperbolicSpace.rho E) lam
                (HyperbolicSpace.boundaryDistance x
                  u) ∂HyperbolicSpace.boundaryMeasure E =
        f x

theorem HyperbolicSpace.hasInversion_iff.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (W : ℝ) (c : ℝ → ℂ) (f : E → ℂ) :
  HyperbolicSpace.HasInversion W c f ↔
    ∀ (x : E),
      ∫ (lam : ℝ),
          ∫ (u : ↑(Metric.sphere 0 1)),
            HyperbolicSpace.helgasonFourier
                  f lam u *
                ↑(SymmetricSpace.plancherelDensity
                    W c lam) *
              SymmetricSpace.horosphericalCharacter
                (HyperbolicSpace.rho E)
                lam
                (HyperbolicSpace.boundaryDistance
                  x
                  u) ∂HyperbolicSpace.boundaryMeasure
              E =
        f x

The four pieces of data are all available. The space is the ambient Euclidean space carrying the invariant measure, which is concentrated on the ball — using the whole space rather than the ball as a subtype costs nothing and keeps every construction on a plain Euclidean space. The rank is one, so the frequency is a real number and \mathrm d\lambda is Lebesgue measure on \mathbb R; fixing it to be Lebesgue is deliberate, since Helgason writes the formula against a different normalization and that is exactly where the powers of \pi in the constant live. The boundary is the unit sphere with the normalized surface measure, and that normalization is not a choice: by the uniqueness theorem it is the orbit measure of any unit vector, hence the rotation-invariant probability measure. The Plancherel density keeps |W| and c as arguments, because pinning them down for \mathbb H^m is a normalization question to be settled by proof rather than by quotation.

One identity is worth naming on its own: the modulus of the Helgason--Fourier kernel is a real power of the Poisson kernel, |e^{(i\lambda+t)\langle x,u\rangle}|=P(x,u)^t, with no dependence on the frequency. At t=\varrho this is the weight a layer of a network on \mathbb H^m carries, so that weight is P(x,u)^{(m-1)/2} — the square root of the Euclidean Poisson kernel when m=2, and in general the half-density that makes the transform an isometry rather than an input-dependent coefficient.

The manifold of positive definite matrices

Theorem5.8.9

Statement uses 2

Statement dependency previews

Preview

Theorem 5.8.7

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

The Möbius transformation restricted to the ideal boundary is a conformal homeomorphism of the sphere whose multiplier is the Poisson kernel. \operatorname{dist}(\partial\varphi_a u,\partial\varphi_a v)=\sqrt{P(a,u)P(a,v)}\operatorname{dist}(u,v), so the chordal distance is multiplied by the geometric mean of the multiplier at the two endpoints. The inverse is the boundary restriction of the involution \sigma_a=-\varphi_a.

Lean code for Theorem5.8.9●19 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.mobiusFactor_eq_poissonKernel.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u a : E}
  (hu : ‖u‖ = 1) :
  HyperbolicSpace.mobiusFactor a u = HyperbolicSpace.poissonKernel a u

theorem HyperbolicSpace.mobiusFactor_eq_poissonKernel.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u a : E}
  (hu : ‖u‖ = 1) :
  HyperbolicSpace.mobiusFactor a u =
    HyperbolicSpace.poissonKernel a u

On the ideal boundary the conformal factor of the Möbius transformation is the Poisson kernel,
`λ_a(u) = P(a,u)`. Ahlfors' bracket `[u,a]²` is the squared Euclidean distance `‖u-a‖²` there, and
that is the denominator of `P(a,u)`. The hypothesis `‖a‖ < 1` is not needed: both sides are
quotients, and no positivity is used.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.norm_sq_mobius_sub_of_mem_sphere.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u v a : E}
  (hu : ‖u‖ = 1) (hv : ‖v‖ = 1) (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a u - HyperbolicSpace.mobius a v‖ ^ 2 =
    HyperbolicSpace.poissonKernel a u *
        HyperbolicSpace.poissonKernel a v *
      ‖u - v‖ ^ 2

theorem HyperbolicSpace.norm_sq_mobius_sub_of_mem_sphere.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {u v a : E}
  (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
  (ha : ‖a‖ < 1) :
  ‖HyperbolicSpace.mobius a u -
          HyperbolicSpace.mobius a v‖ ^
      2 =
    HyperbolicSpace.poissonKernel a u *
        HyperbolicSpace.poissonKernel a
          v *
      ‖u - v‖ ^ 2

**The Möbius transformation is conformal on the ideal boundary with multiplier the Poisson
kernel**: `‖φ_a u - φ_a v‖² = P(a,u) P(a,v) ‖u-v‖²` for boundary points `u`, `v`.

The squared chordal distance is multiplied by the product of the multipliers at the two endpoints,
which is conformality with multiplier `P(a,·)`: it is the conformal distortion identity of
`LeanRidgelet.ToMathlib.LieGroup.Hyperbolic.MobiusMeasure` with both factors read on the boundary
by `HyperbolicSpace.mobiusFactor_eq_poissonKernel`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

def HyperbolicSpace.boundaryMobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) : ↑(Metric.sphere 0 1)

def HyperbolicSpace.boundaryMobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E)
  (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  ↑(Metric.sphere 0 1)

Implementation after :=

:=
  ⟨mobius a (u : E),
    mem_sphere_zero_iff_norm.2 (norm_mobius_eq_one (mem_sphere_zero_iff_norm.1 u.2) ha)⟩

**The Möbius transformation on the ideal boundary**, `∂φ_a`: the restriction of `φ_a` to
`∂ℍ^m = 𝕊^{m-1}`, a self-map of the sphere by `HyperbolicSpace.norm_mobius_eq_one`.

The hypothesis `‖a‖ < 1` is an explicit argument rather than an instance or a bundled point of the
ball: it is exactly what the codomain claim needs, it is the form every lemma of this family takes
it in, and proof irrelevance makes the map independent of which proof is supplied.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.coe_boundaryMobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E} (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  ↑(HyperbolicSpace.boundaryMobius a ha u) = HyperbolicSpace.mobius a ↑u

theorem HyperbolicSpace.coe_boundaryMobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  ↑(HyperbolicSpace.boundaryMobius a ha
        u) =
    HyperbolicSpace.mobius a ↑u

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

def HyperbolicSpace.boundaryMobiusSymm.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E) (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) : ↑(Metric.sphere 0 1)

def HyperbolicSpace.boundaryMobiusSymm.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E)
  (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  ↑(Metric.sphere 0 1)

Implementation after :=

:=
  ⟨mobiusInvol a (-(u : E)), mem_sphere_zero_iff_norm.2 (by
    rw [norm_mobiusInvol]
    exact norm_mobius_eq_one (by rw [norm_neg]; exact mem_sphere_zero_iff_norm.1 u.2) ha)⟩

The inverse of `∂φ_a` on the ideal boundary, the restriction of `u ↦ σ_a(-u)`.

The negation is essential rather than cosmetic: `φ_a` is not an involution, its negative `σ_a` is
(`HyperbolicSpace.mobiusInvol_mobiusInvol`), so the inverse of `φ_a` is `y ↦ σ_a(-y)` — in one
dimension `y ↦ (y+a)/(1+ay)` against `φ_a(x) = (x-a)/(1-ax)`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.coe_boundaryMobiusSymm.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E} (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  ↑(HyperbolicSpace.boundaryMobiusSymm a ha u) =
    HyperbolicSpace.mobiusInvol a (-↑u)

theorem HyperbolicSpace.coe_boundaryMobiusSymm.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  ↑(HyperbolicSpace.boundaryMobiusSymm a
        ha u) =
    HyperbolicSpace.mobiusInvol a (-↑u)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.boundaryMobiusSymm_boundaryMobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E} (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryMobiusSymm a ha
      (HyperbolicSpace.boundaryMobius a ha u) =
    u

theorem HyperbolicSpace.boundaryMobiusSymm_boundaryMobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryMobiusSymm a ha
      (HyperbolicSpace.boundaryMobius a ha
        u) =
    u

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.boundaryMobius_boundaryMobiusSymm.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E} (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryMobius a ha
      (HyperbolicSpace.boundaryMobiusSymm a ha u) =
    u

theorem HyperbolicSpace.boundaryMobius_boundaryMobiusSymm.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryMobius a ha
      (HyperbolicSpace.boundaryMobiusSymm
        a ha u) =
    u

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

def HyperbolicSpace.boundaryMobiusEquiv.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E)
  (ha : ‖a‖ < 1) : ↑(Metric.sphere 0 1) ≃ ↑(Metric.sphere 0 1)

def HyperbolicSpace.boundaryMobiusEquiv.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E)
  (ha : ‖a‖ < 1) :
  ↑(Metric.sphere 0 1) ≃
    ↑(Metric.sphere 0 1)

Implementation after :=

:= boundaryMobius a ha
  invFun := boundaryMobiusSymm a ha
  left_inv := boundaryMobiusSymm_boundaryMobius ha
  right_inv := boundaryMobius_boundaryMobiusSymm ha

**The boundary map is a bijection of the sphere**, the inverse being the boundary restriction of
`u ↦ σ_a(-u)`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.coe_boundaryMobiusEquiv.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E)
  (ha : ‖a‖ < 1) :
  ⇑(HyperbolicSpace.boundaryMobiusEquiv a ha) =
    HyperbolicSpace.boundaryMobius a ha

theorem HyperbolicSpace.coe_boundaryMobiusEquiv.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E)
  (ha : ‖a‖ < 1) :
  ⇑(HyperbolicSpace.boundaryMobiusEquiv a
        ha) =
    HyperbolicSpace.boundaryMobius a ha

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.injective_boundaryMobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Function.Injective (HyperbolicSpace.boundaryMobius a ha)

theorem HyperbolicSpace.injective_boundaryMobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Function.Injective
    (HyperbolicSpace.boundaryMobius a ha)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.surjective_boundaryMobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Function.Surjective (HyperbolicSpace.boundaryMobius a ha)

theorem HyperbolicSpace.surjective_boundaryMobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Function.Surjective
    (HyperbolicSpace.boundaryMobius a ha)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.bijective_boundaryMobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Function.Bijective (HyperbolicSpace.boundaryMobius a ha)

theorem HyperbolicSpace.bijective_boundaryMobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Function.Bijective
    (HyperbolicSpace.boundaryMobius a ha)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.dist_boundaryMobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E} (ha : ‖a‖ < 1)
  (u v : ↑(Metric.sphere 0 1)) :
  dist (HyperbolicSpace.boundaryMobius a ha u)
      (HyperbolicSpace.boundaryMobius a ha v) =
    √(HyperbolicSpace.poissonKernel a ↑u *
          HyperbolicSpace.poissonKernel a ↑v) *
      dist u v

theorem HyperbolicSpace.dist_boundaryMobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1)
  (u v : ↑(Metric.sphere 0 1)) :
  dist
      (HyperbolicSpace.boundaryMobius a ha
        u)
      (HyperbolicSpace.boundaryMobius a ha
        v) =
    √(HyperbolicSpace.poissonKernel a ↑u *
          HyperbolicSpace.poissonKernel a
            ↑v) *
      dist u v

**Conformality of the boundary map in metric form**: `∂φ_a` multiplies the chordal distance of
the sphere by the geometric mean of the Poisson kernel at the two endpoints,

`dist (∂φ_a u) (∂φ_a v) = √(P(a,u) P(a,v)) · dist u v`.

This is the square root of `HyperbolicSpace.norm_sq_mobius_sub_of_mem_sphere`, the Poisson kernel
being positive at boundary points.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.continuous_boundaryMobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) : Continuous (HyperbolicSpace.boundaryMobius a ha)

theorem HyperbolicSpace.continuous_boundaryMobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Continuous
    (HyperbolicSpace.boundaryMobius a ha)

The boundary map is continuous: `φ_a` is differentiable at every point of the closed ball, in
particular at every point of the sphere, and the sphere carries the subspace topology.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.continuous_boundaryMobiusSymm.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) : Continuous (HyperbolicSpace.boundaryMobiusSymm a ha)

theorem HyperbolicSpace.continuous_boundaryMobiusSymm.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {a : E}
  (ha : ‖a‖ < 1) :
  Continuous
    (HyperbolicSpace.boundaryMobiusSymm a
      ha)

defdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

def HyperbolicSpace.boundaryMobiusHomeomorph.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] (a : E)
  (ha : ‖a‖ < 1) : ↑(Metric.sphere 0 1) ≃ₜ ↑(Metric.sphere 0 1)

def HyperbolicSpace.boundaryMobiusHomeomorph.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] (a : E)
  (ha : ‖a‖ < 1) :
  ↑(Metric.sphere 0 1) ≃ₜ
    ↑(Metric.sphere 0 1)

Implementation after :=

:= boundaryMobiusEquiv a ha
  continuous_toFun := continuous_boundaryMobius ha
  continuous_invFun := continuous_boundaryMobiusSymm ha

**The boundary map is a homeomorphism of the sphere.** Bijectivity is the involution `σ_a`,
continuity in both directions the differentiability of `φ_a` on the closed ball.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.boundaryDistance_coe_self.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryDistance (↑u) u = 0

theorem HyperbolicSpace.boundaryDistance_coe_self.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryDistance (↑u)
      u =
    0

The composite distance of the ball model takes the junk value `0` at a boundary point read
against itself, because `P(u,u) = 0/0 = 0` and `Real.log 0 = 0`.

This is what obstructs an instance of `SymmetricSpace.IsCompositeCocycle` for the Möbius action on
all of `E`, as the module docstring explains: the predicate quantifies over every point of the
ambient space, and there the transformation law would read `0 = 0 - ⟨a,u⟩`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/Hyperbolic/BoundaryMobius.lean

complete

theorem HyperbolicSpace.boundaryDistance_mobius.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1) (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryDistance (HyperbolicSpace.mobius a x)
      (HyperbolicSpace.boundaryMobius a ha u) =
    HyperbolicSpace.boundaryDistance x u -
      HyperbolicSpace.boundaryDistance a u

theorem HyperbolicSpace.boundaryDistance_mobius.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] {x a : E}
  (hx : ‖x‖ < 1) (ha : ‖a‖ < 1)
  (u : ↑(Metric.sphere 0 1)) :
  HyperbolicSpace.boundaryDistance
      (HyperbolicSpace.mobius a x)
      (HyperbolicSpace.boundaryMobius a ha
        u) =
    HyperbolicSpace.boundaryDistance x u -
      HyperbolicSpace.boundaryDistance a u

**The transformation law of the composite distance on the boundary sphere**,
`⟨φ_a x, ∂φ_a u⟩ = ⟨x,u⟩ - ⟨a,u⟩`: moving the point of the ball and the boundary normal by the same
Möbius transformation translates `boundaryDistance` by a quantity depending on the normal alone.

This is `HyperbolicSpace.compositeDistance_mobius` transported to the sphere-indexed form the
abstract Helgason--Fourier layer consumes. It is a lemma rather than an instance of
`SymmetricSpace.IsCompositeCocycle`: that predicate asks for the identity at every point of the
ambient space, where it is false, and the hypothesis `‖x‖ < 1` here is what makes it true. See the
module docstring.

One rewriting is the whole content. On the boundary Ahlfors' bracket is the squared Euclidean distance, [u,a]^2=\|u-a\|^2, so the conformal factor \lambda_a(x)=(1-\|a\|^2)/[x,a]^2 restricted to the boundary is the Poisson kernel P(a,u). Substituting that into the conformal distortion identity already proved for the ball gives the multiplier form, and no derivative along the sphere is taken — the statement needs none. The negation in the inverse is not decoration: \varphi_a is not an involution, only \sigma_a is.

The transformation law of the composite distance is recorded here as a plain lemma with the hypothesis \|x\|<1, and not as an instance of mathlib_symmetric_cocycle, because as an instance it would be false rather than merely unproved. The abstract predicate quantifies over every point of the ambient space, and the composite distance of the ball model carries a junk value outside the ball: at a boundary point read against itself the Poisson kernel is 0/0, so both sides of the law vanish and the law would force \langle a,u\rangle=0 at every boundary point. That already fails at u=a/\|a\|, where P(a,u)=(1+\|a\|)/(1-\|a\|). The honest instance is on the subtype, and saying so is worth more than producing one.

What is not here is the measure-theoretic step, \mathrm d(\partial\varphi_a u)=P(a,u)^{m-1}\mathrm du — that a conformal self-map of the sphere scales the surface measure by the (m-1)st power of its multiplier — which is what the quasi-invariance of the boundary measure needs on top of the above. The gap is in Mathlib and not in these identities: there is no change-of-variables formula for a Hausdorff measure on a submanifold, the boundary measure is built from the polar decomposition of Lebesgue measure and carries no transformation law under a map of the sphere, and the ambient change-of-variables theorem is useless because the sphere is null for the ambient measure.

Theorem5.8.10

uses 1used by 1✓L∃∀N

The Cholesky diagonal of a positive definite real matrix is positive. On the higher-rank symmetric space \mathbb P_m=GL(m,\mathbb R)/O(m) the Iwasawa decomposition is the Cholesky decomposition x=\nu\lambda\nu^\top with \nu unit lower triangular and \lambda positive diagonal. Mathlib already has the decomposition, as the LDL decomposition built by Gram--Schmidt; what the symmetric-space theory needs on top of it is that the diagonal factor is positive, so that its logarithm is defined.

Lean code for Theorem5.8.10●10 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

def Matrix.choleskyDiag.{u_1} {n : Type u_1} [Fintype n] [LinearOrder n]
  [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n ℝ}
  (hS : S.PosDef) : n → ℝ

def Matrix.choleskyDiag.{u_1} {n : Type u_1}
  [Fintype n] [LinearOrder n]
  [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : S.PosDef) :
  n → ℝ

Implementation after :=

:= LDL.diagEntries hS

The diagonal factor of the Cholesky decomposition of a positive definite real matrix, as a
function on the index type: the vector `λ` in `x = ν λ ν^⊤` with `ν` unit lower triangular.

This is Mathlib's `LDL.diagEntries` under a name that matches the use made of it on the symmetric
space `ℙ_m`, where the Cholesky decomposition is the Iwasawa decomposition.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.choleskyDiag_eq.{u_1} {n : Type u_1} [Fintype n] [LinearOrder n]
  [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n ℝ}
  (hS : S.PosDef) : Matrix.choleskyDiag hS = LDL.diagEntries hS

theorem Matrix.choleskyDiag_eq.{u_1}
  {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : S.PosDef) :
  Matrix.choleskyDiag hS =
    LDL.diagEntries hS

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.posDef_ldlDiag.{u_1} {n : Type u_1} [Fintype n] [LinearOrder n]
  [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n ℝ}
  (hS : S.PosDef) : (LDL.diag hS).PosDef

theorem Matrix.posDef_ldlDiag.{u_1} {n : Type u_1}
  [Fintype n] [LinearOrder n]
  [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : S.PosDef) :
  (LDL.diag hS).PosDef

The diagonal matrix of the Cholesky decomposition is positive definite: it is the conjugate of
`S` by the invertible matrix `LDL.lowerInv`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.choleskyDiag_pos.{u_1} {n : Type u_1} [Fintype n] [LinearOrder n]
  [WellFoundedLT n] [LocallyFiniteOrderBot n] {S : Matrix n n ℝ}
  (hS : S.PosDef) (i : n) : 0 < Matrix.choleskyDiag hS i

theorem Matrix.choleskyDiag_pos.{u_1}
  {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : S.PosDef)
  (i : n) : 0 < Matrix.choleskyDiag hS i

**The Cholesky diagonal is positive.** This is what makes `log ∘ choleskyDiag` — and with it
the composite distance `⟨x, kM⟩ = ½ log λ(k^⊤ x k)` of the symmetric space `ℙ_m` — well defined.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.cholesky_conj_diag.{u_1} {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : S.PosDef) :
  LDL.lower hS * Matrix.diagonal (Matrix.choleskyDiag hS) *
      (LDL.lower hS).transpose =
    S

theorem Matrix.cholesky_conj_diag.{u_1}
  {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : S.PosDef) :
  LDL.lower hS *
        Matrix.diagonal
          (Matrix.choleskyDiag hS) *
      (LDL.lower hS).transpose =
    S

**The Cholesky decomposition** of a positive definite real matrix, `S = L D L^⊤` with `L` unit
lower triangular and `D` the positive diagonal matrix of `Matrix.choleskyDiag`.

This is `LDL.lower_conj_diag` over `ℝ`, where the conjugate transpose is the transpose.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

def Matrix.choleskyDiagTotal.{u_1} {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n]
  (S : Matrix n n ℝ) : n → ℝ

def Matrix.choleskyDiagTotal.{u_1}
  {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  (S : Matrix n n ℝ) : n → ℝ

Implementation after :=

:=
  @dite _ S.PosDef (Classical.dec _) (fun h => choleskyDiag h) fun _ => 1

The Cholesky diagonal as a *total* function of the matrix, taking the junk value `1` off the
positive definite matrices.

The composite distance of `ℙ_m` is `⟨x, kM⟩ = ½ log λ(k^⊤ x k)`, and reading it as a plain function
of the matrix — rather than one carrying a positive-definiteness proof — is what lets it be used
inside the definition of the Helgason--Fourier transform. The junk value is `1` rather than `0` so
that the total function is positive everywhere and its logarithm is defined.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.choleskyDiagTotal_of_posDef.{u_1} {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : S.PosDef) :
  S.choleskyDiagTotal = Matrix.choleskyDiag hS

theorem Matrix.choleskyDiagTotal_of_posDef.{u_1}
  {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : S.PosDef) :
  S.choleskyDiagTotal =
    Matrix.choleskyDiag hS

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.choleskyDiagTotal_of_not_posDef.{u_1} {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : ¬S.PosDef) : S.choleskyDiagTotal = 1

theorem Matrix.choleskyDiagTotal_of_not_posDef.{u_1}
  {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  {S : Matrix n n ℝ} (hS : ¬S.PosDef) :
  S.choleskyDiagTotal = 1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.choleskyDiagTotal_pos.{u_1} {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n]
  (S : Matrix n n ℝ) (i : n) : 0 < S.choleskyDiagTotal i

theorem Matrix.choleskyDiagTotal_pos.{u_1}
  {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  (S : Matrix n n ℝ) (i : n) :
  0 < S.choleskyDiagTotal i

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.choleskyDiagTotal_ne_zero.{u_1} {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n] [LocallyFiniteOrderBot n]
  (S : Matrix n n ℝ) (i : n) : S.choleskyDiagTotal i ≠ 0

theorem Matrix.choleskyDiagTotal_ne_zero.{u_1}
  {n : Type u_1} [Fintype n]
  [LinearOrder n] [WellFoundedLT n]
  [LocallyFiniteOrderBot n]
  (S : Matrix n n ℝ) (i : n) :
  S.choleskyDiagTotal i ≠ 0

That is not a computation: the diagonal factor is the conjugate of the matrix by the invertible Gram--Schmidt factor, conjugation by an invertible matrix preserves positive definiteness, and a positive definite matrix has positive diagonal entries. Restating the decomposition over \mathbb R, where the conjugate transpose is the transpose, then gives the Iwasawa factorization in the form harmonic analysis on \mathbb P_m consumes. A total form, junk 1 off the positive definite cone, lets the diagonal be named inside a definition without carrying a positivity proof.

The article being formalized writes the composite distance of \mathbb P_m as \tfrac12\log\lambda in this diagonal. The model below does not: it uses the leading principal minors instead, for the reason recorded in the next statement. The Cholesky diagonal remains what the minors are computed from, and the two are the same data.

Theorem5.8.11

uses 1

Used by 3

Reverse dependency previews

Preview

Definition 3.1.14

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The leading principal minors of a positive definite matrix, and their invariance under the nilpotent and finite factors of the Iwasawa decomposition. For lower triangular L the corner of a conjugate is the conjugate of the corner, (LYL^\top)_j=L_jY_jL_j^\top; hence |(LYL^\top)_j|=|Y_j| when L has unit diagonal, and likewise when L is a \pm1 diagonal matrix. The dictionary to the Cholesky diagonal is |Y_j|=\prod_{i\le j}\lambda_i.

Lean code for Theorem5.8.11●23 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

def Matrix.cornerEmb {m : ℕ} (i : Fin m) : Fin (↑i + 1) → Fin m

def Matrix.cornerEmb {m : ℕ} (i : Fin m) :
  Fin (↑i + 1) → Fin m

Implementation after :=

:= Fin.castLE i.isLt

The inclusion of the upper-left `(i+1) × (i+1)` corner into the whole index set. Naming it keeps
`Fin.castLE i.isLt` — whose proof argument has type `↑i < m` where `Fin.castLE` wants `↑i + 1 ≤ m` —
from appearing in every statement, where the mismatch obstructs rewriting.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.coe_cornerEmb {m : ℕ} (i : Fin m) (a : Fin (↑i + 1)) :
  ↑(Matrix.cornerEmb i a) = ↑a

theorem Matrix.coe_cornerEmb {m : ℕ} (i : Fin m)
  (a : Fin (↑i + 1)) :
  ↑(Matrix.cornerEmb i a) = ↑a

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerEmb_injective {m : ℕ} (i : Fin m) :
  Function.Injective (Matrix.cornerEmb i)

theorem Matrix.cornerEmb_injective {m : ℕ}
  (i : Fin m) :
  Function.Injective (Matrix.cornerEmb i)

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

def Matrix.cornerDet {m : ℕ} (Y : Matrix (Fin m) (Fin m) ℝ) (i : Fin m) : ℝ

def Matrix.cornerDet {m : ℕ}
  (Y : Matrix (Fin m) (Fin m) ℝ)
  (i : Fin m) : ℝ

Implementation after :=

:=
  (Y.submatrix (cornerEmb i) (cornerEmb i)).det

The determinant of the upper-left `(i+1) × (i+1)` corner of `Y`, the `(i+1)`-st leading
principal minor. Terras' power function on `ℙ_m` is the product of real powers of these.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.posDef_submatrix_cornerEmb {m : ℕ} {Y : Matrix (Fin m) (Fin m) ℝ}
  (hY : Y.PosDef) (i : Fin m) :
  (Y.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i)).PosDef

theorem Matrix.posDef_submatrix_cornerEmb {m : ℕ}
  {Y : Matrix (Fin m) (Fin m) ℝ}
  (hY : Y.PosDef) (i : Fin m) :
  (Y.submatrix (Matrix.cornerEmb i)
      (Matrix.cornerEmb i)).PosDef

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDet_pos {m : ℕ} {Y : Matrix (Fin m) (Fin m) ℝ}
  (hY : Y.PosDef) (i : Fin m) : 0 < Y.cornerDet i

theorem Matrix.cornerDet_pos {m : ℕ}
  {Y : Matrix (Fin m) (Fin m) ℝ}
  (hY : Y.PosDef) (i : Fin m) :
  0 < Y.cornerDet i

The leading principal minors of a positive definite matrix are positive: each corner is itself
positive definite, and a positive definite matrix has positive determinant.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

def Matrix.cornerDetTotal {m : ℕ} (Y : Matrix (Fin m) (Fin m) ℝ)
  (i : Fin m) : ℝ

def Matrix.cornerDetTotal {m : ℕ}
  (Y : Matrix (Fin m) (Fin m) ℝ)
  (i : Fin m) : ℝ

Implementation after :=

:=
  @dite _ Y.PosDef (Classical.dec _) (fun _ => cornerDet Y i) fun _ => 1

The leading principal minors as a *total* function of the matrix, junk value `1` off the
positive definite matrices, so that the composite distance of `ℙ_m` can be a plain function.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDetTotal_of_posDef {m : ℕ} {Y : Matrix (Fin m) (Fin m) ℝ}
  (hY : Y.PosDef) : Y.cornerDetTotal = Y.cornerDet

theorem Matrix.cornerDetTotal_of_posDef {m : ℕ}
  {Y : Matrix (Fin m) (Fin m) ℝ}
  (hY : Y.PosDef) :
  Y.cornerDetTotal = Y.cornerDet

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDetTotal_of_not_posDef {m : ℕ}
  {Y : Matrix (Fin m) (Fin m) ℝ} (hY : ¬Y.PosDef) : Y.cornerDetTotal = 1

theorem Matrix.cornerDetTotal_of_not_posDef
  {m : ℕ} {Y : Matrix (Fin m) (Fin m) ℝ}
  (hY : ¬Y.PosDef) : Y.cornerDetTotal = 1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDetTotal_pos {m : ℕ} (Y : Matrix (Fin m) (Fin m) ℝ)
  (i : Fin m) : 0 < Y.cornerDetTotal i

theorem Matrix.cornerDetTotal_pos {m : ℕ}
  (Y : Matrix (Fin m) (Fin m) ℝ)
  (i : Fin m) : 0 < Y.cornerDetTotal i

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDetTotal_ne_zero {m : ℕ} (Y : Matrix (Fin m) (Fin m) ℝ)
  (i : Fin m) : Y.cornerDetTotal i ≠ 0

theorem Matrix.cornerDetTotal_ne_zero {m : ℕ}
  (Y : Matrix (Fin m) (Fin m) ℝ)
  (i : Fin m) : Y.cornerDetTotal i ≠ 0

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.submatrix_cornerEmb_mul_of_lowerTriangular {m : ℕ}
  {L Y : Matrix (Fin m) (Fin m) ℝ}
  (hL : ∀ (p q : Fin m), p < q → L p q = 0) (i : Fin m) :
  (L * Y).submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i) =
    L.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i) *
      Y.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i)

theorem Matrix.submatrix_cornerEmb_mul_of_lowerTriangular
  {m : ℕ} {L Y : Matrix (Fin m) (Fin m) ℝ}
  (hL :
    ∀ (p q : Fin m), p < q → L p q = 0)
  (i : Fin m) :
  (L * Y).submatrix (Matrix.cornerEmb i)
      (Matrix.cornerEmb i) =
    L.submatrix (Matrix.cornerEmb i)
        (Matrix.cornerEmb i) *
      Y.submatrix (Matrix.cornerEmb i)
        (Matrix.cornerEmb i)

**The one computation in this file.** For `L` lower triangular, the corner of `L * Y` is the
product of the corners.

The reason is that the first `i+1` rows of a lower triangular matrix are supported in the first
`i+1` columns, so in the sum defining `(L * Y) (e a) (e b)` every term whose summation index lies
beyond the corner has `L (e a) k = 0`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.submatrix_cornerEmb_mul_transpose_of_lowerTriangular {m : ℕ}
  {L Y : Matrix (Fin m) (Fin m) ℝ}
  (hL : ∀ (p q : Fin m), p < q → L p q = 0) (i : Fin m) :
  (Y * L.transpose).submatrix (Matrix.cornerEmb i)
      (Matrix.cornerEmb i) =
    Y.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i) *
      (L.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i)).transpose

theorem Matrix.submatrix_cornerEmb_mul_transpose_of_lowerTriangular
  {m : ℕ} {L Y : Matrix (Fin m) (Fin m) ℝ}
  (hL :
    ∀ (p q : Fin m), p < q → L p q = 0)
  (i : Fin m) :
  (Y * L.transpose).submatrix
      (Matrix.cornerEmb i)
      (Matrix.cornerEmb i) =
    Y.submatrix (Matrix.cornerEmb i)
        (Matrix.cornerEmb i) *
      (L.submatrix (Matrix.cornerEmb i)
          (Matrix.cornerEmb i)).transpose

The transposed companion: for `L` lower triangular, the corner of `Y * Lᵀ` is the product of the
corners.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.submatrix_cornerEmb_conj_of_lowerTriangular {m : ℕ}
  {L Y : Matrix (Fin m) (Fin m) ℝ}
  (hL : ∀ (p q : Fin m), p < q → L p q = 0) (i : Fin m) :
  (L * Y * L.transpose).submatrix (Matrix.cornerEmb i)
      (Matrix.cornerEmb i) =
    L.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i) *
        Y.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i) *
      (L.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i)).transpose

theorem Matrix.submatrix_cornerEmb_conj_of_lowerTriangular
  {m : ℕ} {L Y : Matrix (Fin m) (Fin m) ℝ}
  (hL :
    ∀ (p q : Fin m), p < q → L p q = 0)
  (i : Fin m) :
  (L * Y * L.transpose).submatrix
      (Matrix.cornerEmb i)
      (Matrix.cornerEmb i) =
    L.submatrix (Matrix.cornerEmb i)
          (Matrix.cornerEmb i) *
        Y.submatrix (Matrix.cornerEmb i)
          (Matrix.cornerEmb i) *
      (L.submatrix (Matrix.cornerEmb i)
          (Matrix.cornerEmb i)).transpose

The corner of a conjugate by a lower triangular matrix is the conjugate of the corner.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.blockTriangular_submatrix_cornerEmb {m : ℕ}
  {L : Matrix (Fin m) (Fin m) ℝ}
  (hL : ∀ (p q : Fin m), p < q → L p q = 0) (i : Fin m) :
  (L.submatrix (Matrix.cornerEmb i)
        (Matrix.cornerEmb i)).BlockTriangular
    ⇑OrderDual.toDual

theorem Matrix.blockTriangular_submatrix_cornerEmb
  {m : ℕ} {L : Matrix (Fin m) (Fin m) ℝ}
  (hL :
    ∀ (p q : Fin m), p < q → L p q = 0)
  (i : Fin m) :
  (L.submatrix (Matrix.cornerEmb i)
        (Matrix.cornerEmb
          i)).BlockTriangular
    ⇑OrderDual.toDual

The corner of a lower triangular matrix is lower triangular.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.det_submatrix_cornerEmb_of_lowerTriangular {m : ℕ}
  {L : Matrix (Fin m) (Fin m) ℝ}
  (hL : ∀ (p q : Fin m), p < q → L p q = 0) (i : Fin m) :
  (L.submatrix (Matrix.cornerEmb i) (Matrix.cornerEmb i)).det =
    ∏ c, L (Matrix.cornerEmb i c) (Matrix.cornerEmb i c)

theorem Matrix.det_submatrix_cornerEmb_of_lowerTriangular
  {m : ℕ} {L : Matrix (Fin m) (Fin m) ℝ}
  (hL :
    ∀ (p q : Fin m), p < q → L p q = 0)
  (i : Fin m) :
  (L.submatrix (Matrix.cornerEmb i)
        (Matrix.cornerEmb i)).det =
    ∏ c,
      L (Matrix.cornerEmb i c)
        (Matrix.cornerEmb i c)

The determinant of the corner of a lower triangular matrix is the product of the first diagonal
entries.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDet_conj_of_lowerTriangular_unit {m : ℕ}
  {L Y : Matrix (Fin m) (Fin m) ℝ}
  (hL : ∀ (p q : Fin m), p < q → L p q = 0)
  (hd : ∀ (p : Fin m), L p p = 1) (i : Fin m) :
  (L * Y * L.transpose).cornerDet i = Y.cornerDet i

theorem Matrix.cornerDet_conj_of_lowerTriangular_unit
  {m : ℕ} {L Y : Matrix (Fin m) (Fin m) ℝ}
  (hL :
    ∀ (p q : Fin m), p < q → L p q = 0)
  (hd : ∀ (p : Fin m), L p p = 1)
  (i : Fin m) :
  (L * Y * L.transpose).cornerDet i =
    Y.cornerDet i

**`N`-invariance of the leading principal minors.** Conjugating by a lower triangular matrix
with unit diagonal does not change them. Horospheres in `ℙ_m` are the orbits of the nilpotent factor
of the Iwasawa decomposition, so this is what makes the composite distance a function of the
horosphere.

In the Cholesky diagonal the same statement needs uniqueness of the LDL decomposition, which Mathlib
does not have; here it is the corner identity together with `det L_j = 1`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDet_conj_diagonal_sign {m : ℕ}
  {Y : Matrix (Fin m) (Fin m) ℝ} {d : Fin m → ℝ}
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) (i : Fin m) :
  (Matrix.diagonal d * Y * (Matrix.diagonal d).transpose).cornerDet i =
    Y.cornerDet i

theorem Matrix.cornerDet_conj_diagonal_sign
  {m : ℕ} {Y : Matrix (Fin m) (Fin m) ℝ}
  {d : Fin m → ℝ}
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1)
  (i : Fin m) :
  (Matrix.diagonal d * Y *
          (Matrix.diagonal
              d).transpose).cornerDet
      i =
    Y.cornerDet i

**`M`-invariance of the leading principal minors.** Conjugating by a diagonal matrix of signs
does not change them, because the corner determinant of such a matrix squares to `1`. The boundary
of `ℙ_m` is `K/M` with `M = D_{±1}`, so this is what makes the composite distance well defined on
the boundary.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.diagonal_sign_mul_self {m : ℕ} {d : Fin m → ℝ}
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  Matrix.diagonal d * Matrix.diagonal d = 1

theorem Matrix.diagonal_sign_mul_self {m : ℕ}
  {d : Fin m → ℝ}
  (hd :
    ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  Matrix.diagonal d * Matrix.diagonal d =
    1

A diagonal matrix of signs is its own inverse.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.isUnit_diagonal_sign {m : ℕ} {d : Fin m → ℝ}
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) : IsUnit (Matrix.diagonal d)

theorem Matrix.isUnit_diagonal_sign {m : ℕ}
  {d : Fin m → ℝ}
  (hd :
    ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  IsUnit (Matrix.diagonal d)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.posDef_conj_diagonal_sign_iff {m : ℕ}
  {Y : Matrix (Fin m) (Fin m) ℝ} {d : Fin m → ℝ}
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  (Matrix.diagonal d * Y * (Matrix.diagonal d).transpose).PosDef ↔
    Y.PosDef

theorem Matrix.posDef_conj_diagonal_sign_iff
  {m : ℕ} {Y : Matrix (Fin m) (Fin m) ℝ}
  {d : Fin m → ℝ}
  (hd :
    ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  (Matrix.diagonal d * Y *
        (Matrix.diagonal
            d).transpose).PosDef ↔
    Y.PosDef

Conjugating by a diagonal matrix of signs preserves positive definiteness in both directions,
the conjugation being an involution.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDetTotal_conj_diagonal_sign {m : ℕ}
  {Y : Matrix (Fin m) (Fin m) ℝ} {d : Fin m → ℝ}
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) (i : Fin m) :
  (Matrix.diagonal d * Y * (Matrix.diagonal d).transpose).cornerDetTotal
      i =
    Y.cornerDetTotal i

theorem Matrix.cornerDetTotal_conj_diagonal_sign
  {m : ℕ} {Y : Matrix (Fin m) (Fin m) ℝ}
  {d : Fin m → ℝ}
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1)
  (i : Fin m) :
  (Matrix.diagonal d * Y *
          (Matrix.diagonal
              d).transpose).cornerDetTotal
      i =
    Y.cornerDetTotal i

**`M`-invariance of the total form of the leading principal minors.** The junk value off the
positive definite cone is unaffected because the conjugation preserves the cone.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CornerDet.lean

complete

theorem Matrix.cornerDet_of_ldl {m : ℕ} {L Y : Matrix (Fin m) (Fin m) ℝ}
  {d : Fin m → ℝ} (hL : ∀ (p q : Fin m), p < q → L p q = 0)
  (hone : ∀ (p : Fin m), L p p = 1)
  (hY : Y = L * Matrix.diagonal d * L.transpose) (i : Fin m) :
  Y.cornerDet i = ∏ c, d (Matrix.cornerEmb i c)

theorem Matrix.cornerDet_of_ldl {m : ℕ}
  {L Y : Matrix (Fin m) (Fin m) ℝ}
  {d : Fin m → ℝ}
  (hL :
    ∀ (p q : Fin m), p < q → L p q = 0)
  (hone : ∀ (p : Fin m), L p p = 1)
  (hY :
    Y =
      L * Matrix.diagonal d * L.transpose)
  (i : Fin m) :
  Y.cornerDet i =
    ∏ c, d (Matrix.cornerEmb i c)

**The corner determinants are the partial products of the Cholesky diagonal.** If
`Y = L (diagonal d) Lᵀ` with `L` lower triangular with unit diagonal, then `|Y_j| = ∏_{i ≤ j} d_i`.

This is the translation between the two coordinate systems in which harmonic analysis on `ℙ_m` is
written: the article's composite distance is `½ log λ` in the Cholesky diagonal, Terras' power
function is built from `log|Y_j|`, and the two therefore differ by a triangular partial-sum
substitution.

Terras writes harmonic analysis on \mathbb P_m in terms of the power function p_s(Y)=\prod_j|Y_j|^{s_j} over the upper-left corners Y_j, so in her coordinates the composite distance is the vector j\mapsto\log|Y_j| and the horospherical character is p_s on the nose. That is the reason to prefer the minors to the Cholesky diagonal, and it is not only bookkeeping. The composite distance has to be N-invariant, horospheres being N-orbits, and M-invariant, the boundary being K/M rather than K. Stated in the Cholesky diagonal, both facts need uniqueness of the LDL decomposition, which Mathlib does not have and which is a real piece of work. Stated in the minors they are elementary, and the whole of their content is the displayed identity above — which holds because the first j rows of a lower triangular matrix are supported in the first j columns, and because \det L_j=1 for a unitriangular L and (\det L_j)^2=1 for a sign matrix.

So the choice of coordinates removes a dependency rather than merely relabelling one. It is also what lets Terras' constants be used verbatim, as the next statement records.

Theorem5.8.12

Statement uses 3

Statement dependency previews

Preview

Theorem 5.7.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Definition 3.1.14

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The manifold of positive definite matrices, and its Helgason--Fourier inversion formula as a proposition. \mathbb P_m=GL(m,\mathbb R)/O(m) is the higher-rank example of Section 5 — the rank is m, against one for hyperbolic space whatever its dimension. Supplying its geometry to the abstract layer makes the inversion formula on it a definite claim.

Lean code for Theorem5.8.12●23 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Cholesky.lean

complete

theorem Matrix.posDef_transpose_mul_mul.{u_1} {n : Type u_1} [Fintype n]
  {S : Matrix n n ℝ} [DecidableEq n] {g : Matrix n n ℝ} (hg : IsUnit g)
  (hS : S.PosDef) : (g.transpose * S * g).PosDef

theorem Matrix.posDef_transpose_mul_mul.{u_1}
  {n : Type u_1} [Fintype n]
  {S : Matrix n n ℝ} [DecidableEq n]
  {g : Matrix n n ℝ} (hg : IsUnit g)
  (hS : S.PosDef) :
  (g.transpose * S * g).PosDef

Conjugating a positive definite matrix by an invertible one preserves positive definiteness:
`g^⊤ S g` is positive definite. This is the action `g · x = g x g^⊤` of `GL(m,ℝ)` on the symmetric
space `ℙ_m` of positive definite matrices, read with `g^⊤` in place of `g`.

abbrevdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

abbrev SpdSpace.UpperIdx (m : ℕ) : Type

abbrev SpdSpace.UpperIdx (m : ℕ) : Type

Implementation after :=

:= {p : Fin m × Fin m // p.1 ≤ p.2}

The index type of the upper-triangular coordinates of a symmetric `m × m` matrix: the pairs
`(i,j)` with `i ≤ j`. Its cardinality is `m(m+1)/2`, the dimension of `ℙ_m`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

def SpdSpace.ofUpper {m : ℕ} (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m)) :
  Matrix (Fin m) (Fin m) ℝ

def SpdSpace.ofUpper {m : ℕ}
  (c :
    EuclideanSpace ℝ
      (SpdSpace.UpperIdx m)) :
  Matrix (Fin m) (Fin m) ℝ

Implementation after :=

:=
  Matrix.of fun i j => if h : i ≤ j then c ⟨(i, j), h⟩ else c ⟨(j, i), (not_le.1 h).le⟩

The symmetric matrix with prescribed upper-triangular coordinates. Together with
`SpdSpace.invariantMeasure` this is the chart in which the article's `∏_{i ≤ j} dx_{ij}` is
Lebesgue measure.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

theorem SpdSpace.ofUpper_apply_of_le {m : ℕ}
  (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m)) {i j : Fin m}
  (h : i ≤ j) : SpdSpace.ofUpper c i j = c.ofLp ⟨(i, j), h⟩

theorem SpdSpace.ofUpper_apply_of_le {m : ℕ}
  (c :
    EuclideanSpace ℝ
      (SpdSpace.UpperIdx m))
  {i j : Fin m} (h : i ≤ j) :
  SpdSpace.ofUpper c i j =
    c.ofLp ⟨(i, j), h⟩

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

theorem SpdSpace.ofUpper_apply_of_not_le {m : ℕ}
  (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m)) {i j : Fin m}
  (h : ¬i ≤ j) : SpdSpace.ofUpper c i j = c.ofLp ⟨(j, i), ⋯⟩

theorem SpdSpace.ofUpper_apply_of_not_le {m : ℕ}
  (c :
    EuclideanSpace ℝ
      (SpdSpace.UpperIdx m))
  {i j : Fin m} (h : ¬i ≤ j) :
  SpdSpace.ofUpper c i j =
    c.ofLp ⟨(j, i), ⋯⟩

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

theorem SpdSpace.ofUpper_isSymm {m : ℕ}
  (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m)) :
  (SpdSpace.ofUpper c).IsSymm

theorem SpdSpace.ofUpper_isSymm {m : ℕ}
  (c :
    EuclideanSpace ℝ
      (SpdSpace.UpperIdx m)) :
  (SpdSpace.ofUpper c).IsSymm

The chart lands in the symmetric matrices.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

theorem SpdSpace.measurable_ofUpper_apply {m : ℕ} (i j : Fin m) :
  Measurable fun c ↦ SpdSpace.ofUpper c i j

theorem SpdSpace.measurable_ofUpper_apply {m : ℕ}
  (i j : Fin m) :
  Measurable fun c ↦
    SpdSpace.ofUpper c i j

The chart is measurable entrywise. Stated this way because Mathlib puts no measurable space on
`Matrix`, deliberately not inheriting the `Pi` instance.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

def SpdSpace.chart (m : ℕ) : Set (EuclideanSpace ℝ (SpdSpace.UpperIdx m))

def SpdSpace.chart (m : ℕ) :
  Set
    (EuclideanSpace ℝ
      (SpdSpace.UpperIdx m))

Implementation after :=

:= {c | (ofUpper c).PosDef}

The positive definite cone read in the upper-triangular coordinates.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

def SpdSpace.invariantDensity (m : ℕ)
  (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m)) : ℝ

def SpdSpace.invariantDensity (m : ℕ)
  (c :
    EuclideanSpace ℝ
      (SpdSpace.UpperIdx m)) :
  ℝ

Implementation after :=

:=
  |(ofUpper c).det| ^ (-((m : ℝ) + 1) / 2)

The density `|det x|^{-(m+1)/2}` of the invariant measure of `ℙ_m` against Lebesgue measure in
the upper-triangular coordinates.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

def SpdSpace.invariantMeasure (m : ℕ) :
  MeasureTheory.Measure (EuclideanSpace ℝ (SpdSpace.UpperIdx m))

def SpdSpace.invariantMeasure (m : ℕ) :
  MeasureTheory.Measure
    (EuclideanSpace ℝ
      (SpdSpace.UpperIdx m))

Implementation after :=

:=
  (volume.restrict (chart m)).withDensity fun c => ENNReal.ofReal (invariantDensity m c)

**The `G`-invariant measure of `ℙ_m`**, `|det x|^{-(m+1)/2} ∏_{i ≤ j} dx_{ij}`, read on
the chart and concentrated on the positive definite cone.

No manifold theory and no normed-space structure on the symmetric matrices is needed: Lebesgue
measure of the chart *is* `∏_{i ≤ j} dx_{ij}`. The invariance under `g · x = g x g^⊤` is the
Jacobian statement of a later file; here the measure is only defined.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

def SpdSpace.act {m : ℕ} (g x : Matrix (Fin m) (Fin m) ℝ) :
  Matrix (Fin m) (Fin m) ℝ

def SpdSpace.act {m : ℕ}
  (g x : Matrix (Fin m) (Fin m) ℝ) :
  Matrix (Fin m) (Fin m) ℝ

Implementation after :=

:= g * x * gᵀ

The action of `GL(m,ℝ)` on `ℙ_m`, `g · x = g x g^⊤`, which identifies `ℙ_m` with
`GL(m,ℝ)/O(m)` through `gK ↦ g g^⊤`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

theorem SpdSpace.act_one {m : ℕ} (x : Matrix (Fin m) (Fin m) ℝ) :
  SpdSpace.act 1 x = x

theorem SpdSpace.act_one {m : ℕ}
  (x : Matrix (Fin m) (Fin m) ℝ) :
  SpdSpace.act 1 x = x

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

theorem SpdSpace.isSymm_act {m : ℕ} {g x : Matrix (Fin m) (Fin m) ℝ}
  (hx : x.IsSymm) : (SpdSpace.act g x).IsSymm

theorem SpdSpace.isSymm_act {m : ℕ}
  {g x : Matrix (Fin m) (Fin m) ℝ}
  (hx : x.IsSymm) :
  (SpdSpace.act g x).IsSymm

The action preserves the symmetric matrices.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/SpdModel.lean

complete

theorem SpdSpace.posDef_act {m : ℕ} {g x : Matrix (Fin m) (Fin m) ℝ}
  (hg : IsUnit g) (hx : x.PosDef) : (SpdSpace.act g x).PosDef

theorem SpdSpace.posDef_act {m : ℕ}
  {g x : Matrix (Fin m) (Fin m) ℝ}
  (hg : IsUnit g) (hx : x.PosDef) :
  (SpdSpace.act g x).PosDef

**The action preserves `ℙ_m`.** This is `Matrix.posDef_transpose_mul_mul` read for the action:
`g x g^⊤` is the conjugate of `x` by the invertible matrix `g^⊤`.

abbrevdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

abbrev SpdSpace.Boundary (m : ℕ) : Type

abbrev SpdSpace.Boundary (m : ℕ) : Type

Implementation after :=

:=
  unitary (EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m))

The orthogonal group of `ℝ^m`, in the coordinate-free form used throughout this development:
the unitary group of the algebra of continuous operators. It stands in for the boundary
`∂ℙ_m = K/M = O(m)/D_{±1}` of `ℙ_m`, the composite distance being `M`-invariant.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

def SpdSpace.boundaryMatrix {m : ℕ} (Q : SpdSpace.Boundary m) :
  Matrix (Fin m) (Fin m) ℝ

def SpdSpace.boundaryMatrix {m : ℕ}
  (Q : SpdSpace.Boundary m) :
  Matrix (Fin m) (Fin m) ℝ

Implementation after :=

:=
  (Matrix.toEuclideanCLM (n := Fin m) (𝕜 := ℝ)).symm
    (Q : EuclideanSpace ℝ (Fin m) →L[ℝ] EuclideanSpace ℝ (Fin m))

The matrix of an element of the orthogonal group, through the star-algebra equivalence between
matrices and operators on `EuclideanSpace`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

def SpdSpace.compositeDistance {m : ℕ}
  (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m))
  (Q : SpdSpace.Boundary m) : EuclideanSpace ℝ (Fin m)

def SpdSpace.compositeDistance {m : ℕ}
  (c :
    EuclideanSpace ℝ
      (SpdSpace.UpperIdx m))
  (Q : SpdSpace.Boundary m) :
  EuclideanSpace ℝ (Fin m)

Implementation after :=

:=
  WithLp.toLp 2 fun i =>
    Real.log (Matrix.cornerDetTotal ((boundaryMatrix Q)ᵀ * ofUpper c * boundaryMatrix Q) i)

**The vector-valued composite distance of `ℙ_m`**, `⟨x, kM⟩_j = log|(k^⊤ x k)_j|`, the vector of
logarithms of the leading principal minors.

The rank of `ℙ_m` is `m`, so this is genuinely vector valued — unlike the rank-one hyperbolic case,
where the composite distance is a scalar. Pairing it against `s` and exponentiating returns Terras'
power function `p_s(Y) = ∏_j|Y_j|^{s_j}` exactly, which is what lets her `ϱ`, `c`-function and
constant be used without a change of variables. The minors are read through
`Matrix.cornerDetTotal`, the total form, so that no positive-definiteness proof has to be carried
into the definition; on the chart the matrix is positive definite and the total form agrees with the
minors.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

theorem SpdSpace.compositeDistance_apply {m : ℕ}
  (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m)) (Q : SpdSpace.Boundary m)
  (i : Fin m) :
  (SpdSpace.compositeDistance c Q).ofLp i =
    Real.log
      (((SpdSpace.boundaryMatrix Q).transpose * SpdSpace.ofUpper c *
            SpdSpace.boundaryMatrix Q).cornerDetTotal
        i)

theorem SpdSpace.compositeDistance_apply {m : ℕ}
  (c :
    EuclideanSpace ℝ
      (SpdSpace.UpperIdx m))
  (Q : SpdSpace.Boundary m) (i : Fin m) :
  (SpdSpace.compositeDistance c Q).ofLp
      i =
    Real.log
      (((SpdSpace.boundaryMatrix
                  Q).transpose *
              SpdSpace.ofUpper c *
            SpdSpace.boundaryMatrix
              Q).cornerDetTotal
        i)

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

def SpdSpace.spdRho (m : ℕ) : EuclideanSpace ℝ (Fin m)

def SpdSpace.spdRho (m : ℕ) :
  EuclideanSpace ℝ (Fin m)

Implementation after :=

:=
  WithLp.toLp 2 fun i => if (i : ℕ) + 1 = m then ((m : ℝ) - 1) / 4 else -(1 / 2)

**Terras' shift** `ϱ = -ρ = (-½,…,-½,(m-1)/4)`, the constant of the Helgason--Fourier transform
of `ℙ_m` in the coordinates of the power function. The last coordinate is the exceptional one; the
contour of the inversion formula is `Re s = ϱ`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

def SpdSpace.helgasonFourier {m : ℕ} (rho : EuclideanSpace ℝ (Fin m))
  (f : EuclideanSpace ℝ (SpdSpace.UpperIdx m) → ℂ)
  (lam : EuclideanSpace ℝ (Fin m)) (Q : SpdSpace.Boundary m) : ℂ

def SpdSpace.helgasonFourier {m : ℕ}
  (rho : EuclideanSpace ℝ (Fin m))
  (f :
    EuclideanSpace ℝ
        (SpdSpace.UpperIdx m) →
      ℂ)
  (lam : EuclideanSpace ℝ (Fin m))
  (Q : SpdSpace.Boundary m) : ℂ

Implementation after :=

:=
  SymmetricSpace.helgasonFourier (invariantMeasure m) compositeDistance rho f lam Q

**The Helgason--Fourier transform on `ℙ_m`**,
`f̂(λ,u) = ∫ f(x) e^{(-iλ+ϱ)⟨x,u⟩} dμ(x)`,
with `μ` the invariant measure of `ℙ_m` and `ϱ` a parameter.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

theorem SpdSpace.helgasonFourier_eq {m : ℕ} (rho : EuclideanSpace ℝ (Fin m))
  (f : EuclideanSpace ℝ (SpdSpace.UpperIdx m) → ℂ)
  (lam : EuclideanSpace ℝ (Fin m)) (Q : SpdSpace.Boundary m) :
  SpdSpace.helgasonFourier rho f lam Q =
    ∫ (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m)),
      f c *
        SymmetricSpace.horosphericalCharacter rho (-lam)
          (SpdSpace.compositeDistance c Q) ∂SpdSpace.invariantMeasure m

theorem SpdSpace.helgasonFourier_eq {m : ℕ}
  (rho : EuclideanSpace ℝ (Fin m))
  (f :
    EuclideanSpace ℝ
        (SpdSpace.UpperIdx m) →
      ℂ)
  (lam : EuclideanSpace ℝ (Fin m))
  (Q : SpdSpace.Boundary m) :
  SpdSpace.helgasonFourier rho f lam Q =
    ∫ (c :
      EuclideanSpace ℝ
        (SpdSpace.UpperIdx m)),
      f c *
        SymmetricSpace.horosphericalCharacter
          rho (-lam)
          (SpdSpace.compositeDistance c
            Q) ∂SpdSpace.invariantMeasure
        m

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

def SpdSpace.HasInversion {m : ℕ} (W : ℝ) (c : EuclideanSpace ℝ (Fin m) → ℂ)
  (f : EuclideanSpace ℝ (SpdSpace.UpperIdx m) → ℂ) : Prop

def SpdSpace.HasInversion {m : ℕ} (W : ℝ)
  (c : EuclideanSpace ℝ (Fin m) → ℂ)
  (f :
    EuclideanSpace ℝ
        (SpdSpace.UpperIdx m) →
      ℂ) :
  Prop

Implementation after :=

:=
  SymmetricSpace.HasHelgasonInversion (invariantMeasure m)
    (volume : Measure (EuclideanSpace ℝ (Fin m)))
    (ContinuousLinearMap.orthogonalHaar (E := EuclideanSpace ℝ (Fin m)))
    compositeDistance (spdRho m) W c f

**The Helgason--Fourier inversion formula on `ℙ_m`**, as a proposition:

`f(x) = |W|^{-1} ∫_{𝔞*} ∫_{∂ℙ_m} f̂(λ,u) e^{(iλ+ϱ)⟨x,u⟩} |c(λ)|^{-2} du dλ`

with `dλ` Lebesgue measure on `𝔞* ≅ ℝ^m`, `du` the Haar probability measure of the orthogonal
group, and `dμ` the invariant measure `|det x|^{-(m+1)/2} ∏_{i ≤ j} dx_{ij}`.

Rank `m`, so the frequency is a vector and the Jacobian exponent of the reconstruction formula is
`m` — the opposite extreme from the hyperbolic case, where the rank is one whatever the dimension.
`ϱ` is Terras' `spdRho`; the order of the Weyl group and the `c`-function remain parameters, for
the reason given in the module docstring.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/HelgasonFourier.lean

complete

theorem SpdSpace.hasInversion_iff {m : ℕ} (W : ℝ)
  (c : EuclideanSpace ℝ (Fin m) → ℂ)
  (f : EuclideanSpace ℝ (SpdSpace.UpperIdx m) → ℂ) :
  SpdSpace.HasInversion W c f ↔
    ∀ (x : EuclideanSpace ℝ (SpdSpace.UpperIdx m)),
      ∫ (lam : EuclideanSpace ℝ (Fin m)),
          ∫ (Q : SpdSpace.Boundary m),
            SpdSpace.helgasonFourier (SpdSpace.spdRho m) f lam Q *
                ↑(SymmetricSpace.plancherelDensity W c lam) *
              SymmetricSpace.horosphericalCharacter (SpdSpace.spdRho m)
                lam
                (SpdSpace.compositeDistance x
                  Q) ∂ContinuousLinearMap.orthogonalHaar =
        f x

theorem SpdSpace.hasInversion_iff {m : ℕ} (W : ℝ)
  (c : EuclideanSpace ℝ (Fin m) → ℂ)
  (f :
    EuclideanSpace ℝ
        (SpdSpace.UpperIdx m) →
      ℂ) :
  SpdSpace.HasInversion W c f ↔
    ∀
      (x :
        EuclideanSpace ℝ
          (SpdSpace.UpperIdx m)),
      ∫ (lam : EuclideanSpace ℝ (Fin m)),
          ∫ (Q : SpdSpace.Boundary m),
            SpdSpace.helgasonFourier
                  (SpdSpace.spdRho m) f
                  lam Q *
                ↑(SymmetricSpace.plancherelDensity
                    W c lam) *
              SymmetricSpace.horosphericalCharacter
                (SpdSpace.spdRho m) lam
                (SpdSpace.compositeDistance
                  x
                  Q) ∂ContinuousLinearMap.orthogonalHaar =
        f x

Two arrangements make the article's measure |\det x|^{-(m+1)/2}\prod_{i\le j}\mathrm dx_{ij} into a measure, and both follow the precedent of the hyperbolic ball rather than building manifold theory. The carrier: that formula integrates over the m(m+1)/2 independent entries of a symmetric matrix, so restricting Lebesgue measure of the full matrix space to the symmetric matrices would give zero. So \mathbb P_m is modelled by the chart of upper-triangular coordinates, on which Lebesgue measure is \prod_{i\le j}\mathrm dx_{ij} — the same device as the singular-value chart of the d-plane development, and one that also sidesteps a gap, Mathlib giving Matrix neither an inner product nor a measurable space. The positivity: the measure is concentrated on the positive definite cone by restricting to the preimage of \mathbb P_m.

The composite distance is \langle x,kM\rangle_j=\log|(k^\top xk)_j|, the vector of logarithms of the leading principal minors, read through the total form of the minors so that no positivity proof has to be carried into the definition of the transform. The boundary K/M=O(m)/D_{\pm1} is represented by O(m) itself with its Haar probability measure, in the coordinate-free form used throughout this development; that is legitimate because the composite distance is M-invariant, and in these coordinates that invariance is the elementary Matrix.cornerDet_conj_diagonal_sign rather than a consequence of a uniqueness theorem Mathlib does not have.

\varrho is fixed, as in the hyperbolic case, to (-\tfrac12,\ldots,-\tfrac12,(m-1)/4). That is the article's value, and it is right: with the composite distance in the minors, e^{(i\lambda+\varrho)\langle x,u\rangle} is Terras' power function p_{\varrho+i\lambda}(x[k]) identically, so her contour \operatorname{Re}s=-\rho with \rho=(\tfrac12,\ldots,\tfrac12,(1-n)/4) — Harmonic Analysis on Symmetric Spaces, Thm 1.3.1(1) — transfers unchanged. An earlier version of this development recorded the article's \varrho as a probable mis-transcription of the half-sum of the positive restricted roots. It is not; it is Terras' contour, and the entry has been withdrawn.

What remains parameters are |W| and the c-function. Terras gives both explicitly, her c_n(s) as a product of beta quotients and her \omega_n as a product of gamma factors, and both now apply verbatim. The one thing not yet pinned is the conversion between her contour integral \mathrm ds over \operatorname{Re}s=-\rho, whose (2\pi i)^{-n} sits inside \omega_n, and Lebesgue measure \mathrm d\lambda on \mathfrak a^*, which is this development's convention. That is a computation, and the discipline here is that constants come out of proofs.

Theorem5.8.13

Statement uses 2

Statement dependency previews

Preview

Theorem 5.8.11

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

The composite distance of \mathbb P_m descends to the boundary K/M. Multiplying a boundary point on the right by a diagonal matrix of signs leaves the composite distance unchanged, and therefore leaves the Helgason--Fourier transform unchanged in its boundary argument. This is what makes an integral written over O(m) an integral over K/M=O(m)/D_{\pm1}: the integrand is constant on the fibres.

Lean code for Theorem5.8.13●6 declarations

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Boundary.lean

complete

theorem SpdSpace.boundaryMatrix_mul {m : ℕ} (Q R : SpdSpace.Boundary m) :
  SpdSpace.boundaryMatrix (Q * R) =
    SpdSpace.boundaryMatrix Q * SpdSpace.boundaryMatrix R

theorem SpdSpace.boundaryMatrix_mul {m : ℕ}
  (Q R : SpdSpace.Boundary m) :
  SpdSpace.boundaryMatrix (Q * R) =
    SpdSpace.boundaryMatrix Q *
      SpdSpace.boundaryMatrix R

The matrix of a product of boundary points is the product of their matrices: the map is the
inverse of a star-algebra equivalence.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Boundary.lean

complete

theorem SpdSpace.boundaryMatrix_one {m : ℕ} : SpdSpace.boundaryMatrix 1 = 1

theorem SpdSpace.boundaryMatrix_one {m : ℕ} :
  SpdSpace.boundaryMatrix 1 = 1

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Boundary.lean

complete

def SpdSpace.signUnitary {m : ℕ} (d : Fin m → ℝ)
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) : SpdSpace.Boundary m

def SpdSpace.signUnitary {m : ℕ}
  (d : Fin m → ℝ)
  (hd :
    ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  SpdSpace.Boundary m

Implementation after :=

:=
  ⟨Matrix.toEuclideanCLM (n := Fin m) (𝕜 := ℝ) (Matrix.diagonal d), by
    have hstar : star (Matrix.diagonal d) = Matrix.diagonal d := by
      rw [star_eq_conjTranspose, Matrix.diagonal_conjTranspose]
      simp
    refine Unitary.mem_iff.2 ⟨?_, ?_⟩ <;>
      rw [← map_star, hstar, ← map_mul, Matrix.diagonal_sign_mul_self hd, map_one]⟩

**An element of `M = D_{±1}` as a boundary point.** A diagonal matrix of signs is orthogonal, so
it is a unitary of the operator algebra; the hypothesis is carried in the definition because there
is no reason to name the non-orthogonal diagonal matrices.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Boundary.lean

complete

theorem SpdSpace.boundaryMatrix_signUnitary {m : ℕ} (d : Fin m → ℝ)
  (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  SpdSpace.boundaryMatrix (SpdSpace.signUnitary d hd) =
    Matrix.diagonal d

theorem SpdSpace.boundaryMatrix_signUnitary
  {m : ℕ} (d : Fin m → ℝ)
  (hd :
    ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  SpdSpace.boundaryMatrix
      (SpdSpace.signUnitary d hd) =
    Matrix.diagonal d

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Boundary.lean

complete

theorem SpdSpace.compositeDistance_mul_signUnitary {m : ℕ}
  (c : EuclideanSpace ℝ (SpdSpace.UpperIdx m)) (Q : SpdSpace.Boundary m)
  (d : Fin m → ℝ) (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  SpdSpace.compositeDistance c (Q * SpdSpace.signUnitary d hd) =
    SpdSpace.compositeDistance c Q

theorem SpdSpace.compositeDistance_mul_signUnitary
  {m : ℕ}
  (c :
    EuclideanSpace ℝ
      (SpdSpace.UpperIdx m))
  (Q : SpdSpace.Boundary m)
  (d : Fin m → ℝ)
  (hd :
    ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  SpdSpace.compositeDistance c
      (Q * SpdSpace.signUnitary d hd) =
    SpdSpace.compositeDistance c Q

**The composite distance of `ℙ_m` is `M`-invariant.** Multiplying a boundary point on the right
by a diagonal matrix of signs conjugates the argument of the leading principal minors by that
matrix, and `Matrix.cornerDetTotal_conj_diagonal_sign` says the minors do not see it.

This is what makes the Helgason--Fourier transform of `ℙ_m` an integral over the boundary
`K/M = O(m)/D_{±1}` even though it is written as an integral over `O(m)`: the integrand is constant
on the fibres of `O(m) → K/M`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/Boundary.lean

complete

theorem SpdSpace.helgasonFourier_mul_signUnitary {m : ℕ}
  (rho : EuclideanSpace ℝ (Fin m))
  (f : EuclideanSpace ℝ (SpdSpace.UpperIdx m) → ℂ)
  (lam : EuclideanSpace ℝ (Fin m)) (Q : SpdSpace.Boundary m)
  (d : Fin m → ℝ) (hd : ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  SpdSpace.helgasonFourier rho f lam (Q * SpdSpace.signUnitary d hd) =
    SpdSpace.helgasonFourier rho f lam Q

theorem SpdSpace.helgasonFourier_mul_signUnitary
  {m : ℕ} (rho : EuclideanSpace ℝ (Fin m))
  (f :
    EuclideanSpace ℝ
        (SpdSpace.UpperIdx m) →
      ℂ)
  (lam : EuclideanSpace ℝ (Fin m))
  (Q : SpdSpace.Boundary m)
  (d : Fin m → ℝ)
  (hd :
    ∀ (p : Fin m), d p = 1 ∨ d p = -1) :
  SpdSpace.helgasonFourier rho f lam
      (Q * SpdSpace.signUnitary d hd) =
    SpdSpace.helgasonFourier rho f lam Q

The Helgason--Fourier transform of `ℙ_m` is `M`-invariant in its boundary argument, and so is a
function on `K/M`. Immediate from the `M`-invariance of the composite distance, the transform
depending on the boundary point through nothing else.

The invariance of the minors under conjugation by a sign matrix is the earlier Matrix.cornerDet_conj_diagonal_sign, and it is not the same statement. That one is about conjugating a matrix; what the boundary integral needs is about multiplying a boundary point by an element of M. The gap between the two is exactly the star-algebra equivalence between matrices and operators on EuclideanSpace, which is how the orthogonal group is presented throughout this development — coordinate-free, as the unitary group of an operator algebra. Being an algebra map it carries the sign matrices into the unitary group and turns a product of boundary points into a product of matrices, which closes the gap and nothing more is needed.

Recording it as a theorem rather than as a remark in the definition of the transform is the point. The total form of the minors has to be handled too: its junk value off the positive definite cone would break the invariance if the conjugation could leave the cone, and it cannot, because conjugating by an invertible symmetric matrix preserves positive definiteness in both directions.

Theorem5.8.14

Statement uses 2

Statement dependency previews

Preview

Theorem 5.8.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Terras' explicit c-function and constant for \mathbb P_m, transcribed. c_m(s)=\prod_{1\le i\le j\le m-1}B(\tfrac12,s_i+\cdots+s_j+\tfrac12(j-i+1))/B(\tfrac12,\tfrac12(j-i+1)) and \omega_m=\prod_{j=1}^{m}\Gamma(j/2)/(j(2\pi i)\pi^{j/2}), of Harmonic Analysis on Symmetric Spaces, Thm 1.3.1(1), together with her contour s=\varrho+i\lambda and the Plancherel density built from them.

Lean code for Theorem5.8.14●31 declarations

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.beta (a b : ℂ) : ℂ

def SpdSpace.beta (a b : ℂ) : ℂ

Implementation after :=

:= Complex.Gamma a * Complex.Gamma b / Complex.Gamma (a + b)

**The Euler beta function** `B(a,b) = Γ(a)Γ(b)/Γ(a+b)`, in the form Terras uses it in
Thm 1.3.1(1).

Mathlib's `Complex.betaIntegral` is the Euler integral `∫_0^1 x^{a-1}(1-x)^{b-1} dx`, which needs
both arguments to have positive real part. Terras' `c`-function is evaluated on a contour where the
second argument has real part exactly `0`, so the integral is not available there and the gamma
quotient — its meromorphic continuation — is what is meant. The two agree where both are defined;
see `SpdSpace.betaIntegral_eq_beta`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.beta_eq (a b : ℂ) :
  SpdSpace.beta a b =
    Complex.Gamma a * Complex.Gamma b / Complex.Gamma (a + b)

theorem SpdSpace.beta_eq (a b : ℂ) :
  SpdSpace.beta a b =
    Complex.Gamma a * Complex.Gamma b /
      Complex.Gamma (a + b)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.beta_comm (a b : ℂ) : SpdSpace.beta a b = SpdSpace.beta b a

theorem SpdSpace.beta_comm (a b : ℂ) :
  SpdSpace.beta a b = SpdSpace.beta b a

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.betaIntegral_eq_beta {a b : ℂ} (ha : 0 < a.re)
  (hb : 0 < b.re) : a.betaIntegral b = SpdSpace.beta a b

theorem SpdSpace.betaIntegral_eq_beta {a b : ℂ}
  (ha : 0 < a.re) (hb : 0 < b.re) :
  a.betaIntegral b = SpdSpace.beta a b

Where the Euler integral converges it is the gamma quotient. This is Mathlib's
`Complex.betaIntegral_eq_Gamma_mul_div`, restated as the agreement of the two beta functions; it is
what justifies calling the quotient a beta function at all.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.partialSum {m : ℕ} (s : Fin m → ℂ) (i j : Fin m) : ℂ

def SpdSpace.partialSum {m : ℕ}
  (s : Fin m → ℂ) (i j : Fin m) : ℂ

Implementation after :=

:= ∑ k ∈ Finset.Icc i j, s k

The block sum `s_i + ⋯ + s_j` appearing in each factor of Terras' `c`-function. The block is
`Finset.Icc i j` in `Fin m`, so it is empty unless `i ≤ j`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.partialSum_apply {m : ℕ} (s : Fin m → ℂ) (i j : Fin m) :
  SpdSpace.partialSum s i j = ∑ k ∈ Finset.Icc i j, s k

theorem SpdSpace.partialSum_apply {m : ℕ}
  (s : Fin m → ℂ) (i j : Fin m) :
  SpdSpace.partialSum s i j =
    ∑ k ∈ Finset.Icc i j, s k

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.partialSum_self {m : ℕ} (s : Fin m → ℂ) (i : Fin m) :
  SpdSpace.partialSum s i i = s i

theorem SpdSpace.partialSum_self {m : ℕ}
  (s : Fin m → ℂ) (i : Fin m) :
  SpdSpace.partialSum s i i = s i

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.blockLength {m : ℕ} (i j : Fin m) : ℕ

def SpdSpace.blockLength {m : ℕ}
  (i j : Fin m) : ℕ

Implementation after :=

:= (Finset.Icc i j).card

The length `j-i+1` of the block, as the cardinality of `Finset.Icc i j`. Terras' factors carry
`½(j-i+1)`, which is half this number; writing it as a cardinality avoids truncated subtraction and
makes the empty block `i > j` — which never occurs in `SpdSpace.cIndex` — harmless.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.blockLength_eq {m : ℕ} (i j : Fin m) :
  SpdSpace.blockLength i j = ↑j + 1 - ↑i

theorem SpdSpace.blockLength_eq {m : ℕ}
  (i j : Fin m) :
  SpdSpace.blockLength i j = ↑j + 1 - ↑i

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.blockLength_self {m : ℕ} (i : Fin m) :
  SpdSpace.blockLength i i = 1

theorem SpdSpace.blockLength_self {m : ℕ}
  (i : Fin m) :
  SpdSpace.blockLength i i = 1

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.cIndex (m : ℕ) : Finset (Fin m × Fin m)

def SpdSpace.cIndex (m : ℕ) :
  Finset (Fin m × Fin m)

Implementation after :=

:=
  Finset.univ.filter fun p => p.1 ≤ p.2 ∧ (p.2 : ℕ) + 1 < m

The index set of Terras' product, `{(i,j) : 1 ≤ i ≤ j ≤ m-1}`, transcribed to the `0`-based
indexing of `Fin m`: the Lean pair `(i,j)` is Terras' `(i+1, j+1)`, so her `j ≤ n-1` is
`(j : ℕ) + 1 < m` here.

The two smallest cases, which are what an off-by-one would break:

* `m = 1`: the condition `(j : ℕ) + 1 < 1` is false, the set is empty, and `c_1(s) = 1` — Terras'
  `n = 1` case, where Thm 1.3.1(1) is Mellin inversion.
* `m = 2`: the only pair is `(0,0)`, Terras' `(i,j) = (1,1)`, giving the single factor
  `B(½, s_1 + ½)/B(½, ½)`.

Both are checked below as `example`s, together with `m = 3`, where the three pairs `(0,0)`, `(0,1)`,
`(1,1)` are Terras' `(1,1)`, `(1,2)`, `(2,2)`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.mem_cIndex {m : ℕ} {p : Fin m × Fin m} :
  p ∈ SpdSpace.cIndex m ↔ p.1 ≤ p.2 ∧ ↑p.2 + 1 < m

theorem SpdSpace.mem_cIndex {m : ℕ}
  {p : Fin m × Fin m} :
  p ∈ SpdSpace.cIndex m ↔
    p.1 ≤ p.2 ∧ ↑p.2 + 1 < m

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.cFactor {m : ℕ} (s : Fin m → ℂ) (i j : Fin m) : ℂ

def SpdSpace.cFactor {m : ℕ} (s : Fin m → ℂ)
  (i j : Fin m) : ℂ

Implementation after :=

:=
  beta (1 / 2) (partialSum s i j + (blockLength i j : ℂ) / 2) /
    beta (1 / 2) ((blockLength i j : ℂ) / 2)

One factor `B(½, s_i + ⋯ + s_j + ½(j-i+1)) / B(½, ½(j-i+1))` of Terras' `c`-function.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.cFactor_eq {m : ℕ} (s : Fin m → ℂ) (i j : Fin m) :
  SpdSpace.cFactor s i j =
    SpdSpace.beta (1 / 2)
        (SpdSpace.partialSum s i j + ↑(SpdSpace.blockLength i j) / 2) /
      SpdSpace.beta (1 / 2) (↑(SpdSpace.blockLength i j) / 2)

theorem SpdSpace.cFactor_eq {m : ℕ}
  (s : Fin m → ℂ) (i j : Fin m) :
  SpdSpace.cFactor s i j =
    SpdSpace.beta (1 / 2)
        (SpdSpace.partialSum s i j +
          ↑(SpdSpace.blockLength i j) /
            2) /
      SpdSpace.beta (1 / 2)
        (↑(SpdSpace.blockLength i j) / 2)

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.cFunction (m : ℕ) (s : Fin m → ℂ) : ℂ

def SpdSpace.cFunction (m : ℕ)
  (s : Fin m → ℂ) : ℂ

Implementation after :=

:= ∏ p ∈ cIndex m, cFactor s p.1 p.2

**Terras' `c`-function of `ℙ_m`** (*Harmonic Analysis on Symmetric Spaces — Higher Rank Spaces,
Positive Definite Matrix Space and Generalizations*, 2nd ed., Thm 1.3.1(1)),

`c_m(s) = ∏_{1 ≤ i ≤ j ≤ m-1} B(½, s_i + ⋯ + s_j + ½(j-i+1)) / B(½, ½(j-i+1))`.

This is a transcription, not a derivation: it is *not* proved here to be the Harish-Chandra integral
`SymmetricSpace.cFunctionIntegral` of the model, and nothing in this file asserts that it is. See
the module docstring.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.cFunction_eq (m : ℕ) (s : Fin m → ℂ) :
  SpdSpace.cFunction m s =
    ∏ p ∈ SpdSpace.cIndex m, SpdSpace.cFactor s p.1 p.2

theorem SpdSpace.cFunction_eq (m : ℕ)
  (s : Fin m → ℂ) :
  SpdSpace.cFunction m s =
    ∏ p ∈ SpdSpace.cIndex m,
      SpdSpace.cFactor s p.1 p.2

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.cFunction_one (s : Fin 1 → ℂ) : SpdSpace.cFunction 1 s = 1

theorem SpdSpace.cFunction_one (s : Fin 1 → ℂ) :
  SpdSpace.cFunction 1 s = 1

`c_1(s) = 1`: for `m = 1` the range `1 ≤ i ≤ j ≤ 0` is empty. Terras' `n = 1` case of
Thm 1.3.1(1) is ordinary Mellin inversion, which carries no `c`-function.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.cFunction_two (s : Fin 2 → ℂ) :
  SpdSpace.cFunction 2 s =
    SpdSpace.beta (1 / 2) (s 0 + 1 / 2) / SpdSpace.beta (1 / 2) (1 / 2)

theorem SpdSpace.cFunction_two (s : Fin 2 → ℂ) :
  SpdSpace.cFunction 2 s =
    SpdSpace.beta (1 / 2) (s 0 + 1 / 2) /
      SpdSpace.beta (1 / 2) (1 / 2)

`c_2(s)` has the single factor `B(½, s_1 + ½)/B(½, ½)`, Terras' pair `(i,j) = (1,1)`.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.weylConstant (m : ℕ) : ℂ

def SpdSpace.weylConstant (m : ℕ) : ℂ

Implementation after :=

:=
  ∏ j ∈ Finset.Icc 1 m, Complex.Gamma ((j : ℂ) / 2) /
    ((j : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) * ((Real.pi ^ ((j : ℝ) / 2) : ℝ) : ℂ))

**Terras' constant `ω_m`** of the inversion formula on `ℙ_m`
(*Harmonic Analysis on Symmetric Spaces — Higher Rank Spaces, Positive Definite Matrix Space and
Generalizations*, 2nd ed., Thm 1.3.1(1)),

`ω_m = ∏_{j=1}^{m} Γ(j/2) / ( j (2πi) π^{j/2} )`.

The `2πi` is kept literally rather than simplified into a real constant, because it belongs to
Terras' contour measure `ds` on `Re s = -ρ` and the conversion of that measure to Lebesgue measure
`dλ` on `𝔞* ≅ ℝ^m` has not been carried out in this development. Simplifying it would silently pick
a normalization; the discipline here is that constants come out of proofs.

At `m = 2` the product evaluates to `-1/(8π³)`: the `j = 1` factor is
`Γ(½)/(2πi√π) = (2πi)^{-1}` and the `j = 2` factor is `Γ(1)/(2·2πi·π) = (4π²i)^{-1}`, so the product
is `(2πi)^{-2}(2π)^{-1}`. That is an arithmetic check on the transcription, not a quotation.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.weylConstant_eq (m : ℕ) :
  SpdSpace.weylConstant m =
    ∏ j ∈ Finset.Icc 1 m,
      Complex.Gamma (↑j / 2) /
        (↑j * (2 * ↑Real.pi * Complex.I) * ↑(Real.pi ^ (↑j / 2)))

theorem SpdSpace.weylConstant_eq (m : ℕ) :
  SpdSpace.weylConstant m =
    ∏ j ∈ Finset.Icc 1 m,
      Complex.Gamma (↑j / 2) /
        (↑j * (2 * ↑Real.pi * Complex.I) *
          ↑(Real.pi ^ (↑j / 2)))

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.weylConstant_zero : SpdSpace.weylConstant 0 = 1

theorem SpdSpace.weylConstant_zero :
  SpdSpace.weylConstant 0 = 1

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.spdRho_apply (m : ℕ) (k : Fin m) :
  (SpdSpace.spdRho m).ofLp k =
    if ↑k + 1 = m then (↑m - 1) / 4 else -(1 / 2)

theorem SpdSpace.spdRho_apply (m : ℕ)
  (k : Fin m) :
  (SpdSpace.spdRho m).ofLp k =
    if ↑k + 1 = m then (↑m - 1) / 4
    else -(1 / 2)

The coordinates of `SpdSpace.spdRho`: `-½` except at the last index, where it is `(m-1)/4`.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.spdRho_eq_neg_half_of_mem_Icc {m : ℕ} {i j k : Fin m}
  (hj : ↑j + 1 < m) (hk : k ∈ Finset.Icc i j) :
  (SpdSpace.spdRho m).ofLp k = -(1 / 2)

theorem SpdSpace.spdRho_eq_neg_half_of_mem_Icc
  {m : ℕ} {i j k : Fin m}
  (hj : ↑j + 1 < m)
  (hk : k ∈ Finset.Icc i j) :
  (SpdSpace.spdRho m).ofLp k = -(1 / 2)

On a block of Terras' product the shift is constantly `-½`: the block ends at `j` with
`j + 1 < m`, so none of its indices is the exceptional last one.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.contourParam (m : ℕ) (lam : EuclideanSpace ℝ (Fin m))
  (j : Fin m) : ℂ

def SpdSpace.contourParam (m : ℕ)
  (lam : EuclideanSpace ℝ (Fin m))
  (j : Fin m) : ℂ

Implementation after :=

:=
  ((spdRho m j : ℝ) : ℂ) + Complex.I * ((lam j : ℝ) : ℂ)

**Terras' contour** `s = ϱ + iλ`, that is `Re s = -ρ` in her notation, parametrized by the real
frequency `λ ∈ 𝔞* ≅ ℝ^m` that the abstract Helgason--Fourier layer uses.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.contourParam_apply (m : ℕ) (lam : EuclideanSpace ℝ (Fin m))
  (j : Fin m) :
  SpdSpace.contourParam m lam j =
    ↑((SpdSpace.spdRho m).ofLp j) + Complex.I * ↑(lam.ofLp j)

theorem SpdSpace.contourParam_apply (m : ℕ)
  (lam : EuclideanSpace ℝ (Fin m))
  (j : Fin m) :
  SpdSpace.contourParam m lam j =
    ↑((SpdSpace.spdRho m).ofLp j) +
      Complex.I * ↑(lam.ofLp j)

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.re_partialSum_add_blockLength_eq_zero {m : ℕ} {i j : Fin m}
  (h : (i, j) ∈ SpdSpace.cIndex m) (lam : EuclideanSpace ℝ (Fin m)) :
  (SpdSpace.partialSum (SpdSpace.contourParam m lam) i j +
        ↑(SpdSpace.blockLength i j) / 2).re =
    0

theorem SpdSpace.re_partialSum_add_blockLength_eq_zero
  {m : ℕ} {i j : Fin m}
  (h : (i, j) ∈ SpdSpace.cIndex m)
  (lam : EuclideanSpace ℝ (Fin m)) :
  (SpdSpace.partialSum
          (SpdSpace.contourParam m lam) i
          j +
        ↑(SpdSpace.blockLength i j) /
          2).re =
    0

**On the contour the beta functions of `c_m` sit exactly on the boundary of convergence of the
Euler integral.** For every block `(i,j)` of Terras' product the second argument
`s_i + ⋯ + s_j + ½(j-i+1)` of the numerator has real part `0`, because the shift contributes
`-½(j-i+1)` and the frequency contributes nothing.

This is what forces `SpdSpace.beta` to be the gamma quotient: `Complex.betaIntegral` needs positive
real part in both arguments, so it is undefined at precisely the values `c_m` is evaluated at.

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.contourCFunction (m : ℕ) (lam : EuclideanSpace ℝ (Fin m)) : ℂ

def SpdSpace.contourCFunction (m : ℕ)
  (lam : EuclideanSpace ℝ (Fin m)) : ℂ

Implementation after :=

:=
  cFunction m (contourParam m lam)

**Terras' `c`-function on the contour** `Re s = ϱ`, that is `λ ↦ c_m(ϱ + iλ)` with
`ϱ = SpdSpace.spdRho m = (-½,…,-½,(m-1)/4)`.

This is the shape the abstract layer wants: `SymmetricSpace.plancherelDensity` and
`SpdSpace.HasInversion` take the `c`-function as a function of the real frequency `λ ∈ 𝔞* ≅ ℝ^m`,
while Terras' `c_m` is a function of the complex `s`, the two being related by her contour.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.contourCFunction_eq (m : ℕ) (lam : EuclideanSpace ℝ (Fin m)) :
  SpdSpace.contourCFunction m lam =
    SpdSpace.cFunction m fun j ↦
      ↑((SpdSpace.spdRho m).ofLp j) + Complex.I * ↑(lam.ofLp j)

theorem SpdSpace.contourCFunction_eq (m : ℕ)
  (lam : EuclideanSpace ℝ (Fin m)) :
  SpdSpace.contourCFunction m lam =
    SpdSpace.cFunction m fun j ↦
      ↑((SpdSpace.spdRho m).ofLp j) +
        Complex.I * ↑(lam.ofLp j)

defdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

def SpdSpace.plancherelDensity (m : ℕ) (W : ℝ)
  (lam : EuclideanSpace ℝ (Fin m)) : ℝ

def SpdSpace.plancherelDensity (m : ℕ) (W : ℝ)
  (lam : EuclideanSpace ℝ (Fin m)) : ℝ

Implementation after :=

:=
  SymmetricSpace.plancherelDensity W (contourCFunction m) lam

The Plancherel density of `ℙ_m` built from Terras' `c`-function,
`κ(λ) = (|W| ‖c_m(ϱ+iλ)‖²)^{-1}`.

The order `W` of the Weyl group stays a parameter, and no value is fixed for it here. Terras'
Thm 1.3.1(1) carries no factor `|W|^{-1}` at all: her whole constant is `ω_m`, in front of
`|c_m(s)|^{-2}` and against her contour measure `ds`. So the split between `|W|` and `c` in
`SymmetricSpace.plancherelDensity` is a convention that has to be matched to Terras' by the same
computation that converts `ds` to Lebesgue measure `dλ`, and that computation is not done here.
Feeding this density into `SpdSpace.HasInversion` gives the inversion formula of `ℙ_m` with Terras'
`c`-function in place of an abstract one; that is a proposition about `f`, not a theorem proved
here.

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.plancherelDensity_eq (m : ℕ) (W : ℝ)
  (lam : EuclideanSpace ℝ (Fin m)) :
  SpdSpace.plancherelDensity m W lam =
    (W * ‖SpdSpace.contourCFunction m lam‖ ^ 2)⁻¹

theorem SpdSpace.plancherelDensity_eq (m : ℕ)
  (W : ℝ)
  (lam : EuclideanSpace ℝ (Fin m)) :
  SpdSpace.plancherelDensity m W lam =
    (W *
        ‖SpdSpace.contourCFunction m
              lam‖ ^
          2)⁻¹

theoremdefined in LeanRidgelet/ToMathlib/LieGroup/PositiveDefinite/CFunction.lean

complete

theorem SpdSpace.plancherelDensity_pos {m : ℕ} {W : ℝ} (hW : 0 < W)
  {lam : EuclideanSpace ℝ (Fin m)}
  (hc : SpdSpace.contourCFunction m lam ≠ 0) :
  0 < SpdSpace.plancherelDensity m W lam

theorem SpdSpace.plancherelDensity_pos {m : ℕ}
  {W : ℝ} (hW : 0 < W)
  {lam : EuclideanSpace ℝ (Fin m)}
  (hc :
    SpdSpace.contourCFunction m lam ≠ 0) :
  0 < SpdSpace.plancherelDensity m W lam

The density is positive wherever Terras' `c`-function does not vanish, for a positive order of
the Weyl group.

This is a transcription and says so. Harish-Chandra's c-function is the integral \int_{\bar N}e^{-(i\lambda+\varrho)(H(\bar n))}\mathrm d\bar n, which is what the abstract layer takes as its definition, and the identity between that integral and Terras' product of beta quotients is the Gindikin--Karpelevich formula for \mathbb P_m — a theorem, not proved here, and no declaration claims it. Nor is the conversion from Terras' contour measure \mathrm ds to Lebesgue measure \mathrm d\lambda carried out, so \omega_m keeps its 2\pi i literally rather than absorbing it into a real constant, and the order of the Weyl group stays a parameter: Terras' theorem carries no |W|^{-1} at all, her whole constant being \omega_m, so the split between |W| and c is a convention that the same computation has to fix.

What is proved is the part where an error would be silent. The index range of the product is pinned by its two smallest cases — c_1(s)=1, the empty product, and c_2(s)=B(\tfrac12,s_1+\tfrac12)/B(\tfrac12,\tfrac12), the single factor — and by the observation that on the contour the second argument of every numerator has real part exactly zero: a block runs from i to j with j+1<m, so it misses the one exceptional coordinate of \varrho and the shift contributes precisely -\tfrac12(j-i+1). That is also why the beta function here is the gamma quotient rather than Mathlib's Euler integral, which converges only for arguments of positive real part and is therefore undefined at exactly the values c_m is evaluated at.