Commit 2025-02-07 10:03 c3492e17

View on Github →

chore(Analysis/InnerProductSpace): split off continuity, convexity of inner product (#21516) Looking at the longest pole I saw that InnerProductSpace.Basic imports quite a lot that isn't used in downstream files such as Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances. By splitting off two little files I managed to clean up the import hierarchy a bit. This PR adds two new files:

  • InnerProductSpace/Continuous.lean: shows that the inner product is continuous.
  • InnerProductSpace/Convex.lean: shows that inner product spaces are uniformly convex spaces.

Estimated changes

deleted theorem Continuous.inner
deleted theorem ContinuousAt.inner
deleted theorem ContinuousOn.inner
deleted theorem ContinuousWithinAt.inner
deleted theorem Filter.Tendsto.inner
deleted theorem continuous_inner
added theorem Continuous.inner
added theorem ContinuousAt.inner
added theorem ContinuousOn.inner
added theorem Filter.Tendsto.inner
added theorem continuous_inner