Align wrapped module-doc list items

harahu · harahu · commit 0c4d4f99f848 · 2026-02-14T00:33:57.000+01:00
Indent continuation lines in module-level docstring bullet lists across Analysis files so wrapped entries are consistently nested under their bullets.

This is a whitespace-only documentation formatting cleanup (no theorem/code behavior changes).
diff --git a/Mathlib/Analysis/Asymptotics/ExpGrowth.lean b/Mathlib/Analysis/Asymptotics/ExpGrowth.lean
@@ -18,7 +18,7 @@ versions, using a `liminf` and a `limsup` respectively.
 
 - `expGrowthInf`, `expGrowthSup`: respectively, `liminf` and `limsup` of `log (u n) / n`.
 - `expGrowthInfTopHom`, `expGrowthSupBotHom`: the functions `expGrowthInf`, `expGrowthSup`
-as homomorphisms preserving finitary `Inf`/`Sup` respectively.
+  as homomorphisms preserving finitary `Inf`/`Sup` respectively.
 
 ## Tags
 
diff --git a/Mathlib/Analysis/Asymptotics/LinearGrowth.lean b/Mathlib/Analysis/Asymptotics/LinearGrowth.lean
@@ -18,7 +18,7 @@ versions, using a `liminf` and a `limsup` respectively. Most properties are deve
 
 - `linearGrowthInf`, `linearGrowthSup`: respectively, `liminf` and `limsup` of `(u n) / n`.
 - `linearGrowthInfTopHom`, `linearGrowthSupBotHom`: the functions `linearGrowthInf`,
-`linearGrowthSup` as homomorphisms preserving finitary `Inf`/`Sup` respectively.
+  `linearGrowthSup` as homomorphisms preserving finitary `Inf`/`Sup` respectively.
 
 ## TODO
 
diff --git a/Mathlib/Analysis/Complex/Hadamard.lean b/Mathlib/Analysis/Complex/Hadamard.lean
@@ -16,17 +16,17 @@ In this file we present a proof of Hadamard's three-lines Theorem.
 ## Main result
 
 - `norm_le_interp_of_mem_verticalClosedStrip` :
-Hadamard three-line theorem: If `f` is a bounded function, continuous on
-`re ⁻¹' [l, u]` and differentiable on `re ⁻¹' (l, u)`, then for
-`M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x}))`, that is `M(x)` is the supremum of the absolute value of
-`f` along the vertical lines `re z = x`, we have that `∀ z ∈ re ⁻¹' [l, u]` the inequality
-`‖f(z)‖ ≤ M(0) ^ (1 - ((z.re - l) / (u - l))) * M(1) ^ ((z.re - l) / (u - l))` holds.
-This can be seen to be equivalent to the statement
-that `log M(re z)` is a convex function on `[0, 1]`.
+  Hadamard three-line theorem: If `f` is a bounded function, continuous on
+  `re ⁻¹' [l, u]` and differentiable on `re ⁻¹' (l, u)`, then for
+  `M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x}))`, that is `M(x)` is the supremum of the absolute value of
+  `f` along the vertical lines `re z = x`, we have that `∀ z ∈ re ⁻¹' [l, u]` the inequality
+  `‖f(z)‖ ≤ M(0) ^ (1 - ((z.re - l) / (u - l))) * M(1) ^ ((z.re - l) / (u - l))` holds.
+  This can be seen to be equivalent to the statement
+  that `log M(re z)` is a convex function on `[0, 1]`.
 
 - `norm_le_interp_of_mem_verticalClosedStrip'` :
-Variant of the above lemma in simpler terms. In particular, it makes no mention of the helper
-functions defined in this file.
+  Variant of the above lemma in simpler terms. In particular, it makes no mention of the helper
+  functions defined in this file.
 
 ## Main definitions
 
diff --git a/Mathlib/Analysis/Distribution/TemperedDistribution.lean b/Mathlib/Analysis/Distribution/TemperedDistribution.lean
@@ -16,22 +16,22 @@ public import Mathlib.Topology.Algebra.Module.PointwiseConvergence
 ## Main definitions
 
 * `TemperedDistribution E F`: The space `𝓢(E, ℂ) →L[ℂ] F` equipped with the pointwise
-convergence topology.
+  convergence topology.
 * `MeasureTheory.Measure.toTemperedDistribution`: Every measure of temperate growth is a tempered
-distribution.
+  distribution.
 * `Function.HasTemperateGrowth.toTemperedDistribution`: Every function of temperate growth is a
-tempered distribution.
+  tempered distribution.
 * `SchwartzMap.toTemperedDistributionCLM`: The canonical map from `𝓢` to `𝓢'` as a continuous linear
-map.
+  map.
 * `MeasureTheory.Lp.toTemperedDistribution`: Every `Lp` function is a tempered distribution.
 * `TemperedDistribution.mulLeftCLM`: Multiplication with temperate growth function as a continuous
-linear map.
+  linear map.
 * `TemperedDistribution.instLineDeriv`: The directional derivative on tempered distributions.
 * `TemperedDistribution.fourierTransformCLM`: The Fourier transform on tempered distributions.
 
 ## Notation
 * `𝓢'(E, F)`: The space of tempered distributions `TemperedDistribution E F` scoped in
-`SchwartzMap`
+  `SchwartzMap`
 -/
 
 @[expose] public noncomputable section
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -49,7 +49,7 @@ the last section, various properties of matrices are explored.
 - `exists_orthonormalBasis`: provides an orthonormal basis on a finite-dimensional vector space
 
 - `stdOrthonormalBasis`: provides an arbitrarily-chosen `OrthonormalBasis` of a given
-finite-dimensional inner product space
+  finite-dimensional inner product space
 
 For consequences in infinite dimension (Hilbert bases, etc.), see the file
 `Analysis.InnerProductSpace.L2Space`.
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean b/Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
@@ -20,7 +20,7 @@ This file contains results about orthogonal projections in finite-dimensional sp
 
 * `Submodule.det_reflection`: The determinant of `K.reflection` is `(-1) ^ finrank 𝕜 Kᗮ`.
 * `LinearIsometryEquiv.reflections_generate`: The orthogonal group of `F` is
-generated by reflections.
+  generated by reflections.
 
 ## Results that do not use finite dimensionality:
 
diff --git a/Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean b/Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean
@@ -16,7 +16,7 @@ We prove that the topology of pointwise convergence is induced by a family of se
 that it is locally convex in the topological sense
 
 * `PointwiseConvergenceCLM.seminorm`: the seminorms on `E →SLₚₜ[σ] F` given by `A ↦ ‖A x‖` for fixed
-`x : E`.
+  `x : E`.
 * `PointwiseConvergenceCLM.withSeminorm`: the topology is induced by the seminorms.
 * `PointwiseConvergenceCLM.instLocallyConvexSpace`: `E →SLₚₜ[σ] F` is locally convex.
 
diff --git a/Mathlib/Analysis/Matrix/Order.lean b/Mathlib/Analysis/Matrix/Order.lean
@@ -21,9 +21,9 @@ This allows us to use more general results from C⋆-algebras, like `CFC.sqrt`.
 
 * `Matrix.instPartialOrder`: the partial order on matrices given by `x ≤ y := (y - x).PosSemidef`.
 * `Matrix.PosSemidef.dotProduct_mulVec_zero_iff`: for a positive semi-definite matrix `A`,
-we have `x⋆ A x = 0` iff `A x = 0`.
+  we have `x⋆ A x = 0` iff `A x = 0`.
 * `Matrix.toMatrixInnerProductSpace`: the inner product on matrices induced by a
-positive semi-definite matrix `M`: `⟪x, y⟫ = (y * M * xᴴ).trace`.
+  positive semi-definite matrix `M`: `⟪x, y⟫ = (y * M * xᴴ).trace`.
 
 ## Implementation notes
 
diff --git a/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean
@@ -59,7 +59,7 @@ space.
 
 * `PiTensorProduct.norm_eval_le_injectiveSeminorm`: The main property of the injective seminorm
   on `⨂[𝕜] i, Eᵢ`: for every `x` in `⨂[𝕜] i, Eᵢ` and every continuous multilinear map `f` from
-`E = Πᵢ Eᵢ` to a normed space `F`, we have `‖f.lift x‖ ≤ ‖f‖ * injectiveSeminorm x `.
+  `E = Πᵢ Eᵢ` to a normed space `F`, we have `‖f.lift x‖ ≤ ‖f‖ * injectiveSeminorm x `.
 * `PiTensorProduct.mapL_opNorm`: If `f` is a family of continuous linear maps
   `fᵢ : Eᵢ →L[𝕜] Fᵢ`, then `‖PiTensorProduct.mapL f‖ ≤ ∏ i, ‖fᵢ‖`.
 * `PiTensorProduct.mapLMultilinear_opNorm` : If `F` is a normed vecteor space, then
diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -31,7 +31,7 @@ topology.
 The main definitions concern the canonical mapping `StrongDual 𝕜 E → WeakDual 𝕜 E`.
 
 * `StrongDual.toWeakDual` and `WeakDual.toStrongDual`: Linear equivalences from `StrongDual 𝕜 E` to
-`WeakDual 𝕜 E` and in the converse direction.
+  `WeakDual 𝕜 E` and in the converse direction.
 * `NormedSpace.Dual.continuousLinearMapToWeakDual`: A continuous linear mapping from
   `StrongDual 𝕜 E` to `WeakDual 𝕜 E` (same as `StrongDual.toWeakDual` but different bundled data).
 
diff --git a/Mathlib/Analysis/Normed/Operator/Extend.lean b/Mathlib/Analysis/Normed/Operator/Extend.lean
@@ -16,18 +16,18 @@ In this file we provide two different ways to extend a continuous linear map def
 subspace to the entire Banach space.
 
 * `ContinuousLinearMap.extend`: Extend `f : E →SL[σ₁₂] F` to a continuous linear map
-`Eₗ →SL[σ₁₂] F`, where `e : E →ₗ[𝕜] Eₗ` is a dense map that is `IsUniformInducing`.
+  `Eₗ →SL[σ₁₂] F`, where `e : E →ₗ[𝕜] Eₗ` is a dense map that is `IsUniformInducing`.
 * `LinearMap.extendOfNorm`: Extend `f : E →ₛₗ[σ₁₂] F` to a continuous linear map
-`Eₗ →SL[σ₁₂] F`, where `e : E →ₗ[𝕜] Eₗ` is a dense map and we have the norm estimate
-`‖f x‖ ≤ C * ‖e x‖` for all `x : E`.
+  `Eₗ →SL[σ₁₂] F`, where `e : E →ₗ[𝕜] Eₗ` is a dense map and we have the norm estimate
+  `‖f x‖ ≤ C * ‖e x‖` for all `x : E`.
 
 Moreover, we can extend a linear equivalence:
 * `LinearEquiv.extend`: Extend a linear equivalence between normed spaces to a continuous linear
-equivalence between Banach spaces with two dense maps `e₁` and `e₂` and the corresponding norm
-estimates.
+  equivalence between Banach spaces with two dense maps `e₁` and `e₂` and the corresponding norm
+  estimates.
 * `LinearEquiv.extendOfIsometry`: Extend `f : E ≃ₗ[𝕜] F` to a linear isometry equivalence
-`Eₗ →ₗᵢ[𝕜] Fₗ`, where `e₁ : E →ₗ[𝕜] Eₗ` and `e₂ : F →ₗ[𝕜] Fₗ` are dense maps into Banach spaces
-and `f` preserves the norm.
+  `Eₗ →ₗᵢ[𝕜] Fₗ`, where `e₁ : E →ₗ[𝕜] Eₗ` and `e₂ : F →ₗ[𝕜] Fₗ` are dense maps into Banach spaces
+  and `f` preserves the norm.
 
 -/
 
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
@@ -23,8 +23,8 @@ in the extended reals `EReal`, with `log 0 = ⊥` and `log ⊤ = ⊤`.
 - `ENNReal.log_injective`, `ENNReal.log_surjective`, `ENNReal.log_bijective`: `log` is
   injective, surjective, and bijective;
 - `ENNReal.log_mul_add`, `ENNReal.log_pow`, `ENNReal.log_rpow`: `log` satisfies
-the identities `log (x * y) = log x + log y` and `log (x ^ y) = y * log x`
-(with either `y ∈ ℕ` or `y ∈ ℝ`).
+  the identities `log (x * y) = log x + log y` and `log (x ^ y) = y * log x`
+  (with either `y ∈ ℕ` or `y ∈ ℝ`).
 
 ## Tags
 ENNReal, EReal, logarithm
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean b/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean
@@ -16,16 +16,16 @@ public import Mathlib.Topology.MetricSpace.Polish
 We prove that `log` and `exp` define order isomorphisms between `ℝ≥0∞` and `EReal`.
 ## Main DefinitionsP
 - `ENNReal.logOrderIso`: The order isomorphism between `ℝ≥0∞` and `EReal` defined by `log`
-and `exp`.
+  and `exp`.
 - `EReal.expOrderIso`: The order isomorphism between `EReal` and `ℝ≥0∞` defined by `exp`
-and `log`.
+  and `log`.
 - `ENNReal.logHomeomorph`: `log` as a homeomorphism.
 - `EReal.expHomeomorph`: `exp` as a homeomorphism.
 
 ## Main Results
 - `EReal.log_exp`, `ENNReal.exp_log`: `log` and `exp` are inverses of each other.
 - `EReal.exp_nmul`, `EReal.exp_mul`: `exp` satisfies the identities `exp (n * x) = (exp x) ^ n`
-and `exp (x * y) = (exp x) ^ y`.
+  and `exp (x * y) = (exp x) ^ y`.
 - `EReal` is a Polish space.
 
 ## Tags
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean b/Mathlib/Analysis/SpecialFunctions/Log/ERealExp.lean
@@ -21,7 +21,7 @@ in the extended nonnegative reals `ℝ≥0∞`, with `exp ⊥ = 0` and `exp ⊤
 ## Main Results
 - `EReal.exp_strictMono`: `exp` is increasing;
 - `EReal.exp_neg`, `EReal.exp_add`: `exp` satisfies
-the identities `exp (-x) = (exp x)⁻¹` and `exp (x + y) = exp x * exp y`.
+  the identities `exp (-x) = (exp x)⁻¹` and `exp (x + y) = exp x * exp y`.
 
 ## Tags
 ENNReal, EReal, exponential
diff --git a/Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean b/Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
@@ -27,17 +27,17 @@ that `-n < a` for the `n`-th term, and similarly for `b` and `c`.
 - `ordinaryHypergeometricSeries` is the `FormalMultilinearSeries` given above for some `(a b c : 𝕂)`
 - `ordinaryHypergeometric` is the sum of the series for some `(x : 𝔸)`
 - `ordinaryHypergeometricSeries_eq_zero_of_nonpos_int` shows that the `n`-th term of the series is
-zero if any of the parameters are sufficiently large non-positive integers
+  zero if any of the parameters are sufficiently large non-positive integers
 
 ## `[RCLike 𝕂]`
 
 If we have `[RCLike 𝕂]`, then we show that the latter result is an iff, and hence prove that the
 radius of convergence of the series is unity if the series is infinite, or `⊤` otherwise.
 
 - `ordinaryHypergeometricSeries_eq_zero_iff` is iff variant of
-`ordinaryHypergeometricSeries_eq_zero_of_nonpos_int`
+  `ordinaryHypergeometricSeries_eq_zero_of_nonpos_int`
 - `ordinaryHypergeometricSeries_radius_eq_one` proves that the radius of convergence of the
-`ordinaryHypergeometricSeries` is unity under non-trivial parameters
+  `ordinaryHypergeometricSeries` is unity under non-trivial parameters
 
 ## Notation
 
