feat(UnitInterval): x : I and its symmetric sum to 1 (#31396)

Author: YaelDillies

Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.MeasureTheory.Measure.Typeclasses.Finite
+import Mathlib.Topology.UnitInterval
 
 /-!
 # Classes for probability measures
@@ -92,6 +93,11 @@ instance isProbabilityMeasure_ite {p : Prop} [Decidable p] {μ ν : Measure α}
     [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
     IsProbabilityMeasure (ite p μ ν) := by split <;> infer_instance
 
+open unitInterval in
+instance {μ ν : Measure α} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {p : I} :
+    IsProbabilityMeasure (toNNReal p • μ + toNNReal (σ p) • ν) where
+  measure_univ := by simp [← add_smul]
+
 variable [IsProbabilityMeasure μ] {p : α → Prop} {f : β → α}
 
 theorem Measure.isProbabilityMeasure_map {f : α → β} (hf : AEMeasurable f μ) :

Mathlib/Topology/UnitInterval.lean

@@ -385,19 +385,21 @@ theorem iccHomeoI_symm_apply_coe (a b : 𝕜) (h : a < b) (x : Set.Icc (0 : 𝕜
 
 end
 
-section NNReal
+namespace unitInterval
 
-open unitInterval NNReal
+open NNReal
 
 /-- The coercion from `I` to `ℝ≥0`. -/
-def unitInterval.toNNReal : I → ℝ≥0 := fun i ↦ ⟨i.1, i.2.1⟩
+def toNNReal : I → ℝ≥0 := fun i ↦ ⟨i.1, i.2.1⟩
 
-@[fun_prop]
-lemma unitInterval.toNNReal_continuous : Continuous toNNReal := by
-  delta toNNReal
-  fun_prop
+@[simp] lemma toNNReal_zero : toNNReal 0 = 0 := rfl
+@[simp] lemma toNNReal_one : toNNReal 1 = 1 := rfl
 
-@[simp]
-lemma unitInterval.coe_toNNReal (x : I) : ((toNNReal x) : ℝ) = x := rfl
+@[fun_prop] lemma toNNReal_continuous : Continuous toNNReal := by delta toNNReal; fun_prop
+
+@[simp] lemma coe_toNNReal (x : I) : ((toNNReal x) : ℝ) = x := rfl
 
-end NNReal
+@[simp] lemma toNNReal_add_toNNReal_symm (x : I) : toNNReal x + toNNReal (σ x) = 1 := by ext; simp
+@[simp] lemma toNNReal_symm_add_toNNReal (x : I) : toNNReal (σ x) + toNNReal x = 1 := by ext; simp
+
+end unitInterval