GeometricAction.lean`

33 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.CATZero.dist_mid_mid_le line 31
theorem OAI.HyperbolicObstruction.CATZero.dist_mid_mid_sq_le line 41
theorem OAI.HyperbolicObstruction.CATZero.isometry_mid line 49

theorem OAI.HyperbolicObstruction.CATZero.orbit_minimum_of_energy_minimum line 56

Source documentation

Crossed-midpoint convexity turns a minimum of a symmetric displacement energy into a minimum of the squared distances to the fixed orbit tuple.

theorem orbit_minimum_of_energy_minimum {ι : Type*} [Fintype ι]
    (h : CATZero X) (e : ι → X ≃ᵢ X) (σ : ι ≃ ι)
    (hinv : ∀ i, e (σ i) = (e i).symm) (o : X)
    (hmin : ∀ y : X, (∑ i, dist o (e i o) ^ 2) ≤ ∑ i, dist y (e i y) ^ 2) :
    ∀ y : X, (∑ i, dist o (e i o) ^ 2) ≤ ∑ i, dist y (e i o) ^ 2 := by
…

Mentions: OAI.HyperbolicObstruction.CATZero

theorem OAI.HyperbolicObstruction.energy_tangent_barycenter line 80

Source documentation

The zero-barycenter conclusion, for any attained symmetric isometric displacement-energy minimum.

theorem energy_tangent_barycenter {X : Type*} [MetricSpace X] {ι : Type*} [Fintype ι]
    (h : CATZero X) (e : ι → X ≃ᵢ X) (σ : ι ≃ ι)
    (hinv : ∀ i, e (σ i) = (e i).symm) (o : X)
    (hmin : ∀ y : X, (∑ i, dist o (e i o) ^ 2) ≤ ∑ i, dist y (e i y) ^ 2)
    (v : TangentCone h o) :
    (∑ i, (TangentCone.coneData h o).pairing v (TangentCone.log h o (e i o))) ≤ 0 :=
…

Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.TangentCone, OAI.HyperbolicObstruction.TangentCone.coneData, OAI.HyperbolicObstruction.TangentCone.log

theorem OAI.HyperbolicObstruction.GeometricAction.displacement_conjugate line 98
Source documentation
Displacement is invariant under simultaneous point/generator conjugation.
```
theorem displacement_conjugate (A : GeometricAction G X) (g s : G) (x : X) :
    dist x (A.act (g⁻¹ * s * g) x) = dist (A.act g x) (A.act s (A.act g x)) := by
…
```
Mentions: OAI.HyperbolicObstruction.GeometricAction
theorem OAI.HyperbolicObstruction.GeometricAction.energy_minimum line 107
Source documentation
Properness and cocompactness give an attained displacement-energy minimum. No CAT(0) assumption is needed for this compactness step.
```
theorem energy_minimum [Nonempty X] [ProperSpace X] {ι : Type*} [Fintype ι]
    (A : GeometricAction G X) (S : ι → G) :
    ∃ o : X, ∀ y : X, (∑ i, dist o (A.act (S i) o) ^ 2) ≤
      ∑ i, dist y (A.act (S i) y) ^ 2 := by
…
```
Mentions: OAI.HyperbolicObstruction.GeometricAction
theorem OAI.HyperbolicObstruction.GeometricAction.energy_pos line 191
Source documentation
An infinite group with a proper action cannot have zero displacement energy on a finite generating tuple.
```
theorem energy_pos [Infinite G] {ι : Type*} [Fintype ι]
    (A : GeometricAction G X) (S : ι → G)
    (hgen : Subgroup.closure (Set.range S) = ⊤) (o : X) :
    0 < ∑ i, dist o (A.act (S i) o) ^ 2 := by
…
```
Mentions: OAI.HyperbolicObstruction.GeometricAction

theorem OAI.HyperbolicObstruction.expect_snoc line 230

Source documentation

Splitting off the last coordinate of a uniform independent tuple.

theorem expect_snoc {ι : Type*} [Fintype ι] (n : ℕ) (f : (Fin (n + 1) → ι) → ℝ) :
    (𝔼 a, f a) = 𝔼 a : Fin n → ι, 𝔼 i : ι, f (Fin.snoc a i) := by
…

theorem OAI.HyperbolicObstruction.ConeData.normSq_segment_pairing line 244
def OAI.HyperbolicObstruction.ConeData.inductiveMean line 253
Source documentation
The ordered inductive mean, with the harmless value vertex for an empty list. For a list of length j+1, append its last point with weight 1/(j+1).
```
def inductiveMean (T : ConeData X) (h : CATZero X) : (n : ℕ) → (Fin n → X) → X
  | 0, _ => T.vertex
  | n + 1, v => CATZero.segment h
      (inductiveMean T h n (fun i => v i.castSucc)) (v (Fin.last n)) (1 / (n + 1 : ℝ))
```
Mentions: OAI.HyperbolicObstruction.ConeData, OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment
theorem OAI.HyperbolicObstruction.ConeData.reciprocal_mem line 258
theorem OAI.HyperbolicObstruction.ConeData.pairing_inductiveMean line 267
Source documentation
Deterministic concavity for the ordered mean; no associative cone addition is used.
```
theorem pairing_inductiveMean (h : CATZero X) (w : X) (n : ℕ) (v : Fin n → X) :
    (∑ i, T.pairing w (v i)) ≤ (n : ℝ) * T.pairing w (T.inductiveMean h n v) := by
…
```
Mentions: OAI.HyperbolicObstruction.CATZero

theorem OAI.HyperbolicObstruction.ConeData.expected_step line 291

Source documentation

One genuinely independent averaging step, using the zero-barycenter inequality rather than any linear ambient vector space.

theorem expected_step {ι : Type*} [Fintype ι] [Nonempty ι]
    (h : CATZero X) (v : ι → X)
    (hbar : ∀ u, (𝔼 i, T.pairing u (v i)) ≤ 0)
    (hen : (𝔼 i, T.normSq (v i)) = 1) (u : X) {t : ℝ}
    (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    (𝔼 i, T.normSq (CATZero.segment h u (v i) t)) ≤ (1 - t) ^ 2 * T.normSq u + t ^ 2 := by
…

Mentions: OAI.HyperbolicObstruction.CATZero, OAI.HyperbolicObstruction.CATZero.segment

theorem OAI.HyperbolicObstruction.ConeData.expected_inductiveMean_step line 303

theorem OAI.HyperbolicObstruction.ConeData.expected_inductiveMean line 323

Source documentation

The exact 1/t mean-square decay for t independent uniform samples.

theorem expected_inductiveMean {ι : Type*} [Fintype ι] [Nonempty ι]
    (h : CATZero X) (v : ι → X)
    (hbar : ∀ u, (𝔼 i, T.pairing u (v i)) ≤ 0)
    (hen : (𝔼 i, T.normSq (v i)) = 1) (n : ℕ) :
    (𝔼 a : Fin (n + 1) → ι, T.normSq (T.inductiveMean h (n + 1) (v ∘ a))) ≤
      1 / (n + 1 : ℝ) := by
…

Mentions: OAI.HyperbolicObstruction.CATZero

structure OAI.HyperbolicObstruction.FiniteLaw line 356
Source documentation
A finite probability law, retaining real weights for the conditional couplings. Uniform laws are exactly the table match distributions.
```
structure FiniteLaw (α : Type*) [Fintype α] where
…
```
def OAI.HyperbolicObstruction.FiniteLaw.expect line 364
def OAI.HyperbolicObstruction.FiniteLaw.uniform line 366
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_uniform line 374
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_const line 380
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_add line 383
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_sub line 387
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_mul line 391
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_sum line 398
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_mono line 403
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_nonneg line 407
def OAI.HyperbolicObstruction.FiniteLaw.map line 410
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_map line 420
def OAI.HyperbolicObstruction.FiniteLaw.totalVariation line 430
theorem OAI.HyperbolicObstruction.FiniteLaw.totalVariation_nonneg line 432
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_sub_bound line 436
Source documentation
Exact finite total-variation comparison, with the constant 2B.
```
theorem expect_sub_bound (μ ν : FiniteLaw α) (f : α → ℝ) {B : ℝ}
    (hB : ∀ a, |f a| ≤ B) :
    |μ.expect f - ν.expect f| ≤ 2 * B * μ.totalVariation ν := by
…
```
Mentions: OAI.HyperbolicObstruction.FiniteLaw
theorem OAI.HyperbolicObstruction.FiniteLaw.expect_le_sqrt line 453
Source documentation
Finite-probability Cauchy--Schwarz in the scalar form needed for cone norms under arbitrary conditional couplings.
```
theorem expect_le_sqrt (μ : FiniteLaw α) (f : α → ℝ) :
    μ.expect f ≤ Real.sqrt (μ.expect (fun a => f a ^ 2)) := by
…
```
Mentions: OAI.HyperbolicObstruction.FiniteLaw