From 8cbe72e4f18ae27e0136ad9daf10dbea5944bfbc Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 10 Oct 2025 20:57:44 +0200 Subject: [PATCH 1/3] feat: gaussianReal_ext_iff --- Mathlib/Probability/Distributions/Gaussian/Real.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/Probability/Distributions/Gaussian/Real.lean b/Mathlib/Probability/Distributions/Gaussian/Real.lean index 8fa1882c8290d8..a15c4e6aefc8f0 100644 --- a/Mathlib/Probability/Distributions/Gaussian/Real.lean +++ b/Mathlib/Probability/Distributions/Gaussian/Real.lean @@ -537,6 +537,17 @@ lemma memLp_id_gaussianReal' (p : ℝ≥0∞) (hp : p ≠ ∞) : MemLp id p (gau end Moments +/-- Two real Gaussian distributions are equal iff they have the same mean and variance. -/ +lemma gaussianReal_ext_iff {μ₁ μ₂ : ℝ} {v₁ v₂ : ℝ≥0} : + gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂ ↔ μ₁ = μ₂ ∧ v₁ = v₂ := by + refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩ + rw [← integral_id_gaussianReal (μ := μ₁) (v := v₁), + ← integral_id_gaussianReal (μ := μ₂) (v := v₂), h] + simp only [integral_id_gaussianReal, true_and] + suffices (v₁ : ℝ) = v₂ by simpa + rw [← variance_id_gaussianReal (μ := μ₁) (v := v₁), + ← variance_id_gaussianReal (μ := μ₂) (v := v₂), h] + section LinearMap variable {μ : ℝ} {v : ℝ≥0} From 84198caad2ad16ab87e9420efcc95c4e7d04ca3b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Sun, 12 Oct 2025 11:53:42 +0200 Subject: [PATCH 2/3] Apply suggestion from @RemyDegenne --- Mathlib/Probability/Distributions/Gaussian/Real.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Probability/Distributions/Gaussian/Real.lean b/Mathlib/Probability/Distributions/Gaussian/Real.lean index a15c4e6aefc8f0..000de595de9864 100644 --- a/Mathlib/Probability/Distributions/Gaussian/Real.lean +++ b/Mathlib/Probability/Distributions/Gaussian/Real.lean @@ -538,6 +538,7 @@ lemma memLp_id_gaussianReal' (p : ℝ≥0∞) (hp : p ≠ ∞) : MemLp id p (gau end Moments /-- Two real Gaussian distributions are equal iff they have the same mean and variance. -/ +@[ext] lemma gaussianReal_ext_iff {μ₁ μ₂ : ℝ} {v₁ v₂ : ℝ≥0} : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂ ↔ μ₁ = μ₂ ∧ v₁ = v₂ := by refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩ From cd4aa353da19c534bd3cc3a26f12b5baaba2e2b1 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 14 Oct 2025 13:07:09 +0200 Subject: [PATCH 3/3] fix: remove ext --- Mathlib/Probability/Distributions/Gaussian/Real.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Probability/Distributions/Gaussian/Real.lean b/Mathlib/Probability/Distributions/Gaussian/Real.lean index 000de595de9864..a15c4e6aefc8f0 100644 --- a/Mathlib/Probability/Distributions/Gaussian/Real.lean +++ b/Mathlib/Probability/Distributions/Gaussian/Real.lean @@ -538,7 +538,6 @@ lemma memLp_id_gaussianReal' (p : ℝ≥0∞) (hp : p ≠ ∞) : MemLp id p (gau end Moments /-- Two real Gaussian distributions are equal iff they have the same mean and variance. -/ -@[ext] lemma gaussianReal_ext_iff {μ₁ μ₂ : ℝ} {v₁ v₂ : ℝ≥0} : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂ ↔ μ₁ = μ₂ ∧ v₁ = v₂ := by refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩