AmenableCorrection.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Correcting bounded height defects with an invariant mean

This is the averaging step in Proposition recognition-from-height of the manuscript Quasi-isometric recognition of virtually polycyclic groups. The mean is on the actual space of all bounded real functions. Neither the height function itself nor its corrected homomorphism has to be bounded.

def OAI.PolycyclicRecognition.boundedIncrement line 30
Source documentation
The increment of a function of uniformly bounded additive defect is bounded.
```
def boundedIncrement (s : G → ℝ) (D : ℝ)
    (hD : ∀ h k, |s (h * k) - s h - s k| ≤ D) (h : G) : BoundedReal G :=
…
```
theorem OAI.PolycyclicRecognition.boundedIncrement_apply line 41

theorem OAI.PolycyclicRecognition.boundedIncrement_mul line 46

Source documentation

The cocycle identity holds for increments before applying the mean.

theorem boundedIncrement_mul (s : G → ℝ) (D : ℝ)
    (hD : ∀ h k, |s (h * k) - s h - s k| ≤ D) (h k : G) :
    boundedIncrement s D hD (h * k) =
      leftPull k (boundedIncrement s D hD h) + boundedIncrement s D hD k := by
…

Mentions: OAI.PolycyclicRecognition.boundedIncrement

def OAI.PolycyclicRecognition.meanCorrection line 58

Source documentation

Averaging the bounded increments gives an additive homomorphism.

def meanCorrection (M : InvariantMean G) (s : G → ℝ) (D : ℝ)
    (hD : ∀ h k, |s (h * k) - s h - s k| ≤ D) (h : G) : ℝ :=
…

theorem OAI.PolycyclicRecognition.meanCorrection_mul line 62
theorem OAI.PolycyclicRecognition.meanCorrection_one line 72
theorem OAI.PolycyclicRecognition.meanCorrection_dist_le line 80
Source documentation
Positivity of the mean preserves the uniform defect bound exactly.
```
theorem meanCorrection_dist_le (M : InvariantMean G) (s : G → ℝ) (D : ℝ)
    (hD : ∀ h k, |s (h * k) - s h - s k| ≤ D) (h : G) :
    |meanCorrection M s D hD h - s h| ≤ D := by
…
```
Mentions: OAI.PolycyclicRecognition.meanCorrection

theorem OAI.PolycyclicRecognition.exists_meanCorrection line 100

Source documentation

Scalar bounded-defect correction; the original function need not be bounded.

theorem exists_meanCorrection (M : InvariantMean G) (s : G → ℝ) (D : ℝ)
    (hD : ∀ h k, |s (h * k) - s h - s k| ≤ D) :
    ∃ τ : G → ℝ, τ 1 = 0 ∧ (∀ h k, τ (h * k) = τ h + τ k) ∧
      ∀ h, |τ h - s h| ≤ D :=
…

theorem OAI.PolycyclicRecognition.coordinate_defect_le line 108

Source documentation

Coordinate defects are bounded by the defect in the supremum norm.

theorem coordinate_defect_le {ι : Type v} [Fintype ι] (s : G → ι → ℝ) (D : ℝ)
    (hD : ∀ h k, ‖s (h * k) - s h - s k‖ ≤ D) (i : ι) (h k : G) :
    |s (h * k) i - s h i - s k i| ≤ D := by
…

def OAI.PolycyclicRecognition.vectorMeanCorrection line 115

Source documentation

The finite-dimensional correction obtained by applying the mean to each coordinate.

def vectorMeanCorrection {ι : Type v} [Fintype ι]
    (M : InvariantMean G) (s : G → ι → ℝ) (D : ℝ)
    (hD : ∀ h k, ‖s (h * k) - s h - s k‖ ≤ D) (h : G) (i : ι) : ℝ :=
…

theorem OAI.PolycyclicRecognition.vectorMeanCorrection_one line 121
theorem OAI.PolycyclicRecognition.vectorMeanCorrection_mul line 128

theorem OAI.PolycyclicRecognition.vectorMeanCorrection_dist_le line 137

Source documentation

The correction remains within the original defect bound in the supremum norm.

theorem vectorMeanCorrection_dist_le {ι : Type v} [Fintype ι]
    (M : InvariantMean G) (s : G → ι → ℝ) (D : ℝ)
    (hD : ∀ h k, ‖s (h * k) - s h - s k‖ ≤ D) (h : G) :
    ‖vectorMeanCorrection M s D hD h - s h‖ ≤ D := by
…

Mentions: OAI.PolycyclicRecognition.vectorMeanCorrection

def OAI.PolycyclicRecognition.correctedHom line 148

Source documentation

Finite-dimensional bounded-defect correction, packaged as a genuine homomorphism.

def correctedHom {ι : Type v} [Fintype ι]
    (M : InvariantMean G) (s : G → ι → ℝ) (D : ℝ)
    (hD : ∀ h k, ‖s (h * k) - s h - s k‖ ≤ D) :
    G →* Multiplicative (ι → ℝ) where
…

theorem OAI.PolycyclicRecognition.exists_correctedHom line 158

Source documentation

A height map of uniformly bounded additive defect on an amenable group is uniformly close to a homomorphism to a finite-dimensional real vector space.

theorem exists_correctedHom {ι : Type v} [Fintype ι]
    (M : InvariantMean G) (s : G → ι → ℝ) (D : ℝ)
    (hD : ∀ h k, ‖s (h * k) - s h - s k‖ ≤ D) :
    ∃ τ : G →* Multiplicative (ι → ℝ), ∀ h, ‖(τ h).toAdd - s h‖ ≤ D :=
…

theorem OAI.PolycyclicRecognition.exists_correctedHom_of_equiv line 166

Source documentation

Transfer the finite-coordinate correction through a continuous linear equivalence. The resulting bound records the change of norm explicitly.

theorem exists_correctedHom_of_equiv {W : Type*} [NormedAddCommGroup W]
    [NormedSpace ℝ W] {ι : Type v} [Fintype ι]
    (e : W ≃L[ℝ] (ι → ℝ)) (M : InvariantMean G) (s : G → W) (D : ℝ)
    (hD : ∀ h k, ‖s (h * k) - s h - s k‖ ≤ D) :
    ∃ τ : G →* Multiplicative W,
      ∀ h, ‖(τ h).toAdd - s h‖ ≤
        ‖e.symm.toContinuousLinearMap‖ * (‖e.toContinuousLinearMap‖ * D) := by
…

theorem OAI.PolycyclicRecognition.exists_finiteDimensional_correctedHom line 204

Source documentation

On any finite-dimensional real normed space, a height map of uniformly bounded additive defect is uniformly close to a homomorphism.

theorem exists_finiteDimensional_correctedHom {W : Type*} [NormedAddCommGroup W]
    [NormedSpace ℝ W] [FiniteDimensional ℝ W]
    (M : InvariantMean G) (s : G → W) (D : ℝ)
    (hD : ∀ h k, ‖s (h * k) - s h - s k‖ ≤ D) :
    ∃ (τ : G →* Multiplicative W) (B : ℝ), 0 ≤ B ∧
      ∀ h, ‖(τ h).toAdd - s h‖ ≤ B := by
…