chore(Analysis/Calculus): remove unnecessary @[expose] from public sections (leanprover-community#33565)

This PR removes `@[expose]` from `public section` declarations in 87 files under `Mathlib/Analysis/Calculus/` and related directories.

These files only contain theorems/lemmas (no definitions, instances, or other computational content that requires exposed bodies). The `@[expose]` attribute explicitly exposes definition bodies, but theorems have their proofs erased when exported, so `@[expose]` is not needed for them.

This is part of a larger effort to clean up unnecessary `@[expose]` attributes across Mathlib (~1400 files identified as candidates).

🤖 Prepared with Claude Code

Author: kim-em

Mathlib/Analysis/BoundedVariation.lean

@@ -31,7 +31,7 @@ We also give several variations around these results.
 
 -/
 
-@[expose] public section
+public section
 
 open scoped NNReal Topology
 open Set MeasureTheory Filter

Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean

@@ -20,7 +20,7 @@ This file contains results about smoothness of affine maps.
 
 -/
 
-@[expose] public section
+public section
 namespace ContinuousAffineMap
 
 variable {𝕜 V W : Type*} [NontriviallyNormedField 𝕜]

Mathlib/Analysis/Calculus/AddTorsor/Coord.lean

@@ -12,7 +12,7 @@ public import Mathlib.Analysis.Normed.Affine.AddTorsorBases
 # Barycentric coordinates are smooth
 -/
 
-@[expose] public section
+public section
 
 variable {ι 𝕜 E P : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
 variable [NormedAddCommGroup E] [NormedSpace 𝕜 E]

Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

@@ -39,7 +39,7 @@ We also provide estimates in the case if `g x` is close to `g x₀` on this ball
 convolution, smooth function, bump function
 -/
 
-@[expose] public section
+public section
 
 universe uG uE'
 

Mathlib/Analysis/Calculus/BumpFunction/SmoothApprox.lean

@@ -21,7 +21,7 @@ and `HasCompactSupport.contDiff_convolution_left`.
 Here we wrap these results removing measure-related arguments from the assumptions.
 -/
 
-@[expose] public section
+public section
 
 variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
   [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : E → F} {ε : ℝ}

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -34,7 +34,7 @@ In this file, we denote `(⊤ : ℕ∞) : WithTop ℕ∞` with `∞` and `⊤ :
 derivative, differentiability, higher derivative, `C^n`, multilinear, Taylor series, formal series
 -/
 
-@[expose] public section
+public section
 
 noncomputable section
 

Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

@@ -18,7 +18,7 @@ public import Mathlib.Data.Nat.Choose.Multinomial
   derivative of `f` is bounded by `D ^ i`.
 -/
 
-@[expose] public section
+public section
 
 noncomputable section
 

Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean

@@ -15,7 +15,7 @@ We prove that continuously polynomial functions are `C^∞`. In particular, this
 of continuous multilinear maps.
 -/
 
-@[expose] public section
+public section
 
 open Filter Asymptotics
 

Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean

@@ -13,7 +13,7 @@ public import Mathlib.Analysis.Normed.Module.FiniteDimension
 
 -/
 
-@[expose] public section
+public section
 
 
 noncomputable section

Mathlib/Analysis/Calculus/ContDiff/Polynomial.lean

@@ -14,7 +14,7 @@ public import Mathlib.Analysis.Calculus.ContDiff.Operations
 We prove that polynomials are `C^∞`.
 -/
 
-@[expose] public section
+public section
 
 namespace Polynomial