OAI/Analysis/RieszRectifiability/Limits/FiniteAffineVectorLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vector-valued affine strong limits

Coordinatewise affine limits assemble into one ambient affine map. On bounded projection regions, coordinate square integrability and convergence combine through the Euclidean norm identity to give vector-valued strong convergence.

  1. theorem OAI.RieszRectifiability.exists_vector_affine_strong_limit_of_coordinates line 24