From 8e4bc14e358b73acdf3ed060efb30970d49a84fb Mon Sep 17 00:00:00 2001
From: Harald Husum <harald.husum@intelecy.com>
Date: Sun, 29 Mar 2026 19:09:04 +0200
Subject: [PATCH] doc(Analysis): fix typos

---
 Mathlib/Analysis/Distribution/Distribution.lean      | 2 +-
 Mathlib/Analysis/ODE/Gronwall.lean                   | 2 +-
 Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Analysis/Distribution/Distribution.lean b/Mathlib/Analysis/Distribution/Distribution.lean
index cef78d4b56ce64..61503e34b2df75 100644
--- a/Mathlib/Analysis/Distribution/Distribution.lean
+++ b/Mathlib/Analysis/Distribution/Distribution.lean
@@ -127,7 +127,7 @@ which we follow here.
 
 Finally, note that a **sequence** of distributions converges in `𝓓'(Ω, F)` if and only if it
 converges pointwise
-(see [L. Schwartz, *Théorie des distributions*, Chapitre III, §3, Theorème XIII][schwartz1950]).
+(see [L. Schwartz, *Théorie des distributions*, Chapitre III, §3, Théorème XIII][schwartz1950]).
 Due to this fact, some texts endow `𝓓'(Ω, F)` with the pointwise convergence topology. While this
 gives the same converging sequences as the topology of bounded/compact convergence, this is no
 longer true for general filters.
diff --git a/Mathlib/Analysis/ODE/Gronwall.lean b/Mathlib/Analysis/ODE/Gronwall.lean
index 0c420bc54139eb..13e84d93a8aa6b 100644
--- a/Mathlib/Analysis/ODE/Gronwall.lean
+++ b/Mathlib/Analysis/ODE/Gronwall.lean
@@ -89,7 +89,7 @@ theorem gronwallBound_continuous_ε (δ K x : ℝ) : Continuous fun ε => gronwa
   · simp only [gronwallBound_of_K_ne_0 hK]
     fun_prop
 
-/-- The Gronwall bound is monotone with respect to the time variable `x`. -/
+/-- The Grönwall bound is monotone with respect to the time variable `x`. -/
 lemma gronwallBound_mono {δ K ε : ℝ} (hδ : 0 ≤ δ) (hε : 0 ≤ ε) (hK : 0 ≤ K) :
     Monotone (gronwallBound δ K ε) := by
   intro x₁ x₂ hx
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
index 0fb5a6bd93bfde..b098d210c928d5 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
@@ -11,7 +11,7 @@ public import Mathlib.Analysis.SpecialFunctions.Gamma.Beta
 # Deligne's archimedean Gamma-factors
 
 In the theory of L-series one frequently encounters the following functions (of a complex variable
-`s`) introduced in Deligne's landmark paper *Valeurs de fonctions L et periodes d'integrales*:
+`s`) introduced in Deligne's landmark paper *Valeurs de fonctions L et périodes d'intégrales*:
 
 $$ \Gamma_{\mathbb{R}}(s) = \pi ^ {-s / 2} \Gamma (s / 2) $$
 
@@ -38,7 +38,7 @@ namespace Complex
 
 /-- Deligne's archimedean Gamma factor for a real infinite place.
 
-See "Valeurs de fonctions L et periodes d'integrales" § 5.3. Note that this is not the same as
+See "Valeurs de fonctions L et périodes d'intégrales" § 5.3. Note that this is not the same as
 `Real.Gamma`; in particular it is a function `ℂ → ℂ`. -/
 noncomputable def Gammaℝ (s : ℂ) := π ^ (-s / 2) * Gamma (s / 2)
 
@@ -46,7 +46,7 @@ lemma Gammaℝ_def (s : ℂ) : Gammaℝ s = π ^ (-s / 2) * Gamma (s / 2) := rfl
 
 /-- Deligne's archimedean Gamma factor for a complex infinite place.
 
-See "Valeurs de fonctions L et periodes d'integrales" § 5.3. (Some authors omit the factor of 2).
+See "Valeurs de fonctions L et périodes d'intégrales" § 5.3. (Some authors omit the factor of 2).
 Note that this is not the same as `Complex.Gamma`. -/
 noncomputable def Gammaℂ (s : ℂ) := 2 * (2 * π) ^ (-s) * Gamma s