StationaryVolumeAlgebra.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Algebraic consequences of stationary volume comparison

Once the forward volume comparison gives domination of segment supports, the averaged homomorphism factors through canonical height by an invertible linear map. The reverse comparison for the coupled inverse then makes this map a support isometry. Neither conclusion is taken as a new hypothesis.

theorem OAI.PolycyclicRecognition.exists_linearEquiv_factor_of_kernel_le line 25
Source documentation
A surjective quotient and a map to the same finite-dimensional target with a smaller kernel differ by an invertible linear map.
```
theorem exists_linearEquiv_factor_of_kernel_le
    (π l : V →ₗ[ℝ] W) (hπ : Function.Surjective π) (hker : l.ker ≤ π.ker) :
    ∃ A : W ≃ₗ[ℝ] W, ∀ v, l v = A (π v) := by
…
```

theorem OAI.PolycyclicRecognition.exists_linearEquiv_factor_of_support_domination line 61

Source documentation

The actual support norm turns the forward volume inequality into the invertible height factor of the stationary slope.

theorem exists_linearEquiv_factor_of_support_domination
    {I B : Type*} [Fintype I] [Fintype B] [Nonempty B]
    (D : SupportDatum W I B) (π l : V →ₗ[ℝ] W) (hπ : Function.Surjective π)
    (hvol : ∀ v, D.segmentSupport (π v) ≤ D.segmentSupport (l v)) :
    ∃ A : W ≃ₗ[ℝ] W, ∀ v, l v = A (π v) := by
…

Mentions: OAI.PolycyclicRecognition.SupportDatum

theorem OAI.PolycyclicRecognition.support_preserved_of_forward_inverse line 76

Source documentation

Forward comparison and comparison for the same coupled inverse force equality of the support exponents.

theorem support_preserved_of_forward_inverse
    {I B : Type*} [Fintype I] [Fintype B] [Nonempty B]
    (D : SupportDatum W I B) (A : W ≃ₗ[ℝ] W)
    (hforward : ∀ w, D.segmentSupport w ≤ D.segmentSupport (A w))
    (hinverse : ∀ w, D.segmentSupport w ≤ D.segmentSupport (A.symm w)) :
    ∀ w, D.segmentSupport (A w) = D.segmentSupport w := by
…

Mentions: OAI.PolycyclicRecognition.SupportDatum