Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Bounded Measures

Abstract

The actual bounded-coefficient tensor square for the protected measure map. New proofs, Apache-2.0. This implements the uniformly bounded-family part of Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.3.

Theorem 1.1 (bounded Coefficient Map coordinate).

Lean statement: D5/S3/HomologicalAlgebra/Solid/BoundedMeasures.boundedCoefficientMap_coordinate

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/BoundedMeasures.boundedCoefficientMap_coordinate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. The actual bounded-coefficient tensor square for the protected measure map. New proofs, Apache-2.0. This implements the uniformly bounded-family part of Rodriguez Camargo, Notes on Solid Geometry, Lemma 3.3.3.

Theorem 1.2 (bounded Measure Tensor Square).

Lean statement: D5/S3/HomologicalAlgebra/Solid/BoundedMeasures.boundedMeasureTensorSquare

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/BoundedMeasures.boundedMeasureTensorSquare (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite difference of the tail projections lands in the actual protected P. This is the genuine bounded-family version of the tensor square in Lemma 3.3.3.

References