From 55c114bd3b62ed354b5463c29bbb3457f1363285 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Fri, 16 Jan 2026 13:02:59 +0100 Subject: [PATCH 1/8] progress --- Mathlib/test.lean | 158 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 158 insertions(+) create mode 100644 Mathlib/test.lean diff --git a/Mathlib/test.lean b/Mathlib/test.lean new file mode 100644 index 00000000000000..89159be349be49 --- /dev/null +++ b/Mathlib/test.lean @@ -0,0 +1,158 @@ +/- +Copyright (c) 2026 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sébastien Gouëzel +-/ +module + +public import Mathlib + +/-! +# Vector valued Stieltjes measure + +-/ + + +/- +Stratégie globale : +1 - définir une distance sur les ensembles mesurables, donnée par la mesure de leur différence +symétrique +2 - si `m` est une mesure vectorielle finiment additive sur une classe d'ensembles mesurables +dense, majorée par une mesure finie `μ`, alors elle s'étend aux ensembles mesurables en une mesure +vectorielle dénombrablement additive +3 - Cas particulier pour construire une mesure finiment additive sur une classe d'ensembles assez +grande. On part d'un SetSemiring `C` (par exemple les intervalles semi-ouverts) avec une fonction +additive `m` dessus (i.e., si les `sᵢ` sont tous dans `C`, ainsi que leur union disjointe finie, +alors `m (⋃ sᵢ) = ∑ i, m (sᵢ)`). Alors `m` s'étend aux unions finies d'éléments de `C` en y restant +additive. Idée : si `c` s'écrit à la fois comme union disjointe des `sᵢ` et des `tⱼ`, il faut voir +que `∑ m (sᵢ) = ∑ m (tⱼ)`. On le réécrit comme `∑ m (sᵢ ∩ tⱼ)` et on somme soit d'abord sur les `i` +soit d'abord sur les `j`. +4 - implémenter ça pour les mesures de Stieltjes, avec `m ((a, b]) = f b - f a` pour `C` la classe +des intervalles semi-ouverts. Alors 3. est satisfait. +-/ + +open Filter +open scoped symmDiff Topology + +variable {α : Type*} [MeasurableSpace α] {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E] +[CompleteSpace E] + +namespace MeasureTheory + +set_option linter.unusedVariables false in +def MeasuredSets (μ : Measure α) : Type _ := + {s : Set α // MeasurableSet s} + +variable {μ : Measure α} + +instance : SetLike (MeasuredSets μ) α where + coe s := s.1 + coe_injective' := Subtype.coe_injective + +instance : PseudoEMetricSpace (MeasuredSets μ) where + edist s t := μ ((s : Set α) ∆ t) + edist_self := by simp + edist_comm := by grind + edist_triangle s t u := measure_symmDiff_le _ _ _ + +lemma MeasuredSets.edist_def (s t : MeasuredSets μ) : edist s t = μ ((s : Set α) ∆ t) := rfl + +lemma MeasuredSets.continuous_measure : Continuous (fun (s : MeasuredSets μ) ↦ μ s) := by + apply continuous_iff_continuousAt.2 (fun x ↦ ?_) + simp only [ContinuousAt] + rcases eq_top_or_lt_top (μ x) with hx | hx + · simp only [hx] + apply tendsto_const_nhds.congr' + filter_upwards [EMetric.ball_mem_nhds _ zero_lt_one] with y hy + simp only [EMetric.mem_ball, edist_def] at hy + contrapose! hy + simp [measure_symmDiff_eq_top hy.symm hx] + · apply (ENNReal.hasBasis_nhds_of_ne_top hx.ne).tendsto_right_iff.2 (fun ε εpos ↦ ?_) + filter_upwards [EMetric.ball_mem_nhds _ εpos] with a ha + simp only [EMetric.mem_ball, edist_def] at ha + refine ⟨?_, ?_⟩ + · apply tsub_le_iff_right.mpr + calc μ x + _ ≤ μ a + μ (x \ a) := by + rw [← measure_union Set.disjoint_sdiff_right (by exact x.2.diff a.2)] + apply measure_mono + exact Set.diff_subset_iff.mp fun ⦃a_1⦄ a ↦ a + _ ≤ μ a + μ (a ∆ x) := by + gcongr + simp [symmDiff] + _ ≤ μ a + ε := by + gcongr + · calc μ a + _ ≤ μ x + μ (a \ x) := by + rw [← measure_union Set.disjoint_sdiff_right (by exact a.2.diff x.2)] + apply measure_mono + exact Set.diff_subset_iff.mp fun ⦃a_1⦄ a ↦ a + _ ≤ μ x + μ (a ∆ x) := by + gcongr + simp [symmDiff] + _ ≤ μ x + ε := by + gcongr + + +lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m : Set α → E) + (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) + (h'm : ∀ s ∈ C, ∀ t ∈ C, Disjoint s t → m (s ∪ t) = m s + m t) + (hm_diff : ∀ s ∈ C, ∀ t ∈ C, s \ t ∈ C) + (hm_inter : ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C) + (h'C : ∀ t ε, MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε) : + ∃ m' : VectorMeasure α E, ∀ s ∈ C, m' s = m s ∧ ∀ s, ‖m' s‖ₑ ≤ μ s := by + let C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, s = c} + have C'C (s : MeasuredSets μ) (hs : s ∈ C') : (s : Set α) ∈ C := by + rcases hs with ⟨t, ht, rfl⟩ + exact ht + have C'_dense : Dense C' := by + simp only [Dense, EMetric.mem_closure_iff, gt_iff_lt] + intro x ε εpos + rcases h'C x ε x.2 εpos with ⟨s, sC, hs⟩ + refine ⟨⟨s, hC s sC⟩, ⟨s, sC, rfl⟩, ?_⟩ + rw [edist_comm] + exact hs + have A {s t : Set α} : Disjoint (s ∩ t) (s \ t) := Set.disjoint_sdiff_inter.symm + let m₀ : C' → E := fun x ↦ m x + have lip : LipschitzWith 1 m₀ := by + intro s t + have : edist s t = edist (s : MeasuredSets μ) t := rfl + simp only [ENNReal.coe_one, one_mul, this, MeasuredSets.edist_def, m₀, edist_eq_enorm_sub] + rw [measure_symmDiff_eq]; rotate_left + · exact s.1.2.nullMeasurableSet + · exact t.1.2.nullMeasurableSet + have Is : ((s : Set α) ∩ t) ∪ (s \ t) = (s : Set α) := Set.inter_union_diff _ _ + have It : ((t : Set α) ∩ s) ∪ (t \ s) = (t : Set α) := Set.inter_union_diff _ _ + nth_rewrite 1 [← Is] + nth_rewrite 3 [← It] + rw [h'm _ (hm_inter _ (C'C _ t.2) _ (C'C _ s.2)) _ (hm_diff _ (C'C _ t.2) _ (C'C _ s.2)) A, + h'm _ (hm_inter _ (C'C _ s.2) _ (C'C _ t.2)) _ (hm_diff _ (C'C _ s.2) _ (C'C _ t.2)) A, + Set.inter_comm] + simp only [add_sub_add_left_eq_sub, ge_iff_le] + apply enorm_sub_le.trans + gcongr + · exact hm _ (hm_diff _ (C'C _ s.2) _ (C'C _ t.2)) + · exact hm _ (hm_diff _ (C'C _ t.2) _ (C'C _ s.2)) + let m₁ : MeasuredSets μ → E := C'_dense.extend m₀ + have m₁_cont : UniformContinuous m₁ := C'_dense.uniformContinuous_extend lip.uniformContinuous + have B s : ‖m₁ s‖ₑ ≤ μ s := by + have : IsClosed {s | ‖m₁ s‖ₑ ≤ μ s} := + isClosed_le m₁_cont.continuous.enorm MeasuredSets.continuous_measure + + + + + classical + have A (s : MeasuredSets μ) : Cauchy (map m₀ (𝓝[C'] s)) := by + have W := LipschitzOnWith.cauchySeq_comp + apply Metric.cauchy_iff.2 ⟨?_, ?_⟩ + · have : (𝓝[C'] s).NeBot := mem_closure_iff_nhdsWithin_neBot.mp (C'_dense s) + exact map_neBot + · intro ε εpos + simp + + + let m' (s : Set α) := if h : MeasurableSet s then limUnder (𝓝[C'] ⟨s, h⟩) (fun t ↦ m t) else 0 + + +#exit From e00a7db3c942936d556e3c8c29f67ddcde92070e Mon Sep 17 00:00:00 2001 From: sgouezel Date: Fri, 16 Jan 2026 17:17:17 +0100 Subject: [PATCH 2/8] progress --- Mathlib/test.lean | 139 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 119 insertions(+), 20 deletions(-) diff --git a/Mathlib/test.lean b/Mathlib/test.lean index 89159be349be49..8cbdba5dfb893e 100644 --- a/Mathlib/test.lean +++ b/Mathlib/test.lean @@ -32,14 +32,33 @@ des intervalles semi-ouverts. Alors 3. est satisfait. -/ open Filter -open scoped symmDiff Topology +open scoped symmDiff Topology NNReal -variable {α : Type*} [MeasurableSpace α] {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E] +variable {α : Type*} [MeasurableSpace α] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] +lemma Set.union_symmDiff_subset {α : Type*} (a b c : Set α) : (a ∪ b) ∆ c ⊆ a ∆ c ∪ b ∆ c := by + intro x hx + simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ + grind + +lemma Set.symmDiff_union_subset {α : Type*} (a b c : Set α) : a ∆ (b ∪ c) ⊆ a ∆ b ∪ a ∆ c := by + intro x hx + simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ + grind + +lemma Set.union_symmDiff_union_subset {α : Type*} (a b c d : Set α) : + (a ∪ b) ∆ (c ∪ d) ⊆ a ∆ c ∪ b ∆ d := by + intro x hx + simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ + grind + + namespace MeasureTheory set_option linter.unusedVariables false in +/-- The subtype of all measurable sets. We define it as `MeasuredSets μ` to be able to define +a distance on it given by `edist s t = μ (s ∆ t)` -/ def MeasuredSets (μ : Measure α) : Type _ := {s : Set α // MeasurableSet s} @@ -93,14 +112,34 @@ lemma MeasuredSets.continuous_measure : Continuous (fun (s : MeasuredSets μ) _ ≤ μ x + ε := by gcongr +lemma _root_.Dense.lipschitzWith_extend {α β : Type*} + [PseudoEMetricSpace α] [MetricSpace β] [CompleteSpace β] + {s : Set α} (hs : Dense s) {f : s → β} {K : ℝ≥0} (hf : LipschitzWith K f) : + LipschitzWith K (hs.extend f) := by + have : IsClosed {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by + have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous + apply isClosed_le (by fun_prop) + exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop) + have : Dense {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by + apply (hs.prod hs).mono + rintro ⟨x, y⟩ ⟨hx, hy⟩ + have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩ + have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩ + simp only [Set.mem_setOf_eq, Ax, Ay] + exact hf ⟨x, hx⟩ ⟨y, hy⟩ + simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq, Prod.forall] using this + +open scoped ENNReal lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m : Set α → E) (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) (h'm : ∀ s ∈ C, ∀ t ∈ C, Disjoint s t → m (s ∪ t) = m s + m t) - (hm_diff : ∀ s ∈ C, ∀ t ∈ C, s \ t ∈ C) - (hm_inter : ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C) + (hC_diff : ∀ s ∈ C, ∀ t ∈ C, s \ t ∈ C) + (hC_inter : ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C) + (hC_union : ∀ s ∈ C, ∀ t ∈ C, s ∪ t ∈ C) (h'C : ∀ t ε, MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε) : ∃ m' : VectorMeasure α E, ∀ s ∈ C, m' s = m s ∧ ∀ s, ‖m' s‖ₑ ≤ μ s := by + classical let C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, s = c} have C'C (s : MeasuredSets μ) (hs : s ∈ C') : (s : Set α) ∈ C := by rcases hs with ⟨t, ht, rfl⟩ @@ -125,34 +164,94 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m have It : ((t : Set α) ∩ s) ∪ (t \ s) = (t : Set α) := Set.inter_union_diff _ _ nth_rewrite 1 [← Is] nth_rewrite 3 [← It] - rw [h'm _ (hm_inter _ (C'C _ t.2) _ (C'C _ s.2)) _ (hm_diff _ (C'C _ t.2) _ (C'C _ s.2)) A, - h'm _ (hm_inter _ (C'C _ s.2) _ (C'C _ t.2)) _ (hm_diff _ (C'C _ s.2) _ (C'C _ t.2)) A, + rw [h'm _ (hC_inter _ (C'C _ t.2) _ (C'C _ s.2)) _ (hC_diff _ (C'C _ t.2) _ (C'C _ s.2)) A, + h'm _ (hC_inter _ (C'C _ s.2) _ (C'C _ t.2)) _ (hC_diff _ (C'C _ s.2) _ (C'C _ t.2)) A, Set.inter_comm] simp only [add_sub_add_left_eq_sub, ge_iff_le] apply enorm_sub_le.trans gcongr - · exact hm _ (hm_diff _ (C'C _ s.2) _ (C'C _ t.2)) - · exact hm _ (hm_diff _ (C'C _ t.2) _ (C'C _ s.2)) + · exact hm _ (hC_diff _ (C'C _ s.2) _ (C'C _ t.2)) + · exact hm _ (hC_diff _ (C'C _ t.2) _ (C'C _ s.2)) let m₁ : MeasuredSets μ → E := C'_dense.extend m₀ - have m₁_cont : UniformContinuous m₁ := C'_dense.uniformContinuous_extend lip.uniformContinuous - have B s : ‖m₁ s‖ₑ ≤ μ s := by + have m₁_lip : LipschitzWith 1 m₁ := C'_dense.lipschitzWith_extend lip + have B : ∀ s, ‖m₁ s‖ₑ ≤ μ s := by have : IsClosed {s | ‖m₁ s‖ₑ ≤ μ s} := - isClosed_le m₁_cont.continuous.enorm MeasuredSets.continuous_measure + isClosed_le m₁_lip.continuous.enorm MeasuredSets.continuous_measure + have : Dense {s | ‖m₁ s‖ₑ ≤ μ s} := by + apply C'_dense.mono + intro s hs + simp only [Set.mem_setOf_eq] + convert hm s (C'C s hs) + exact C'_dense.extend_eq lip.continuous ⟨s, hs⟩ + simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq] using this + have B' (s t : MeasuredSets μ) (h : Disjoint (s : Set α) t) : + m₁ ⟨s ∪ t, s.2.union t.2⟩ = m₁ s + m₁ t := by + suffices ∀ ε > 0, ‖m₁ (⟨s ∪ t, s.2.union t.2⟩) - m₁ s - m₁ t‖ₑ < ε by + rw [← sub_eq_zero, ← enorm_eq_zero] + contrapose! this + exact ⟨‖m₁ ⟨s ∪ t, s.2.union t.2⟩ - (m₁ s + m₁ t)‖ₑ, this.bot_lt, le_of_eq (by abel_nf)⟩ + intro ε εpos + obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ 16 * δ ≤ ε := by + refine ⟨ε / 16, (ENNReal.div_pos εpos.ne' (by simp)), le_of_eq ?_⟩ + exact ENNReal.mul_div_cancel (by simp) (by simp) + obtain ⟨s', s'C, hs'⟩ : ∃ s' ∈ C, μ (s' ∆ s) < δ := h'C _ _ s.2 δpos + obtain ⟨t', t'C, ht'⟩ : ∃ t' ∈ C, μ (t' ∆ t) < δ := h'C _ _ t.2 δpos + have It : ‖m t' - m₁ t‖ₑ < δ := by + have : m₁ ⟨t', hC _ t'C⟩ = m t' := + C'_dense.extend_eq lip.continuous ⟨⟨t', hC _ t'C⟩, ⟨t', t'C, rfl⟩⟩ + rw [← this, ← edist_eq_enorm_sub] + apply (m₁_lip _ _).trans_lt + simp only [ENNReal.coe_one, MeasuredSets.edist_def, one_mul] + exact ht' + have I : s' ∩ t' ⊆ s ∩ t ∪ (s' ∆ s) ∪ (t' ∆ t) := by + intro x ⟨hxs', hxt'⟩ + by_cases hxs : x ∈ s <;> by_cases hxt : x ∈ t <;> + simp [hxs, hxt, hxs', hxt', symmDiff] + have hμ' : μ (s' ∩ t') < 2 * δ := calc + μ (s' ∩ t') + _ ≤ μ (s ∩ t ∪ (s' ∆ s) ∪ (t' ∆ t)) := measure_mono I + _ = μ ((s' ∆ s) ∪ (t' ∆ t)) := by simp [Set.disjoint_iff_inter_eq_empty.mp h] + _ ≤ μ (s' ∆ s) + μ (t' ∆ t) := measure_union_le _ _ + _ < δ + δ := by gcongr + _ = 2 * δ := by ring + let s'' := s' \ t' + have s''C : s'' ∈ C := hC_diff _ s'C _ t'C + have hs'' : μ (s'' ∆ s) < 3 * δ := calc + μ (s'' ∆ s) + _ ≤ μ (s'' ∆ s') + μ (s' ∆ s) := measure_symmDiff_le _ _ _ + _ < 2 * δ + δ := by gcongr; simp [s'', symmDiff, hμ'] + _ = 3 * δ := by ring + have Is : ‖m s'' - m₁ s‖ₑ < 3 * δ := by + have : m₁ ⟨s'', hC _ s''C⟩ = m s'' := + C'_dense.extend_eq lip.continuous ⟨⟨s'', hC _ s''C⟩, ⟨s'', s''C, rfl⟩⟩ + rw [← this, ← edist_eq_enorm_sub] + apply (m₁_lip _ _).trans_lt + simp only [ENNReal.coe_one, MeasuredSets.edist_def, one_mul] + exact hs'' + have Ist : ‖m (s'' ∪ t') - m₁ ⟨s ∪ t, s.2.union t.2⟩‖ₑ < 4 * δ := by + have s''t'C : s'' ∪ t' ∈ C := hC_union _ s''C _ t'C + have : m₁ ⟨s'' ∪ t', hC _ s''t'C⟩ = m (s'' ∪ t') := + C'_dense.extend_eq lip.continuous ⟨⟨s'' ∪ t', hC _ s''t'C⟩, ⟨s'' ∪ t', s''t'C, rfl⟩⟩ + rw [← this, ← edist_eq_enorm_sub] + apply (m₁_lip _ _).trans_lt + simp only [ENNReal.coe_one, MeasuredSets.edist_def, one_mul] + change μ ((s'' ∪ t') ∆ (s ∪ t)) < 4 * δ + calc μ ((s'' ∪ t') ∆ (s ∪ t)) + _ ≤ μ (s'' ∆ s ∪ t' ∆ t) := measure_mono (Set.union_symmDiff_union_subset ..) + _ ≤ μ (s'' ∆ s) + μ (t' ∆ t) := measure_union_le _ _ + _ < 3 * δ + δ := by gcongr + _ = 4 * δ := by ring + + + + - classical - have A (s : MeasuredSets μ) : Cauchy (map m₀ (𝓝[C'] s)) := by - have W := LipschitzOnWith.cauchySeq_comp - apply Metric.cauchy_iff.2 ⟨?_, ?_⟩ - · have : (𝓝[C'] s).NeBot := mem_closure_iff_nhdsWithin_neBot.mp (C'_dense s) - exact map_neBot - · intro ε εpos - simp - let m' (s : Set α) := if h : MeasurableSet s then limUnder (𝓝[C'] ⟨s, h⟩) (fun t ↦ m t) else 0 + let m' (s : Set α) := if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0 #exit From 65f1d97f28f07c2d54b88d600345fc5f4335eeaf Mon Sep 17 00:00:00 2001 From: sgouezel Date: Fri, 16 Jan 2026 18:20:45 +0100 Subject: [PATCH 3/8] start moving around --- Mathlib/Analysis/Normed/Group/Basic.lean | 20 +++++++- Mathlib/Data/Set/SymmDiff.lean | 17 ++++++- .../Topology/Instances/ENNReal/Lemmas.lean | 17 +++++++ Mathlib/test.lean | 51 ++++++------------- 4 files changed, 67 insertions(+), 38 deletions(-) diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean index 483d9411dc9825..150defff80cfa1 100644 --- a/Mathlib/Analysis/Normed/Group/Basic.lean +++ b/Mathlib/Analysis/Normed/Group/Basic.lean @@ -419,7 +419,7 @@ abbrev GroupNorm.toNormedCommGroup [CommGroup E] (f : GroupNorm E) : NormedCommG section SeminormedGroup variable [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {s : Set E} - {a a₁ a₂ b c : E} {r r₁ r₂ : ℝ} + {a a₁ a₂ b c d : E} {r r₁ r₂ : ℝ} @[to_additive] theorem dist_eq_norm_div (a b : E) : dist a b = ‖a / b‖ := @@ -495,6 +495,11 @@ theorem norm_mul_le_of_le' (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r @[to_additive norm_add₃_le /-- **Triangle inequality** for the norm. -/] lemma norm_mul₃_le' : ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ := norm_mul_le_of_le' (norm_mul_le' _ _) le_rfl +/-- **Triangle inequality** for the norm. -/ +@[to_additive norm_add₄_le /-- **Triangle inequality** for the norm. -/] +lemma norm_mul₄_le' : ‖a * b * c * d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ := + norm_mul_le_of_le' norm_mul₃_le' le_rfl + @[to_additive] lemma norm_div_le_norm_div_add_norm_div (a b c : E) : ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖ := by simpa only [dist_eq_norm_div] using dist_triangle a b c @@ -979,6 +984,19 @@ variable {E : Type*} [TopologicalSpace E] [ESeminormedMonoid E] @[to_additive enorm_add_le] lemma enorm_mul_le' (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ := ESeminormedMonoid.enorm_mul_le a b +@[to_additive enorm_add_le_of_le] +theorem enorm_mul_le_of_le' {r₁ r₂ : ℝ≥0∞} {a₁ a₂ : E} + (h₁ : ‖a₁‖ₑ ≤ r₁) (h₂ : ‖a₂‖ₑ ≤ r₂) : ‖a₁ * a₂‖ₑ ≤ r₁ + r₂ := + (enorm_mul_le' a₁ a₂).trans <| add_le_add h₁ h₂ + +@[to_additive enorm_add₃_le] +lemma enorm_mul₃_le' {a b c : E} : ‖a * b * c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ := + enorm_mul_le_of_le' (enorm_mul_le' _ _) le_rfl + +@[to_additive enorm_add₄_le] +lemma enorm_mul₄_le' {a b c d : E} : ‖a * b * c * d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ := + enorm_mul_le_of_le' enorm_mul₃_le' le_rfl + end ESeminormedMonoid section ENormedMonoid diff --git a/Mathlib/Data/Set/SymmDiff.lean b/Mathlib/Data/Set/SymmDiff.lean index db46c5baca62c7..6714ea826b7a69 100644 --- a/Mathlib/Data/Set/SymmDiff.lean +++ b/Mathlib/Data/Set/SymmDiff.lean @@ -17,7 +17,7 @@ assert_not_exists RelIso namespace Set universe u -variable {α : Type u} {a : α} {s t u : Set α} +variable {α : Type u} {a : α} {s t u v : Set α} open scoped symmDiff @@ -50,4 +50,19 @@ theorem subset_symmDiff_union_symmDiff_left (h : Disjoint s t) : u ⊆ s ∆ u theorem subset_symmDiff_union_symmDiff_right (h : Disjoint t u) : s ⊆ s ∆ t ∪ s ∆ u := h.le_symmDiff_sup_symmDiff_right +lemma union_symmDiff_subset : (s ∪ t) ∆ u ⊆ s ∆ u ∪ t ∆ u := by + intro x hx + simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ + grind + +lemma symmDiff_union_subset : s ∆ (t ∪ u) ⊆ s ∆ t ∪ s ∆ u := by + intro x hx + simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ + grind + +lemma union_symmDiff_union_subset : (s ∪ t) ∆ (u ∪ v) ⊆ s ∆ u ∪ t ∆ v := by + intro x hx + simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ + grind + end Set diff --git a/Mathlib/Topology/Instances/ENNReal/Lemmas.lean b/Mathlib/Topology/Instances/ENNReal/Lemmas.lean index 70207c765aecb6..44d159ff0ede65 100644 --- a/Mathlib/Topology/Instances/ENNReal/Lemmas.lean +++ b/Mathlib/Topology/Instances/ENNReal/Lemmas.lean @@ -1489,3 +1489,20 @@ theorem limsup_add_of_left_tendsto_zero {u : Filter ι} {f : ι → ℝ≥0∞} end LimsupLiminf end ENNReal -- namespace + +lemma Dense.lipschitzWith_extend {α β : Type*} + [PseudoEMetricSpace α] [EMetricSpace β] [CompleteSpace β] + {s : Set α} (hs : Dense s) {f : s → β} {K : ℝ≥0} (hf : LipschitzWith K f) : + LipschitzWith K (hs.extend f) := by + have : IsClosed {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by + have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous + apply isClosed_le (by fun_prop) + exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop) + have : Dense {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by + apply (hs.prod hs).mono + rintro ⟨x, y⟩ ⟨hx, hy⟩ + have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩ + have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩ + simp only [Set.mem_setOf_eq, Ax, Ay] + exact hf ⟨x, hx⟩ ⟨y, hy⟩ + simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq, Prod.forall] using this diff --git a/Mathlib/test.lean b/Mathlib/test.lean index 8cbdba5dfb893e..32c67506d8b32f 100644 --- a/Mathlib/test.lean +++ b/Mathlib/test.lean @@ -37,23 +37,6 @@ open scoped symmDiff Topology NNReal variable {α : Type*} [MeasurableSpace α] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] -lemma Set.union_symmDiff_subset {α : Type*} (a b c : Set α) : (a ∪ b) ∆ c ⊆ a ∆ c ∪ b ∆ c := by - intro x hx - simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ - grind - -lemma Set.symmDiff_union_subset {α : Type*} (a b c : Set α) : a ∆ (b ∪ c) ⊆ a ∆ b ∪ a ∆ c := by - intro x hx - simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ - grind - -lemma Set.union_symmDiff_union_subset {α : Type*} (a b c d : Set α) : - (a ∪ b) ∆ (c ∪ d) ⊆ a ∆ c ∪ b ∆ d := by - intro x hx - simp only [Set.mem_symmDiff, Set.mem_union] at hx ⊢ - grind - - namespace MeasureTheory set_option linter.unusedVariables false in @@ -112,23 +95,6 @@ lemma MeasuredSets.continuous_measure : Continuous (fun (s : MeasuredSets μ) _ ≤ μ x + ε := by gcongr -lemma _root_.Dense.lipschitzWith_extend {α β : Type*} - [PseudoEMetricSpace α] [MetricSpace β] [CompleteSpace β] - {s : Set α} (hs : Dense s) {f : s → β} {K : ℝ≥0} (hf : LipschitzWith K f) : - LipschitzWith K (hs.extend f) := by - have : IsClosed {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by - have : Continuous (hs.extend f) := (hs.uniformContinuous_extend hf.uniformContinuous).continuous - apply isClosed_le (by fun_prop) - exact (ENNReal.continuous_const_mul (by simp)).comp (by fun_prop) - have : Dense {p : α × α | edist (hs.extend f p.1) (hs.extend f p.2) ≤ K * edist p.1 p.2} := by - apply (hs.prod hs).mono - rintro ⟨x, y⟩ ⟨hx, hy⟩ - have Ax : hs.extend f x = f ⟨x, hx⟩ := hs.extend_eq hf.continuous ⟨x, hx⟩ - have Ay : hs.extend f y = f ⟨y, hy⟩ := hs.extend_eq hf.continuous ⟨y, hy⟩ - simp only [Set.mem_setOf_eq, Ax, Ay] - exact hf ⟨x, hx⟩ ⟨y, hy⟩ - simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq, Prod.forall] using this - open scoped ENNReal lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m : Set α → E) @@ -191,8 +157,8 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m contrapose! this exact ⟨‖m₁ ⟨s ∪ t, s.2.union t.2⟩ - (m₁ s + m₁ t)‖ₑ, this.bot_lt, le_of_eq (by abel_nf)⟩ intro ε εpos - obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ 16 * δ ≤ ε := by - refine ⟨ε / 16, (ENNReal.div_pos εpos.ne' (by simp)), le_of_eq ?_⟩ + obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ 8 * δ = ε := by + refine ⟨ε / 8, (ENNReal.div_pos εpos.ne' (by simp)), ?_⟩ exact ENNReal.mul_div_cancel (by simp) (by simp) obtain ⟨s', s'C, hs'⟩ : ∃ s' ∈ C, μ (s' ∆ s) < δ := h'C _ _ s.2 δpos obtain ⟨t', t'C, ht'⟩ : ∃ t' ∈ C, μ (t' ∆ t) < δ := h'C _ _ t.2 δpos @@ -241,6 +207,19 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m _ ≤ μ (s'' ∆ s) + μ (t' ∆ t) := measure_union_le _ _ _ < 3 * δ + δ := by gcongr _ = 4 * δ := by ring + calc ‖m₁ (⟨s ∪ t, s.2.union t.2⟩) - m₁ s - m₁ t‖ₑ + _ = ‖(m (s'' ∪ t') - m s'' - m t') + (m₁ ⟨s ∪ t, s.2.union t.2⟩ - m (s'' ∪ t')) + + (m s'' - m₁ s) + (m t' - m₁ t)‖ₑ := by abel_nf + _ ≤ ‖m (s'' ∪ t') - m s'' - m t'‖ₑ + ‖m₁ ⟨s ∪ t, s.2.union t.2⟩ - m (s'' ∪ t')‖ₑ + + ‖m s'' - m₁ s‖ₑ + ‖m t' - m₁ t‖ₑ := enorm_add₄_le + _ = ‖m₁ ⟨s ∪ t, s.2.union t.2⟩ - m (s'' ∪ t')‖ₑ + ‖m s'' - m₁ s‖ₑ + ‖m t' - m₁ t‖ₑ := by + rw [h'm _ s''C _ t'C Set.disjoint_sdiff_left] + simp + _ < 4 * δ + 3 * δ + δ := by + gcongr + rwa [enorm_sub_rev] + _ = 8 * δ := by ring + _ = ε := hδ From 523f05d29bde8ebd41af7ddf0403fa84dde61085 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Fri, 16 Jan 2026 20:03:38 +0100 Subject: [PATCH 4/8] long file --- Mathlib/Topology/Instances/ENNReal/Lemmas.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/Topology/Instances/ENNReal/Lemmas.lean b/Mathlib/Topology/Instances/ENNReal/Lemmas.lean index 44d159ff0ede65..a65ddae563677b 100644 --- a/Mathlib/Topology/Instances/ENNReal/Lemmas.lean +++ b/Mathlib/Topology/Instances/ENNReal/Lemmas.lean @@ -1506,3 +1506,5 @@ lemma Dense.lipschitzWith_extend {α β : Type*} simp only [Set.mem_setOf_eq, Ax, Ay] exact hf ⟨x, hx⟩ ⟨y, hy⟩ simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq, Prod.forall] using this + +set_option linter.style.longFile 1700 From 45a5116a60417e761e77f8c368d8471c4776ee3f Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sat, 17 Jan 2026 20:58:04 +0100 Subject: [PATCH 5/8] progress --- .../BigOperators/Group/Finset/Basic.lean | 24 ++ .../ProjectiveFamilyContent.lean | 2 +- Mathlib/MeasureTheory/Measure/AddContent.lean | 245 ++++++++++++------ .../OuterMeasure/OfAddContent.lean | 20 +- .../Kernel/IonescuTulcea/Traj.lean | 2 +- Mathlib/Probability/ProductMeasure.lean | 2 +- Mathlib/test.lean | 170 ++++++++++-- 7 files changed, 358 insertions(+), 107 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean index 83750ccb4074b1..97ff53b528cc5b 100644 --- a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean @@ -383,6 +383,30 @@ lemma prod_congr_of_eq_on_inter {ι M : Type*} {s₁ s₂ : Finset ι} {f g : ι conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm] exact prod_congr rfl (by simpa) +/-- If a function `g` is injective on `s`, except for some points where `f (g i) = 1`, then +the product of `f (g x)` over `s` equals the product of `f i` over the image of `s`. -/ +@[to_additive /-- If a function `g` is injective on `s`, except for some points +where `f (g i) = 0`, then the sum of `f (g x)` over `s` equals the sum of `f i` over the +image of `s`. -/] +theorem prod_image_of_apply_eq_one_of_eq [DecidableEq ι] {s : Finset κ} {g : κ → ι} + (hg : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → g i = g j → f (g i) = 1) : + ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) := by + classical + let s' : Finset κ := s.filter (fun i ↦ f (g i) ≠ 1) + have : ∏ x ∈ s, f (g x) = ∏ x ∈ s', f (g x) := by + apply Finset.prod_congr_of_eq_on_inter <;> simp +contextual [s'] + rw [this, ← prod_image (s := s')]; swap + · intro i hi j hj hij + simp only [ne_eq, coe_filter, Set.mem_setOf_eq, s'] at hi hj + contrapose! hg + exact ⟨i, hi.1, j, hj.1, hg, hij, hi.2⟩ + apply Finset.prod_congr_of_eq_on_inter + · simp +contextual [s'] + grind + · simp +contextual [s'] + grind + · simp + @[to_additive] theorem prod_eq_mul_of_mem {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : ∏ x ∈ s, f x = f a * f b := by diff --git a/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean b/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean index 654ce0afacdead..f9e4887a03e313 100644 --- a/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean +++ b/Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean @@ -115,7 +115,7 @@ section ProjectiveFamilyContent cylinders, by setting `projectiveFamilyContent s = P I S` for `s = cylinder I S`, where `I` is a finite set of indices and `S` is a measurable set in `Π i : I, α i`. -/ noncomputable def projectiveFamilyContent (hP : IsProjectiveMeasureFamily P) : - AddContent (measurableCylinders α) := + AddContent ℝ≥0∞ (measurableCylinders α) := isSetRing_measurableCylinders.addContent_of_union (projectiveFamilyFun P) (projectiveFamilyFun_empty hP) (projectiveFamilyFun_union hP) diff --git a/Mathlib/MeasureTheory/Measure/AddContent.lean b/Mathlib/MeasureTheory/Measure/AddContent.lean index e0a06cdec41a4b..3f17d974e41961 100644 --- a/Mathlib/MeasureTheory/Measure/AddContent.lean +++ b/Mathlib/MeasureTheory/Measure/AddContent.lean @@ -62,30 +62,32 @@ open scoped ENNReal Topology Function namespace MeasureTheory variable {α : Type*} {C : Set (Set α)} {s t : Set α} {I : Finset (Set α)} +{G : Type*} [AddCommMonoid G] +variable (G) in /-- An additive content is a set function with value 0 at the empty set which is finitely additive on a given set of sets. -/ structure AddContent (C : Set (Set α)) where /-- The value of the content on a set. -/ - toFun : Set α → ℝ≥0∞ + toFun : Set α → G empty' : toFun ∅ = 0 sUnion' (I : Finset (Set α)) (_h_ss : ↑I ⊆ C) (_h_dis : PairwiseDisjoint (I : Set (Set α)) id) (_h_mem : ⋃₀ ↑I ∈ C) : toFun (⋃₀ I) = ∑ u ∈ I, toFun u -instance : Inhabited (AddContent C) := +instance : Inhabited (AddContent G C) := ⟨{toFun := fun _ => 0 empty' := by simp sUnion' := by simp }⟩ -instance : FunLike (AddContent C) (Set α) ℝ≥0∞ where +instance : FunLike (AddContent G C) (Set α) G where coe m s := m.toFun s coe_injective' m m' _ := by cases m cases m' congr -variable {m m' : AddContent C} +variable {m m' : AddContent G C} @[ext] protected lemma AddContent.ext (h : ∀ s, m s = m' s) : m = m' := DFunLike.ext _ _ h @@ -97,6 +99,26 @@ lemma addContent_sUnion (h_ss : ↑I ⊆ C) m (⋃₀ I) = ∑ u ∈ I, m u := m.sUnion' I h_ss h_dis h_mem +lemma addContent_biUnion {ι : Type*} {a : Finset ι} {f : ι → Set α} (hf : ∀ i ∈ a, f i ∈ C) + (h_dis : PairwiseDisjoint ↑a f) (h_mem : ⋃ i ∈ a, f i ∈ C) : + m (⋃ i ∈ a, f i) = ∑ i ∈ a, m (f i) := by + classical + let b : Finset (Set α) := Finset.image f a + have A : ⋃ i ∈ a, f i = ⋃₀ b := by simp [b] + rw [A, addContent_sUnion]; rotate_left + · simp [b]; grind + · intro s hs t ht hst + simp only [coe_image, Set.mem_image, SetLike.mem_coe, b] at hs ht + rcases hs with ⟨i, hi, rfl⟩ + rcases ht with ⟨j, hj, rfl⟩ + exact h_dis hi hj (by grind) + · rwa [← A] + simp only [b] + rw [Finset.sum_image_of_apply_eq_one_of_eq] + intro i hi j hj hij + contrapose! hij + exact (h_dis hi hj hij).ne (H i hi).ne_empty + lemma addContent_union' (hs : s ∈ C) (ht : t ∈ C) (hst : s ∪ t ∈ C) (h_dis : Disjoint s t) : m (s ∪ t) = m s + m t := by by_cases hs_empty : s = ∅ @@ -118,9 +140,9 @@ lemma addContent_union' (hs : s ∈ C) (ht : t ∈ C) (hst : s ∪ t ∈ C) (h_d rw [← hs_eq_t] at h_dis exact Disjoint.eq_bot_of_self h_dis -/-- An additive content is said to be sigma-sub-additive if for any sequence of sets `f` in `C` such -that `⋃ i, f i ∈ C`, we have `m (⋃ i, f i) ≤ ∑' i, m (f i)`. -/ -def AddContent.IsSigmaSubadditive (m : AddContent C) : Prop := +/-- An additive content with values in `ℝ≥0∞` is said to be sigma-sub-additive if for any sequence +of sets `f` in `C` such that `⋃ i, f i ∈ C`, we have `m (⋃ i, f i) ≤ ∑' i, m (f i)`. -/ +def AddContent.IsSigmaSubadditive (m : AddContent ℝ≥0∞ C) : Prop := ∀ ⦃f : ℕ → Set α⦄ (_hf : ∀ i, f i ∈ C) (_hf_Union : (⋃ i, f i) ∈ C), m (⋃ i, f i) ≤ ∑' i, m (f i) section IsSetSemiring @@ -140,6 +162,92 @@ lemma addContent_eq_add_disjointOfDiffUnion_of_subset (hC : IsSetSemiring C) exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis · rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss] +/-- For an `m : addContent C` on a `SetSemiring C` and `s t : Set α` with `s ⊆ t`, we can write +`m t = m s + ∑ i in hC.disjointOfDiff ht hs, m i`. -/ +theorem eq_add_disjointOfDiff_of_subset (hC : IsSetSemiring C) + (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) : + m t = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i := by + classical + conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst] + rw [← coe_insert, addContent_sUnion] + · rw [sum_insert] + exact hC.notMem_disjointOfDiff ht hs + · rw [coe_insert] + exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs) + · rw [coe_insert] + exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs + · rw [coe_insert] + rwa [hC.sUnion_insert_disjointOfDiff ht hs hst] + +/-- If a set can be written in two different ways as a disjoint union of elements of a semi-ring +of sets `C`, then the sums of the values of `m : addContent C` along the two decompositions give +the same result. +In other words, `m` can be canonically extended to finite unions of elements of `C`. -/ +theorem sum_addContent_eq_of_sUnion_eq (hC : IsSetSemiring C) (J J' : Finset (Set α)) + (hJ : ↑J ⊆ C) (hJdisj : PairwiseDisjoint (J : Set (Set α)) id) + (hJ' : ↑J' ⊆ C) (hJ'disj : PairwiseDisjoint (J' : Set (Set α)) id) + (h : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ↑J') : + ∑ s ∈ J, m s = ∑ t ∈ J', m t := by + calc ∑ s ∈ J, m s + _ = ∑ s ∈ J, (∑ t ∈ J', m (s ∩ t)) := by + apply Finset.sum_congr rfl (fun s hs ↦ ?_) + have : s = ⋃ t ∈ J', s ∩ t := by + apply Set.Subset.antisymm _ (by simp) + intro x hx + have A : x ∈ ⋃₀ ↑J' := by + rw [← h] + simp only [mem_sUnion, SetLike.mem_coe] + exact ⟨s, hs, hx⟩ + simpa [mem_iUnion, mem_inter_iff, exists_and_left, exists_prop, hx] using A + nth_rewrite 1 [this] + apply addContent_biUnion + · exact fun t ht ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht) + · exact fun i hi j hj hij ↦ (hJ'disj hi hj hij).mono (by simp) (by simp) + · rw [← this] + exact hJ hs + _ = ∑ t ∈ J', (∑ s ∈ J, m (s ∩ t)) := sum_comm + _ = ∑ t ∈ J', m t := by + apply Finset.sum_congr rfl (fun t ht ↦ ?_) + have : t = ⋃ s ∈ J, s ∩ t := by + apply Set.Subset.antisymm _ (by simp) + intro x hx + have A : x ∈ ⋃₀ ↑J := by + rw [h] + simp only [mem_sUnion, SetLike.mem_coe] + exact ⟨t, ht, hx⟩ + simpa [mem_iUnion, mem_inter_iff, exists_and_left, exists_prop, hx] using A + nth_rewrite 2 [this] + apply (addContent_biUnion _ _ _).symm + · exact fun s hs ↦ hC.inter_mem _ (hJ hs) _ (hJ' ht) + · exact fun i hi j hj hij ↦ (hJdisj hi hj hij).mono (by simp) (by simp) + · rw [← this] + exact hJ' ht + +open scoped Classical in +noncomputable def AddContent.extendUnion (m : AddContent G C) (s : Set α) : G := + if h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J + then ∑ s ∈ h.choose, m s + else 0 + +lemma AddContent.extendUnion_eq (hC : IsSetSemiring C) + {m : AddContent G C} {s : Set α} {J : Finset (Set α)} + (hJ : ↑J ⊆ C) (h'J : PairwiseDisjoint (J : Set (Set α)) id) (hs : s = ⋃₀ ↑J) : + m.extendUnion s = ∑ s ∈ J, m s := by + have h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J := + ⟨J, hJ, h'J, hs⟩ + simp only [extendUnion, h, ↓reduceDIte] + apply sum_addContent_eq_of_sUnion_eq hC + · exact h.choose_spec.1 + · exact h.choose_spec.2.1 + · exact hJ + + +#exit + + + +variable [PartialOrder G] [CanonicallyOrderedAdd G] + /-- For an `m : addContent C` on a `SetSemiring C`, if `I` is a `Finset` of pairwise disjoint sets in `C` and `⋃₀ I ⊆ t` for `t ∈ C`, then `∑ s ∈ I, m s ≤ m t`. -/ lemma sum_addContent_le_of_subset (hC : IsSetSemiring C) @@ -160,25 +268,8 @@ lemma addContent_mono (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) · simp only [coe_singleton, pairwiseDisjoint_singleton] · simp [hst] -/-- For an `m : addContent C` on a `SetSemiring C` and `s t : Set α` with `s ⊆ t`, we can write -`m t = m s + ∑ i in hC.disjointOfDiff ht hs, m i`. -/ -theorem eq_add_disjointOfDiff_of_subset (hC : IsSetSemiring C) - (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) : - m t = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i := by - classical - conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst] - rw [← coe_insert, addContent_sUnion] - · rw [sum_insert] - exact hC.notMem_disjointOfDiff ht hs - · rw [coe_insert] - exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs) - · rw [coe_insert] - exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs - · rw [coe_insert] - rwa [hC.sUnion_insert_disjointOfDiff ht hs hst] - /-- An `addContent C` on a `SetSemiring C` is sub-additive. -/ -lemma addContent_sUnion_le_sum {m : AddContent C} (hC : IsSetSemiring C) +lemma addContent_sUnion_le_sum {m : AddContent G C} (hC : IsSetSemiring C) (J : Finset (Set α)) (h_ss : ↑J ⊆ C) (h_mem : ⋃₀ ↑J ∈ C) : m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u := by classical @@ -202,7 +293,7 @@ lemma addContent_sUnion_le_sum {m : AddContent C} (hC : IsSetSemiring C) · simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe] at * exact h3.symm ▸ h_mem -lemma addContent_le_sum_of_subset_sUnion {m : AddContent C} (hC : IsSetSemiring C) +lemma addContent_le_sum_of_subset_sUnion {m : AddContent G C} (hC : IsSetSemiring C) {J : Finset (Set α)} (h_ss : ↑J ⊆ C) (ht : t ∈ C) (htJ : t ⊆ ⋃₀ ↑J) : m t ≤ ∑ u ∈ J, m u := by -- we can't apply `addContent_mono` and `addContent_sUnion_le_sum` because `⋃₀ ↑J` might not @@ -223,7 +314,7 @@ lemma addContent_le_sum_of_subset_sUnion {m : AddContent C} (hC : IsSetSemiring exact addContent_mono hC (hC.inter_mem _ ht _ (h_ss hu)) (h_ss hu) inter_subset_right /-- If an `AddContent` is σ-subadditive on a semi-ring of sets, then it is σ-additive. -/ -theorem addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le {m : AddContent C} +theorem addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le {m : AddContent ℝ≥0∞ C} (hC : IsSetSemiring C) -- TODO: `m_subadd` is in fact equivalent to `m.IsSigmaSubadditive`. (m_subadd : ∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : ⋃ i, f i ∈ C) @@ -251,7 +342,7 @@ theorem addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le {m : AddCo exact fun i _ ↦ subset_iUnion _ i /-- If an `AddContent` is σ-subadditive on a semi-ring of sets, then it is σ-additive. -/ -theorem addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive {m : AddContent C} +theorem addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive {m : AddContent ℝ≥0∞ C} (hC : IsSetSemiring C) (m_subadd : m.IsSigmaSubadditive) (f : ℕ → Set α) (hf : ∀ i, f i ∈ C) (hf_Union : (⋃ i, f i) ∈ C) (hf_disj : Pairwise (Disjoint on f)) : @@ -266,7 +357,7 @@ section AddContentExtend /-- An additive content obtained from another one on the same semiring of sets by setting the value of each set not in the semiring at `∞`. -/ protected noncomputable -def AddContent.extend (hC : IsSetSemiring C) (m : AddContent C) : AddContent C where +def AddContent.extend (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) : AddContent ℝ≥0∞ C where toFun := extend (fun x (_ : x ∈ C) ↦ m x) empty' := by rw [extend_eq, addContent_empty]; exact hC.empty_mem sUnion' I h_ss h_dis h_mem := by @@ -277,14 +368,15 @@ def AddContent.extend (hC : IsSetSemiring C) (m : AddContent C) : AddContent C w rw [extend_eq] exact h_ss hs -protected theorem AddContent.extend_eq_extend (hC : IsSetSemiring C) (m : AddContent C) : +protected theorem AddContent.extend_eq_extend (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) : m.extend hC = extend (fun x (_ : x ∈ C) ↦ m x) := rfl -protected theorem AddContent.extend_eq (hC : IsSetSemiring C) (m : AddContent C) (hs : s ∈ C) : +protected theorem AddContent.extend_eq (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) (hs : s ∈ C) : m.extend hC s = m s := by rwa [m.extend_eq_extend, extend_eq] -protected theorem AddContent.extend_eq_top (hC : IsSetSemiring C) (m : AddContent C) (hs : s ∉ C) : +protected theorem AddContent.extend_eq_top + (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) (hs : s ∉ C) : m.extend hC s = ∞ := by rwa [m.extend_eq_extend, extend_eq_top] @@ -297,26 +389,6 @@ lemma addContent_union (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) m (s ∪ t) = m s + m t := addContent_union' hs ht (hC.union_mem hs ht) h_dis -lemma addContent_union_le (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : - m (s ∪ t) ≤ m s + m t := by - rw [← union_diff_self, addContent_union hC hs (hC.diff_mem ht hs)] - · exact add_le_add le_rfl - (addContent_mono hC.isSetSemiring (hC.diff_mem ht hs) ht diff_subset) - · rw [Set.disjoint_iff_inter_eq_empty, inter_diff_self] - -lemma addContent_biUnion_le {ι : Type*} (hC : IsSetRing C) {s : ι → Set α} - {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C) : - m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i) := by - classical - induction S using Finset.induction with - | empty => simp - | insert i S hiS h => - rw [Finset.sum_insert hiS] - simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert] - simp only [Finset.mem_insert, forall_eq_or_imp] at hs - refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_ - exact add_le_add le_rfl (h hs.2) - lemma addContent_biUnion_eq {ι : Type*} (hC : IsSetRing C) {s : ι → Set α} {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C) (hS : (S : Set ι).PairwiseDisjoint s) : m (⋃ i ∈ S, s i) = ∑ i ∈ S, m (s i) := by @@ -333,24 +405,7 @@ lemma addContent_biUnion_eq {ι : Type*} (hC : IsSetRing C) {s : ι → Set α} rw [disjoint_iUnion₂_right] exact fun j hjS ↦ hS.2 j hjS (ne_of_mem_of_not_mem hjS hiS).symm -lemma le_addContent_diff (m : AddContent C) (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : - m s - m t ≤ m (s \ t) := by - conv_lhs => rw [← inter_union_diff s t] - rw [addContent_union hC (hC.inter_mem hs ht) (hC.diff_mem hs ht) disjoint_inf_sdiff, add_comm] - refine add_tsub_le_assoc.trans_eq ?_ - rw [tsub_eq_zero_of_le - (addContent_mono hC.isSetSemiring (hC.inter_mem hs ht) ht inter_subset_right), add_zero] - -lemma addContent_diff_of_ne_top (m : AddContent C) (hC : IsSetRing C) - (hm_ne_top : ∀ s ∈ C, m s ≠ ∞) - {s t : Set α} (hs : s ∈ C) (ht : t ∈ C) (hts : t ⊆ s) : - m (s \ t) = m s - m t := by - have h_union : m (t ∪ s \ t) = m t + m (s \ t) := - addContent_union hC ht (hC.diff_mem hs ht) disjoint_sdiff_self_right - simp_rw [Set.union_diff_self, Set.union_eq_right.mpr hts] at h_union - rw [h_union, ENNReal.add_sub_cancel_left (hm_ne_top _ ht)] - -lemma addContent_accumulate (m : AddContent C) (hC : IsSetRing C) +lemma addContent_accumulate (m : AddContent G C) (hC : IsSetRing C) {s : ℕ → Set α} (hs_disj : Pairwise (Disjoint on s)) (hsC : ∀ i, s i ∈ C) (n : ℕ) : m (Set.accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i) := by induction n with @@ -362,9 +417,9 @@ lemma addContent_accumulate (m : AddContent C) (hC : IsSetRing C) /-- A function which is additive on disjoint elements in a ring of sets `C` defines an additive content on `C`. -/ -def IsSetRing.addContent_of_union (m : Set α → ℝ≥0∞) (hC : IsSetRing C) (m_empty : m ∅ = 0) +def IsSetRing.addContent_of_union (m : Set α → G) (hC : IsSetRing C) (m_empty : m ∅ = 0) (m_add : ∀ {s t : Set α} (_hs : s ∈ C) (_ht : t ∈ C), Disjoint s t → m (s ∪ t) = m s + m t) : - AddContent C where + AddContent G C where toFun := m empty' := m_empty sUnion' I h_ss h_dis h_mem := by @@ -385,10 +440,49 @@ def IsSetRing.addContent_of_union (m : Set α → ℝ≥0∞) (hC : IsSetRing C) Finset.sum_insert hsI, h h_ss.2 h_dis.1] rwa [Set.sUnion_insert] at h_mem +variable [PartialOrder G] [CanonicallyOrderedAdd G] + +lemma addContent_union_le (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : + m (s ∪ t) ≤ m s + m t := by + rw [← union_diff_self, addContent_union hC hs (hC.diff_mem ht hs)] + · exact add_le_add le_rfl + (addContent_mono hC.isSetSemiring (hC.diff_mem ht hs) ht diff_subset) + · rw [Set.disjoint_iff_inter_eq_empty, inter_diff_self] + +lemma addContent_biUnion_le {ι : Type*} (hC : IsSetRing C) {s : ι → Set α} + {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C) : + m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i) := by + classical + induction S using Finset.induction with + | empty => simp + | insert i S hiS h => + rw [Finset.sum_insert hiS] + simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert] + simp only [Finset.mem_insert, forall_eq_or_imp] at hs + refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_ + exact add_le_add le_rfl (h hs.2) + +lemma le_addContent_diff (m : AddContent ℝ≥0∞ C) (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : + m s - m t ≤ m (s \ t) := by + conv_lhs => rw [← inter_union_diff s t] + rw [addContent_union hC (hC.inter_mem hs ht) (hC.diff_mem hs ht) disjoint_inf_sdiff, add_comm] + refine add_tsub_le_assoc.trans_eq ?_ + rw [tsub_eq_zero_of_le + (addContent_mono hC.isSetSemiring (hC.inter_mem hs ht) ht inter_subset_right), add_zero] + +lemma addContent_diff_of_ne_top (m : AddContent ℝ≥0∞ C) (hC : IsSetRing C) + (hm_ne_top : ∀ s ∈ C, m s ≠ ∞) + {s t : Set α} (hs : s ∈ C) (ht : t ∈ C) (hts : t ⊆ s) : + m (s \ t) = m s - m t := by + have h_union : m (t ∪ s \ t) = m t + m (s \ t) := + addContent_union hC ht (hC.diff_mem hs ht) disjoint_sdiff_self_right + simp_rw [Set.union_diff_self, Set.union_eq_right.mpr hts] at h_union + rw [h_union, ENNReal.add_sub_cancel_left (hm_ne_top _ ht)] + /-- In a ring of sets, continuity of an additive content at `∅` implies σ-additivity. This is not true in general in semirings, or without the hypothesis that `m` is finite. See the examples 7 and 8 in Halmos' book Measure Theory (1974), page 40. -/ -theorem addContent_iUnion_eq_sum_of_tendsto_zero (hC : IsSetRing C) (m : AddContent C) +theorem addContent_iUnion_eq_sum_of_tendsto_zero (hC : IsSetRing C) (m : AddContent ℝ≥0∞ C) (hm_ne_top : ∀ s ∈ C, m s ≠ ∞) (hm_tendsto : ∀ ⦃s : ℕ → Set α⦄ (_ : ∀ n, s n ∈ C), Antitone s → (⋂ n, s n) = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)) @@ -419,7 +513,8 @@ theorem addContent_iUnion_eq_sum_of_tendsto_zero (hC : IsSetRing C) (m : AddCont /-- If an additive content is σ-additive on a set ring, then the content of a monotone sequence of sets tends to the content of the union. -/ -theorem tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum (hC : IsSetRing C) +theorem tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum + {m : AddContent ℝ≥0∞ C} (hC : IsSetRing C) (m_iUnion : ∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : (⋃ i, f i) ∈ C) (_hf_disj : Pairwise (Disjoint on f)), m (⋃ i, f i) = ∑' i, m (f i)) ⦃f : ℕ → Set α⦄ (hf_mono : Monotone f) (hf : ∀ i, f i ∈ C) (hf_Union : ⋃ i, f i ∈ C) : @@ -435,7 +530,7 @@ theorem tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum (hC : IsSet exact ENNReal.tendsto_nat_tsum _ /-- If an additive content is σ-additive on a set ring, then it is σ-subadditive. -/ -theorem isSigmaSubadditive_of_addContent_iUnion_eq_tsum (hC : IsSetRing C) +theorem isSigmaSubadditive_of_addContent_iUnion_eq_tsum {m : AddContent ℝ≥0∞ C} (hC : IsSetRing C) (m_iUnion : ∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : (⋃ i, f i) ∈ C) (_hf_disj : Pairwise (Disjoint on f)), m (⋃ i, f i) = ∑' i, m (f i)) : m.IsSigmaSubadditive := by diff --git a/Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean b/Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean index 4487308b3f3e34..fefaacfe9ab7dd 100644 --- a/Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean +++ b/Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean @@ -52,7 +52,7 @@ variable {α : Type*} {C : Set (Set α)} {s : Set α} /-- For `m : AddContent C` sigma-sub-additive, finite on `C`, the `OuterMeasure` given by `m` coincides with `m` on `C`. -/ -theorem ofFunction_eq (hC : IsSetSemiring C) (m : AddContent C) +theorem ofFunction_eq (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) (m_sigma_subadd : m.IsSigmaSubadditive) (m_top : ∀ s ∉ C, m s = ∞) (hs : s ∈ C) : OuterMeasure.ofFunction m addContent_empty s = m s := by refine le_antisymm (OuterMeasure.ofFunction_le s) ?_ @@ -69,7 +69,7 @@ theorem ofFunction_eq (hC : IsSetSemiring C) (m : AddContent C) /-- For `m : AddContent C` sigma-sub-additive, finite on `C`, the `inducedOuterMeasure` given by `m` coincides with `m` on `C`. -/ -theorem inducedOuterMeasure_eq (hC : IsSetSemiring C) (m : AddContent C) +theorem inducedOuterMeasure_eq (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) : inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m s := by suffices inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m.extend hC s by @@ -83,7 +83,7 @@ theorem inducedOuterMeasure_eq (hC : IsSetSemiring C) (m : AddContent C) rw [m.extend_eq hC (hf i)] · exact fun _ ↦ m.extend_eq_top _ -theorem isCaratheodory_ofFunction_of_mem (hC : IsSetSemiring C) (m : AddContent C) +theorem isCaratheodory_ofFunction_of_mem (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) (m_top : ∀ s ∉ C, m s = ∞) (hs : s ∈ C) : (OuterMeasure.ofFunction m addContent_empty).IsCaratheodory s := by rw [OuterMeasure.isCaratheodory_iff_le'] @@ -117,12 +117,12 @@ theorem isCaratheodory_ofFunction_of_mem (hC : IsSetSemiring C) (m : AddContent /-- Every `s ∈ C` for an `m : AddContent C` with `IsSetSemiring C` is Carathéodory measurable with respect to the `inducedOuterMeasure` from `m`. -/ -theorem isCaratheodory_inducedOuterMeasure_of_mem (hC : IsSetSemiring C) (m : AddContent C) +theorem isCaratheodory_inducedOuterMeasure_of_mem (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) {s : Set α} (hs : s ∈ C) : (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s := isCaratheodory_ofFunction_of_mem hC (m.extend hC) (fun _ ↦ m.extend_eq_top hC) hs -theorem isCaratheodory_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent C) +theorem isCaratheodory_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) (s : Set α) (hs : MeasurableSet[MeasurableSpace.generateFrom C] s) : (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).IsCaratheodory s := by induction hs with @@ -133,7 +133,7 @@ theorem isCaratheodory_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddConten /-- Construct a measure from a sigma-subadditive content on a semiring. This measure is defined on the associated Carathéodory sigma-algebra. -/ -noncomputable def measureCaratheodory (m : AddContent C) (hC : IsSetSemiring C) +noncomputable def measureCaratheodory (m : AddContent ℝ≥0∞ C) (hC : IsSetSemiring C) (m_sigma_subadd : m.IsSigmaSubadditive) : @Measure α (inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty).caratheodory := letI : MeasurableSpace α := @@ -150,19 +150,19 @@ noncomputable def measureCaratheodory (m : AddContent C) (hC : IsSetSemiring C) /-- The measure `MeasureTheory.AddContent.measureCaratheodory` generated from an `m : AddContent C` on a `IsSetSemiring C` coincides with the `MeasureTheory.inducedOuterMeasure`. -/ -theorem measureCaratheodory_eq_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent C) +theorem measureCaratheodory_eq_inducedOuterMeasure (hC : IsSetSemiring C) (m : AddContent ℝ≥0∞ C) (m_sigma_subadd : m.IsSigmaSubadditive) : m.measureCaratheodory hC m_sigma_subadd s = inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s := rfl -theorem measureCaratheodory_eq (m : AddContent C) (hC : IsSetSemiring C) +theorem measureCaratheodory_eq (m : AddContent ℝ≥0∞ C) (hC : IsSetSemiring C) (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) : m.measureCaratheodory hC m_sigma_subadd s = m s := m.inducedOuterMeasure_eq hC m_sigma_subadd hs /-- Construct a measure from a sigma-subadditive content on a semiring, assuming the semiring generates a given measurable structure. The measure is defined on this measurable structure. -/ -noncomputable def measure [mα : MeasurableSpace α] (m : AddContent C) (hC : IsSetSemiring C) +noncomputable def measure [mα : MeasurableSpace α] (m : AddContent ℝ≥0∞ C) (hC : IsSetSemiring C) (hC_gen : mα ≤ MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive) : Measure α := (m.measureCaratheodory hC m_sigma_subadd).trim <| @@ -170,7 +170,7 @@ noncomputable def measure [mα : MeasurableSpace α] (m : AddContent C) (hC : Is /-- The measure defined through a sigma-subadditive content on a semiring coincides with the content on the semiring. -/ -theorem measure_eq [mα : MeasurableSpace α] (m : AddContent C) (hC : IsSetSemiring C) +theorem measure_eq [mα : MeasurableSpace α] (m : AddContent ℝ≥0∞ C) (hC : IsSetSemiring C) (hC_gen : mα = MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive) (hs : s ∈ C) : m.measure hC hC_gen.le m_sigma_subadd s = m s := by diff --git a/Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean b/Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean index eb2cf701e3bb52..8a8f0c8d290f7c 100644 --- a/Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean +++ b/Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean @@ -228,7 +228,7 @@ lemma isProjectiveMeasureFamily_partialTraj {a : ℕ} (x₀ : Π i : Iic a, X i) trajectory up to time `a` we can construct an additive content over cylinders. It corresponds to composing the kernels, starting at time `a + 1`. -/ noncomputable def trajContent {a : ℕ} (x₀ : Π i : Iic a, X i) : - AddContent (measurableCylinders X) := + AddContent ℝ≥0∞ (measurableCylinders X) := projectiveFamilyContent (isProjectiveMeasureFamily_partialTraj κ x₀) variable {κ} diff --git a/Mathlib/Probability/ProductMeasure.lean b/Mathlib/Probability/ProductMeasure.lean index 9559f07f26ffe8..403357a736c382 100644 --- a/Mathlib/Probability/ProductMeasure.lean +++ b/Mathlib/Probability/ProductMeasure.lean @@ -74,7 +74,7 @@ lemma isProjectiveMeasureFamily_pi : /-- Consider a family of probability measures. You can take their products for any finite subfamily. This gives an additive content on the measurable cylinders. -/ -noncomputable def piContent : AddContent (measurableCylinders X) := +noncomputable def piContent : AddContent ℝ≥0∞ (measurableCylinders X) := projectiveFamilyContent (isProjectiveMeasureFamily_pi μ) lemma piContent_cylinder {I : Finset ι} {S : Set (Π i : I, X i)} (hS : MeasurableSet S) : diff --git a/Mathlib/test.lean b/Mathlib/test.lean index 32c67506d8b32f..e9b08a810fafa2 100644 --- a/Mathlib/test.lean +++ b/Mathlib/test.lean @@ -34,7 +34,7 @@ des intervalles semi-ouverts. Alors 3. est satisfait. open Filter open scoped symmDiff Topology NNReal -variable {α : Type*} [MeasurableSpace α] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] +variable {α : Type*} [MeasurableSpace α] {E : Type*} [NormedAddCommGroup E] [CompleteSpace E] namespace MeasureTheory @@ -97,19 +97,82 @@ lemma MeasuredSets.continuous_measure : Continuous (fun (s : MeasuredSets μ) open scoped ENNReal -lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m : Set α → E) - (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) - (h'm : ∀ s ∈ C, ∀ t ∈ C, Disjoint s t → m (s ∪ t) = m s + m t) - (hC_diff : ∀ s ∈ C, ∀ t ∈ C, s \ t ∈ C) +/-- A finitely additive vector measure which is dominated by a finite positive measure is in +fact countably additive. -/ +def VectorMeasure.of_additive_of_le_measure + (m : Set α → E) (hm : ∀ s, ‖m s‖ₑ ≤ μ s) [IsFiniteMeasure μ] + (h'm : ∀ s t, MeasurableSet s → MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) + (h''m : ∀ s, ¬ MeasurableSet s → m s = 0) : VectorMeasure α E where + measureOf' := m + empty' := by simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp) + not_measurable' := h''m + m_iUnion' f f_meas f_disj := by + rw [hasSum_iff_tendsto_nat_of_summable_norm]; swap + · simp only [← toReal_enorm] + apply ENNReal.summable_toReal + apply ne_of_lt + calc ∑' i, ‖m (f i)‖ₑ + _ ≤ ∑' i, μ (f i) := by gcongr; apply hm + _ = μ (⋃ i, f i) := (measure_iUnion f_disj f_meas).symm + _ < ⊤ := measure_lt_top μ (⋃ i, f i) + apply tendsto_iff_norm_sub_tendsto_zero.2 + simp_rw [norm_sub_rev, ← toReal_enorm, ← ENNReal.toReal_zero] + apply (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp + have A n : m (⋃ i ∈ Finset.range n, f i) = ∑ i ∈ Finset.range n, m (f i) := by + induction n with + | zero => simpa using h'm ∅ ∅ MeasurableSet.empty MeasurableSet.empty (by simp) + | succ n ih => + simp only [Finset.range_add_one] + rw [Finset.sum_insert (by simp)] + simp only [Finset.mem_insert, Set.iUnion_iUnion_eq_or_left] + rw [h'm _ _ (f_meas n), ih] + · exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i) + · simp only [Finset.mem_range, Set.disjoint_iUnion_right] + intro i hi + exact f_disj hi.ne' + have B n : m (⋃ i, f i) = m (⋃ i ∈ Finset.range n, f i) + m (⋃ i ∈ Set.Ici n, f i) := by + have : ⋃ i, f i = (⋃ i ∈ Finset.range n, f i) ∪ (⋃ i ∈ Set.Ici n, f i) := by + ext; simp; grind + rw [this] + apply h'm + · exact Finset.measurableSet_biUnion _ (fun i hi ↦ f_meas i) + · exact MeasurableSet.biUnion (Set.to_countable _) (fun i hi ↦ f_meas i) + · simp only [Finset.mem_range, Set.mem_Ici, Set.disjoint_iUnion_right, + Set.disjoint_iUnion_left] + intro i hi j hj + exact f_disj (hj.trans_le hi).ne + have C n : m (⋃ i, f i) - ∑ i ∈ Finset.range n, m (f i) = m (⋃ i ∈ Set.Ici n, f i) := by + rw [B n, A]; simp + simp only [C] + apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds + (h := fun n ↦ μ (⋃ i ∈ Set.Ici n, f i)) ?_ (fun i ↦ bot_le) (fun i ↦ hm _) + exact tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint + (fun i ↦ (f_meas i).nullMeasurableSet) f_disj + +/-- Consider a finitely additive vector measure on a dense class of measurable sets which is stable +under binary intersection, union and complement. Assume that it is dominated by a finite positive +measure. Then it extends to a countably additive vector measure. -/ +lemma VectorMeasure.exists_extension_of_additive_of_le_measure [IsFiniteMeasure μ] + (C : Set (Set α)) (m : Set α → E) + (hC : ∀ s ∈ C, MeasurableSet s) (hC_diff : ∀ s ∈ C, ∀ t ∈ C, s \ t ∈ C) (hC_inter : ∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C) (hC_union : ∀ s ∈ C, ∀ t ∈ C, s ∪ t ∈ C) - (h'C : ∀ t ε, MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε) : - ∃ m' : VectorMeasure α E, ∀ s ∈ C, m' s = m s ∧ ∀ s, ‖m' s‖ₑ ≤ μ s := by + (h'C : ∀ t ε, MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε) + (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) (h'm : ∀ s ∈ C, ∀ t ∈ C, Disjoint s t → m (s ∪ t) = m s + m t) : + ∃ m' : VectorMeasure α E, (∀ s ∈ C, m' s = m s) ∧ ∀ s, ‖m' s‖ₑ ≤ μ s := by + /- We will extend by continuity the function `m` from the class `C` to all measurable sets, + thanks to the fact that `C` is dense. To implement this properly, we work in the space + `MeasuredSets μ` with the distance `edist s t = μ (s ∆ t)`. The assumptions guarantee that + `m` is Lipschitz on `C` there, and therefore extends to a Lipschitz function. We check that + the extension is still finitely additive by approximating disjoint measurable sets by disjoint + measurable sets in `C`. Moreover, the extension is still dominated by `μ`. + The countable additivity follows from these two properties and + Lemma `VectorMeasure.of_additive_of_le_measure`. -/ classical + -- Express things inside `MeasuredSets μ`. let C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, s = c} have C'C (s : MeasuredSets μ) (hs : s ∈ C') : (s : Set α) ∈ C := by - rcases hs with ⟨t, ht, rfl⟩ - exact ht + rcases hs with ⟨t, ht, rfl⟩; exact ht have C'_dense : Dense C' := by simp only [Dense, EMetric.mem_closure_iff, gt_iff_lt] intro x ε εpos @@ -117,8 +180,10 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m refine ⟨⟨s, hC s sC⟩, ⟨s, sC, rfl⟩, ?_⟩ rw [edist_comm] exact hs - have A {s t : Set α} : Disjoint (s ∩ t) (s \ t) := Set.disjoint_sdiff_inter.symm + /- Let `m₀` be the function `m` expressed on the subtype of `MeasuredSets μ` made of + elements of `C`. -/ let m₀ : C' → E := fun x ↦ m x + -- It is Lipschitz continuous have lip : LipschitzWith 1 m₀ := by intro s t have : edist s t = edist (s : MeasuredSets μ) t := rfl @@ -130,17 +195,20 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m have It : ((t : Set α) ∩ s) ∪ (t \ s) = (t : Set α) := Set.inter_union_diff _ _ nth_rewrite 1 [← Is] nth_rewrite 3 [← It] - rw [h'm _ (hC_inter _ (C'C _ t.2) _ (C'C _ s.2)) _ (hC_diff _ (C'C _ t.2) _ (C'C _ s.2)) A, - h'm _ (hC_inter _ (C'C _ s.2) _ (C'C _ t.2)) _ (hC_diff _ (C'C _ s.2) _ (C'C _ t.2)) A, - Set.inter_comm] + rw [h'm _ (hC_inter _ (C'C _ t.2) _ (C'C _ s.2)) _ (hC_diff _ (C'C _ t.2) _ (C'C _ s.2)) + Set.disjoint_sdiff_inter.symm, + h'm _ (hC_inter _ (C'C _ s.2) _ (C'C _ t.2)) _ (hC_diff _ (C'C _ s.2) _ (C'C _ t.2)) + Set.disjoint_sdiff_inter.symm, Set.inter_comm] simp only [add_sub_add_left_eq_sub, ge_iff_le] apply enorm_sub_le.trans gcongr · exact hm _ (hC_diff _ (C'C _ s.2) _ (C'C _ t.2)) · exact hm _ (hC_diff _ (C'C _ t.2) _ (C'C _ s.2)) + -- Let `m₁` be the extension of `m₀` to all elements of `MeasuredSets μ` by continuity let m₁ : MeasuredSets μ → E := C'_dense.extend m₀ + -- It is again Lipschitz continuous and bounded by `μ` have m₁_lip : LipschitzWith 1 m₁ := C'_dense.lipschitzWith_extend lip - have B : ∀ s, ‖m₁ s‖ₑ ≤ μ s := by + have hBound : ∀ s, ‖m₁ s‖ₑ ≤ μ s := by have : IsClosed {s | ‖m₁ s‖ₑ ≤ μ s} := isClosed_le m₁_lip.continuous.enorm MeasuredSets.continuous_measure have : Dense {s | ‖m₁ s‖ₑ ≤ μ s} := by @@ -150,16 +218,18 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m convert hm s (C'C s hs) exact C'_dense.extend_eq lip.continuous ⟨s, hs⟩ simpa only [Dense, IsClosed.closure_eq, Set.mem_setOf_eq] using this - have B' (s t : MeasuredSets μ) (h : Disjoint (s : Set α) t) : + /- Most involved technical step: show that the extension `m₁` of `m₀` is still finitely + additive. -/ + have hAddit (s t : MeasuredSets μ) (h : Disjoint (s : Set α) t) : m₁ ⟨s ∪ t, s.2.union t.2⟩ = m₁ s + m₁ t := by suffices ∀ ε > 0, ‖m₁ (⟨s ∪ t, s.2.union t.2⟩) - m₁ s - m₁ t‖ₑ < ε by rw [← sub_eq_zero, ← enorm_eq_zero] contrapose! this exact ⟨‖m₁ ⟨s ∪ t, s.2.union t.2⟩ - (m₁ s + m₁ t)‖ₑ, this.bot_lt, le_of_eq (by abel_nf)⟩ intro ε εpos - obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ 8 * δ = ε := by - refine ⟨ε / 8, (ENNReal.div_pos εpos.ne' (by simp)), ?_⟩ - exact ENNReal.mul_div_cancel (by simp) (by simp) + obtain ⟨δ, δpos, hδ⟩ : ∃ δ, 0 < δ ∧ 8 * δ = ε := + ⟨ε / 8, (ENNReal.div_pos εpos.ne' (by simp)), ENNReal.mul_div_cancel (by simp) (by simp)⟩ + -- approximate `s` and `t` up to `δ` by sets `s'` and `t'` in `C`. obtain ⟨s', s'C, hs'⟩ : ∃ s' ∈ C, μ (s' ∆ s) < δ := h'C _ _ s.2 δpos obtain ⟨t', t'C, ht'⟩ : ∃ t' ∈ C, μ (t' ∆ t) < δ := h'C _ _ t.2 δpos have It : ‖m t' - m₁ t‖ₑ < δ := by @@ -169,6 +239,7 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m apply (m₁_lip _ _).trans_lt simp only [ENNReal.coe_one, MeasuredSets.edist_def, one_mul] exact ht' + -- `s'` and `t'` have no reason to be disjoint, but their intersection has small measure have I : s' ∩ t' ⊆ s ∩ t ∪ (s' ∆ s) ∪ (t' ∆ t) := by intro x ⟨hxs', hxt'⟩ by_cases hxs : x ∈ s <;> by_cases hxt : x ∈ t <;> @@ -180,6 +251,8 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m _ ≤ μ (s' ∆ s) + μ (t' ∆ t) := measure_union_le _ _ _ < δ + δ := by gcongr _ = 2 * δ := by ring + -- Therefore, the set `s'' := s' \ t'` still approximates well the original set `s`, it belongs + -- to `C`, and moreover `s''` and `t'` are disjoint. let s'' := s' \ t' have s''C : s'' ∈ C := hC_diff _ s'C _ t'C have hs'' : μ (s'' ∆ s) < 3 * δ := calc @@ -194,6 +267,7 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m apply (m₁_lip _ _).trans_lt simp only [ENNReal.coe_one, MeasuredSets.edist_def, one_mul] exact hs'' + -- `s'' ∪ t'` also approximates well `s ∪ t`. have Ist : ‖m (s'' ∪ t') - m₁ ⟨s ∪ t, s.2.union t.2⟩‖ₑ < 4 * δ := by have s''t'C : s'' ∪ t' ∈ C := hC_union _ s''C _ t'C have : m₁ ⟨s'' ∪ t', hC _ s''t'C⟩ = m (s'' ∪ t') := @@ -207,6 +281,9 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m _ ≤ μ (s'' ∆ s) + μ (t' ∆ t) := measure_union_le _ _ _ < 3 * δ + δ := by gcongr _ = 4 * δ := by ring + -- conclusion: to estimate `m₁ (s ∪ t) - m₁ s - m₁ t`, replace it up to a small error by + -- `m₁ (s'' ∪ t') - m₁ s'' - m₁ t'`, which is zero as `m₁` is additive on `C` and these + -- two sets are disjoint calc ‖m₁ (⟨s ∪ t, s.2.union t.2⟩) - m₁ s - m₁ t‖ₑ _ = ‖(m (s'' ∪ t') - m s'' - m t') + (m₁ ⟨s ∪ t, s.2.union t.2⟩ - m (s'' ∪ t')) + (m s'' - m₁ s) + (m t' - m₁ t)‖ₑ := by abel_nf @@ -220,8 +297,64 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m rwa [enorm_sub_rev] _ = 8 * δ := by ring _ = ε := hδ + -- conclusion of the proof: the function `s ↦ m₁ s` if `s` is measurable, and `0` otherwise, + -- defines a vector measure satisfying the required properties + let m' (s : Set α) := if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0 + let m'' : VectorMeasure α E := by + apply VectorMeasure.of_additive_of_le_measure m' (μ := μ) + · intro s + by_cases hs : MeasurableSet s + · simpa [hs, m'] using hBound _ + · simp [hs, m'] + · intro s t hs ht hst + simp only [hs, ht, MeasurableSet.union, ↓reduceDIte, m'] + exact hAddit ⟨s, hs⟩ ⟨t, ht⟩ hst + · intro s hs + simp [m', hs] + refine ⟨m'', fun s hs ↦ ?_, fun s ↦ ?_⟩ + · change m' s = m s + simp only [hC s hs, ↓reduceDIte, m'] + exact C'_dense.extend_eq lip.continuous ⟨⟨s, hC _ hs⟩, ⟨s, hs, rfl⟩⟩ + · change ‖m' s‖ₑ ≤ μ s + by_cases hs : MeasurableSet s + · simp only [hs, ↓reduceDIte, m'] + exact hBound ⟨s, hs⟩ + · simp [m', hs] +#check Set.PairwiseDisjoint + +open Set + +/-- Assume that a function is finitely additive on the elements of a set semiring `C` +(i.e. `m (⋃ i, s i) = ∑ i, m (s i)` whenever the `s i` are disjoint elements in `C` +with union in `C`). Then its extension to finite unions of elements of `C` is well defined, i.e., +it does not depend on the decomposition of a set as such a finite union. -/ +lemma glouk (C : Set (Set α)) (hC : IsSetSemiring C) {ι ι' : Type*} (a : Finset ι) (a' : Finset ι') + (f : ι → Set α) (hfC : ∀ i ∈ a, f i ∈ C) (hfdisj : PairwiseDisjoint a f) + (f' : ι' → Set α) (hf'C : ∀ i ∈ a', f' i ∈ C) (hf'disj : PairwiseDisjoint a' f') + (h : ⋃ i ∈ a, f i = ⋃ i ∈ a', f' i) + (m : Set α → E) + (hm : ∀ (b : Finset (Set α)), (∀ s ∈ b, s ∈ C) → PairwiseDisjoint (b : Set (Set α)) id → + (⋃ s ∈ b, s) ∈ C → m (⋃ s ∈ b, s) = ∑ s ∈ b, m s) : + ∑ i ∈ a, m (f i) = ∑ i ∈ a', m (f' i) := by + let g : ι × ι' → Set α := fun p ↦ f p.1 ∩ f' p.2 + have : ∀ p ∈ a ×ˢ a', g p ∈ C := by + intro p hp + simp only [Finset.mem_product] at hp + apply hC.inter_mem _ (hfC _ hp.1) _ (hf'C _ hp.2) + calc ∑ i ∈ a, m (f i) + _ = ∑ i ∈ a, (∑ j ∈ a', m (f i ∩ f' j)) := by + apply Finset.sum_congr rfl (fun i hi ↦ ?_) + have : f i = ⋃ j ∈ a', f i ∩ f' j := by + apply Subset.antisymm _ (by simp) + intro x hx + have A : x ∈ ⋃ j ∈ a', f' j := by + rw [← h] + simp only [mem_iUnion, exists_prop] + exact ⟨i, hi, hx⟩ + simpa [mem_iUnion, mem_inter_iff, exists_and_left, exists_prop, hx] using A + nth_rewrite 1 [this] @@ -230,7 +363,6 @@ lemma exists_extension (C : Set (Set α)) (hC : ∀ s ∈ C, MeasurableSet s) (m - let m' (s : Set α) := if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0 #exit From 9eb8d1073202979fa3c62e25ae2ae8e38adc94e4 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sun, 18 Jan 2026 11:25:54 +0100 Subject: [PATCH 6/8] better --- .../BigOperators/Group/Finset/Basic.lean | 57 +++++++------ Mathlib/MeasureTheory/Measure/AddContent.lean | 81 +++++++++++++++++-- 2 files changed, 107 insertions(+), 31 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean index 97ff53b528cc5b..cae457415d4bac 100644 --- a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean @@ -89,7 +89,11 @@ theorem prod_pair [DecidableEq ι] {a b : ι} (h : a ≠ b) : (∏ x ∈ ({a, b} : Finset ι), f x) = f a * f b := by rw [prod_insert (notMem_singleton.2 h), prod_singleton] -@[to_additive (attr := simp)] +/-- If a function is injective on a finset, products over the original finset or its image coincide. +See also `prod_image_of_pairwise_eq_one` for a version with weaker assumptions. -/ +@[to_additive (attr := simp) /-- If a function is injective on a finset, sums over the original +finset or its image coincide. +See also `sum_image_of_pairwise_eq_zero` for a version with weaker assumptions. -/] theorem prod_image [DecidableEq ι] {s : Finset κ} {g : κ → ι} : Set.InjOn g s → ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) := fold_image @@ -210,7 +214,12 @@ lemma prod_sum_eq_prod_toLeft_mul_prod_toRight (s : Finset (ι ⊕ κ)) (f : ι theorem prod_sumElim (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) : ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x := by simp -@[to_additive] +/-- Given a finite family of pairwise disjoint finsets, the product over their union is the product +of the products over the sets. +See also `prod_biUnion_of_pairwise_eq_one` for a version with weaker assumptions. -/ +@[to_additive /-- Given a finite family of pairwise disjoint finsets, the sum over their union is +the sum of the sums over the sets. +See also `sum_biUnion_of_pairwise_eq_zero` for a version with weaker assumptions. -/] theorem prod_biUnion [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι} (hs : Set.PairwiseDisjoint (↑s) t) : ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i := by rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion] @@ -383,30 +392,6 @@ lemma prod_congr_of_eq_on_inter {ι M : Type*} {s₁ s₂ : Finset ι} {f g : ι conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm] exact prod_congr rfl (by simpa) -/-- If a function `g` is injective on `s`, except for some points where `f (g i) = 1`, then -the product of `f (g x)` over `s` equals the product of `f i` over the image of `s`. -/ -@[to_additive /-- If a function `g` is injective on `s`, except for some points -where `f (g i) = 0`, then the sum of `f (g x)` over `s` equals the sum of `f i` over the -image of `s`. -/] -theorem prod_image_of_apply_eq_one_of_eq [DecidableEq ι] {s : Finset κ} {g : κ → ι} - (hg : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → g i = g j → f (g i) = 1) : - ∏ x ∈ s.image g, f x = ∏ x ∈ s, f (g x) := by - classical - let s' : Finset κ := s.filter (fun i ↦ f (g i) ≠ 1) - have : ∏ x ∈ s, f (g x) = ∏ x ∈ s', f (g x) := by - apply Finset.prod_congr_of_eq_on_inter <;> simp +contextual [s'] - rw [this, ← prod_image (s := s')]; swap - · intro i hi j hj hij - simp only [ne_eq, coe_filter, Set.mem_setOf_eq, s'] at hi hj - contrapose! hg - exact ⟨i, hi.1, j, hj.1, hg, hij, hi.2⟩ - apply Finset.prod_congr_of_eq_on_inter - · simp +contextual [s'] - grind - · simp +contextual [s'] - grind - · simp - @[to_additive] theorem prod_eq_mul_of_mem {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : ∏ x ∈ s, f x = f a * f b := by @@ -808,6 +793,26 @@ lemma prod_mul_eq_prod_mul_of_exists {s : Finset ι} {f : ι → M} {b₁ b₂ : simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert] rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)] +@[to_additive] +theorem prod_biUnion_of_pairwise_eq_one [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι} + (hs : (s : Set κ).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1) : + ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i := by + classical + let t' k := (t k).filter (fun i ↦ f i ≠ 1) + have : ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s.biUnion t', f x := by + apply prod_congr_of_eq_on_inter + · simp +contextual; grind + · simp +contextual; grind + · simp + rw [this, prod_biUnion]; swap + · intro i hi j hj hij a hai haj k hk + have hki : k ∈ t' i := hai hk + have hkj : k ∈ t' j := haj hk + simp only [ne_eq, mem_filter, t'] at hki hkj + exact (hki.2 (hs hi hj hij k (by grind) )).elim + apply Finset.prod_congr rfl (fun i hi ↦ ?_) + exact prod_filter_ne_one (t i) + @[to_additive] lemma prod_filter_of_pairwise_eq_one [DecidableEq ι] {f : κ → ι} {g : ι → M} {n : κ} {I : Finset κ} (hn : n ∈ I) (hf : (I : Set κ).Pairwise fun i j ↦ f i = f j → g (f i) = 1) : diff --git a/Mathlib/MeasureTheory/Measure/AddContent.lean b/Mathlib/MeasureTheory/Measure/AddContent.lean index 3f17d974e41961..99ff5be6f07a74 100644 --- a/Mathlib/MeasureTheory/Measure/AddContent.lean +++ b/Mathlib/MeasureTheory/Measure/AddContent.lean @@ -114,10 +114,11 @@ lemma addContent_biUnion {ι : Type*} {a : Finset ι} {f : ι → Set α} (hf : exact h_dis hi hj (by grind) · rwa [← A] simp only [b] - rw [Finset.sum_image_of_apply_eq_one_of_eq] - intro i hi j hj hij - contrapose! hij - exact (h_dis hi hj hij).ne (H i hi).ne_empty + rw [sum_image_of_pairwise_eq_zero] + intro i hi j hj hij h'ij + have : Disjoint (f i) (f j) := h_dis hi hj hij + simp only [← h'ij, disjoint_self, Set.bot_eq_empty] at this + simp [this] lemma addContent_union' (hs : s ∈ C) (ht : t ∈ C) (hst : s ∪ t ∈ C) (h_dis : Disjoint s t) : m (s ∪ t) = m s + m t := by @@ -230,7 +231,7 @@ noncomputable def AddContent.extendUnion (m : AddContent G C) (s : Set α) : G : else 0 lemma AddContent.extendUnion_eq (hC : IsSetSemiring C) - {m : AddContent G C} {s : Set α} {J : Finset (Set α)} + (m : AddContent G C) {s : Set α} {J : Finset (Set α)} (hJ : ↑J ⊆ C) (h'J : PairwiseDisjoint (J : Set (Set α)) id) (hs : s = ⋃₀ ↑J) : m.extendUnion s = ∑ s ∈ J, m s := by have h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J := @@ -240,6 +241,76 @@ lemma AddContent.extendUnion_eq (hC : IsSetSemiring C) · exact h.choose_spec.1 · exact h.choose_spec.2.1 · exact hJ + · exact h'J + · rw [← hs] + exact h.choose_spec.2.2.symm + +lemma AddContent.extendUnion_eq_of_mem (hC : IsSetSemiring C) + (m : AddContent G C) {s : Set α} (hs : s ∈ C) : + m.extendUnion s = m s := by + have : m.extendUnion s = ∑ t ∈ {s}, m t := + m.extendUnion_eq hC (by simp [hs]) (by simp) (by simp) + simp [this] + +def _root_.Set.extendUnion (C : Set (Set α)) : Set (Set α) := + {s | ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J} + +#check Finset.biUnion + +def AddContent.extendUnion' (m : AddContent G C) (hC : IsSetSemiring C) : + AddContent G C.extendUnion where + toFun := m.extendUnion + empty' := by rw [m.extendUnion_eq_of_mem hC hC.empty_mem, addContent_empty] + sUnion' I hI h'I hh'I := by + classical + have A (s) (hs : s ∈ I) : ∃ (J : Finset (Set α)), + ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J := hI hs + choose! J hJC hJdisj hJs using A + let K : Finset (Set α) := Finset.biUnion I J + have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by + simp [K, sUnion_eq_biUnion] at hJs ⊢; grind + rw [this, m.extendUnion_eq hC (J := K) (by simpa [K] using hJC) _ rfl]; swap + · intro a ha b hb hab + simp only [coe_biUnion, SetLike.mem_coe, mem_iUnion, exists_prop, K] at ha hb + rcases ha with ⟨i, iI, hi⟩ + rcases hb with ⟨j, jI, hj⟩ + rcases eq_or_ne i j with rfl | hij + · exact hJdisj i iI hi hj hab + · apply (h'I iI jI hij).mono + · simp only [id_eq, Set.le_eq_subset] + rw [hJs i iI] + simp only [sUnion_eq_biUnion, SetLike.mem_coe] + exact Set.subset_biUnion_of_mem (u := id) hi + · simp only [id_eq, Set.le_eq_subset] + rw [hJs j jI] + simp only [sUnion_eq_biUnion, SetLike.mem_coe] + exact Set.subset_biUnion_of_mem (u := id) hj + simp only [K] + rw [sum_biUnion]; swap + · intro i hi j hj hij + intro k hk hl u hu + simp only [Finset.le_eq_subset] at hk hl + have : Disjoint i j := h'I hi hj hij + have : Disjoint u u := by + apply this.mono + · simp only [Set.le_eq_subset] + rw [hJs i hi] + simp only [sUnion_eq_biUnion, SetLike.mem_coe] + apply Set.subset_biUnion_of_mem (u := id) (hk hu) + · simp only [Set.le_eq_subset] + rw [hJs j hj] + simp only [sUnion_eq_biUnion, SetLike.mem_coe] + apply Set.subset_biUnion_of_mem (u := id) (hl hu) + simp at this + + + + + + + + + #exit From 575ef9f655d7b15988070dfe7d2a5a12de1adf6c Mon Sep 17 00:00:00 2001 From: Sebastien Gouezel Date: Sun, 18 Jan 2026 12:38:42 +0100 Subject: [PATCH 7/8] better --- .../BigOperators/Group/Finset/Basic.lean | 11 +-- Mathlib/MeasureTheory/Measure/AddContent.lean | 92 +++++++++---------- 2 files changed, 45 insertions(+), 58 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean index cae457415d4bac..08e617852cdc3c 100644 --- a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean @@ -799,19 +799,14 @@ theorem prod_biUnion_of_pairwise_eq_one [DecidableEq ι] {s : Finset κ} {t : κ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i := by classical let t' k := (t k).filter (fun i ↦ f i ≠ 1) - have : ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s.biUnion t', f x := by - apply prod_congr_of_eq_on_inter - · simp +contextual; grind - · simp +contextual; grind - · simp - rw [this, prod_biUnion]; swap + have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by ext; simp [t']; grind + rw [← prod_filter_ne_one, ← this, prod_biUnion]; swap · intro i hi j hj hij a hai haj k hk have hki : k ∈ t' i := hai hk have hkj : k ∈ t' j := haj hk simp only [ne_eq, mem_filter, t'] at hki hkj exact (hki.2 (hs hi hj hij k (by grind) )).elim - apply Finset.prod_congr rfl (fun i hi ↦ ?_) - exact prod_filter_ne_one (t i) + exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i)) @[to_additive] lemma prod_filter_of_pairwise_eq_one [DecidableEq ι] {f : κ → ι} {g : ι → M} {n : κ} {I : Finset κ} diff --git a/Mathlib/MeasureTheory/Measure/AddContent.lean b/Mathlib/MeasureTheory/Measure/AddContent.lean index 99ff5be6f07a74..5c279d18e4feff 100644 --- a/Mathlib/MeasureTheory/Measure/AddContent.lean +++ b/Mathlib/MeasureTheory/Measure/AddContent.lean @@ -225,18 +225,20 @@ theorem sum_addContent_eq_of_sUnion_eq (hC : IsSetSemiring C) (J J' : Finset (Se exact hJ' ht open scoped Classical in -noncomputable def AddContent.extendUnion (m : AddContent G C) (s : Set α) : G := +/-- Extend a content over `C` to the finite unions of elements of `C` by additivity. +Use instead `AddContent.extendUnion` which is the same function bundled as an `AddContent`. -/ +noncomputable def AddContent.extendUnionFun (m : AddContent G C) (s : Set α) : G := if h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J then ∑ s ∈ h.choose, m s else 0 -lemma AddContent.extendUnion_eq (hC : IsSetSemiring C) +lemma AddContent.extendUnionFun_eq (hC : IsSetSemiring C) (m : AddContent G C) {s : Set α} {J : Finset (Set α)} (hJ : ↑J ⊆ C) (h'J : PairwiseDisjoint (J : Set (Set α)) id) (hs : s = ⋃₀ ↑J) : - m.extendUnion s = ∑ s ∈ J, m s := by + m.extendUnionFun s = ∑ s ∈ J, m s := by have h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J := ⟨J, hJ, h'J, hs⟩ - simp only [extendUnion, h, ↓reduceDIte] + simp only [extendUnionFun, h, ↓reduceDIte] apply sum_addContent_eq_of_sUnion_eq hC · exact h.choose_spec.1 · exact h.choose_spec.2.1 @@ -245,75 +247,65 @@ lemma AddContent.extendUnion_eq (hC : IsSetSemiring C) · rw [← hs] exact h.choose_spec.2.2.symm -lemma AddContent.extendUnion_eq_of_mem (hC : IsSetSemiring C) +lemma AddContent.extendUnionFun_eq_of_mem (hC : IsSetSemiring C) (m : AddContent G C) {s : Set α} (hs : s ∈ C) : - m.extendUnion s = m s := by - have : m.extendUnion s = ∑ t ∈ {s}, m t := - m.extendUnion_eq hC (by simp [hs]) (by simp) (by simp) + m.extendUnionFun s = m s := by + have : m.extendUnionFun s = ∑ t ∈ {s}, m t := + m.extendUnionFun_eq hC (by simp [hs]) (by simp) (by simp) simp [this] -def _root_.Set.extendUnion (C : Set (Set α)) : Set (Set α) := +/-- Finite disjoint unions of elements of a set of sets. -/ +def _root_.Set.finiteUnions (C : Set (Set α)) : Set (Set α) := {s | ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J} -#check Finset.biUnion - -def AddContent.extendUnion' (m : AddContent G C) (hC : IsSetSemiring C) : - AddContent G C.extendUnion where - toFun := m.extendUnion - empty' := by rw [m.extendUnion_eq_of_mem hC hC.empty_mem, addContent_empty] +/-- Extend a content over `C` to the finite unions of elements of `C` by additivity. -/ +noncomputable def AddContent.extendUnion (m : AddContent G C) (hC : IsSetSemiring C) : + AddContent G C.finiteUnions where + toFun := m.extendUnionFun + empty' := by rw [m.extendUnionFun_eq_of_mem hC hC.empty_mem, addContent_empty] sUnion' I hI h'I hh'I := by classical have A (s) (hs : s ∈ I) : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J := hI hs choose! J hJC hJdisj hJs using A + have H {a i} (hi : i ∈ I) (ha : a ∈ J i) : a ⊆ i := by + rw [hJs i hi] + simp only [sUnion_eq_biUnion, SetLike.mem_coe] + exact Set.subset_biUnion_of_mem (u := id) ha let K : Finset (Set α) := Finset.biUnion I J have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by simp [K, sUnion_eq_biUnion] at hJs ⊢; grind - rw [this, m.extendUnion_eq hC (J := K) (by simpa [K] using hJC) _ rfl]; swap + rw [this, m.extendUnionFun_eq hC (J := K) (by simpa [K] using hJC) _ rfl]; swap · intro a ha b hb hab simp only [coe_biUnion, SetLike.mem_coe, mem_iUnion, exists_prop, K] at ha hb rcases ha with ⟨i, iI, hi⟩ rcases hb with ⟨j, jI, hj⟩ rcases eq_or_ne i j with rfl | hij · exact hJdisj i iI hi hj hab - · apply (h'I iI jI hij).mono - · simp only [id_eq, Set.le_eq_subset] - rw [hJs i iI] - simp only [sUnion_eq_biUnion, SetLike.mem_coe] - exact Set.subset_biUnion_of_mem (u := id) hi - · simp only [id_eq, Set.le_eq_subset] - rw [hJs j jI] - simp only [sUnion_eq_biUnion, SetLike.mem_coe] - exact Set.subset_biUnion_of_mem (u := id) hj + · exact (h'I iI jI hij).mono (H iI hi) (H jI hj) simp only [K] - rw [sum_biUnion]; swap - · intro i hi j hj hij - intro k hk hl u hu - simp only [Finset.le_eq_subset] at hk hl - have : Disjoint i j := h'I hi hj hij - have : Disjoint u u := by - apply this.mono - · simp only [Set.le_eq_subset] - rw [hJs i hi] - simp only [sUnion_eq_biUnion, SetLike.mem_coe] - apply Set.subset_biUnion_of_mem (u := id) (hk hu) - · simp only [Set.le_eq_subset] - rw [hJs j hj] - simp only [sUnion_eq_biUnion, SetLike.mem_coe] - apply Set.subset_biUnion_of_mem (u := id) (hl hu) - simp at this - - - - - - - - + rw [sum_biUnion_of_pairwise_eq_zero]; swap + · intro i hi j hj hij k hk + simp only [Finset.mem_inter] at hk + have : Disjoint k k := by + have : Disjoint i j := h'I hi hj hij + exact this.mono (H hi hk.1) (H hj hk.2) + simp only [disjoint_self, Set.bot_eq_empty] at this + simp [this] + apply Finset.sum_congr rfl (fun i hi ↦ ?_) + exact (m.extendUnionFun_eq hC (hJC i hi) (hJdisj i hi) (hJs i hi)).symm +lemma AddContent.extendUnion_eq (hC : IsSetSemiring C) + (m : AddContent G C) {s : Set α} {J : Finset (Set α)} + (hJ : ↑J ⊆ C) (h'J : PairwiseDisjoint (J : Set (Set α)) id) (hs : s = ⋃₀ ↑J) : + m.extendUnion hC s = ∑ s ∈ J, m s := + m.extendUnionFun_eq hC hJ h'J hs +lemma AddContent.extendUnion_eq_of_mem (hC : IsSetSemiring C) + (m : AddContent G C) {s : Set α} (hs : s ∈ C) : + m.extendUnion hC s = m s := + m.extendUnionFun_eq_of_mem hC hs -#exit From d3f23e00e6df0a968456eab62f1f6760a017557a Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sun, 18 Jan 2026 18:56:16 +0100 Subject: [PATCH 8/8] more on contents --- Mathlib/MeasureTheory/Measure/AddContent.lean | 140 ++++++++++++++++-- Mathlib/MeasureTheory/SetSemiring.lean | 52 +++++++ 2 files changed, 178 insertions(+), 14 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/AddContent.lean b/Mathlib/MeasureTheory/Measure/AddContent.lean index 5c279d18e4feff..878f22c33dfcf6 100644 --- a/Mathlib/MeasureTheory/Measure/AddContent.lean +++ b/Mathlib/MeasureTheory/Measure/AddContent.lean @@ -239,13 +239,9 @@ lemma AddContent.extendUnionFun_eq (hC : IsSetSemiring C) have h : ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J := ⟨J, hJ, h'J, hs⟩ simp only [extendUnionFun, h, ↓reduceDIte] - apply sum_addContent_eq_of_sUnion_eq hC - · exact h.choose_spec.1 - · exact h.choose_spec.2.1 - · exact hJ - · exact h'J - · rw [← hs] - exact h.choose_spec.2.2.symm + apply sum_addContent_eq_of_sUnion_eq hC _ _ h.choose_spec.1 h.choose_spec.2.1 hJ h'J + rw [← hs] + exact h.choose_spec.2.2.symm lemma AddContent.extendUnionFun_eq_of_mem (hC : IsSetSemiring C) (m : AddContent G C) {s : Set α} (hs : s ∈ C) : @@ -254,10 +250,6 @@ lemma AddContent.extendUnionFun_eq_of_mem (hC : IsSetSemiring C) m.extendUnionFun_eq hC (by simp [hs]) (by simp) (by simp) simp [this] -/-- Finite disjoint unions of elements of a set of sets. -/ -def _root_.Set.finiteUnions (C : Set (Set α)) : Set (Set α) := - {s | ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J} - /-- Extend a content over `C` to the finite unions of elements of `C` by additivity. -/ noncomputable def AddContent.extendUnion (m : AddContent G C) (hC : IsSetSemiring C) : AddContent G C.finiteUnions where @@ -306,9 +298,6 @@ lemma AddContent.extendUnion_eq_of_mem (hC : IsSetSemiring C) m.extendUnion hC s = m s := m.extendUnionFun_eq_of_mem hC hs - - - variable [PartialOrder G] [CanonicallyOrderedAdd G] /-- For an `m : addContent C` on a `SetSemiring C`, if `I` is a `Finset` of pairwise disjoint @@ -415,6 +404,129 @@ theorem addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive {m : AddCont end IsSetSemiring +section OnIoc + +variable [LinearOrder α] {G : Type*} [AddCommGroup G] + +open scoped Classical in +/-- The function associating to an interval `Ioc u v` the difference `f v - f u`. +USe instead `AddContent.ofIoc` which upgrades this function to an additive content. -/ +noncomputable def AddContent.onIocAux (f : α → G) (s : Set α) : G := + if h : ∃ (p : α × α), p.1 ≤ p.2 ∧ s = Set.Ioc p.1 p.2 + then f h.choose.2 - f h.choose.1 else 0 + +lemma AddContent.onIocAux_eq {f : α → G} {u v : α} (h : u ≤ v) : + AddContent.onIocAux f (Ioc u v) = f v - f u := by + have h' : ∃ (p : α × α), p.1 ≤ p.2 ∧ Ioc u v = Ioc p.1 p.2 := ⟨(u, v), h, rfl⟩ + simp only [onIocAux, h', ↓reduceDIte] + set u' := h'.choose.1 + set v' := h'.choose.2 + have hu'v' : u' ≤ v' ∧ Ioc u v = Ioc u' v' := h'.choose_spec + rcases h.eq_or_lt with rfl | huv + · simp only [lt_self_iff_false, not_false_eq_true, Set.Ioc_eq_empty] at hu'v' + have : ¬ u' < v' := Set.Ioc_eq_empty_iff.1 hu'v'.2.symm + have : u' = v' := by order + simp [this] + have : ¬(Set.Ioc u v = ∅) := by simp [Set.Ioc_eq_empty_iff, huv] + rw [hu'v'.2, Set.Ioc_eq_empty_iff, not_not] at this + have I1 : v ≤ v' ∧ u' ≤ u := (Ioc_subset_Ioc_iff huv).1 hu'v'.2.subset + have I2 : v' ≤ v ∧ u ≤ u' := (Ioc_subset_Ioc_iff this).1 hu'v'.2.symm.subset + grind + +lemma AddContent.onIocAux_empty (f : α → G) : + AddContent.onIocAux f ∅ = 0 := by + rcases isEmpty_or_nonempty α with hα | hα + · simp [onIocAux] + inhabit α + have : Ioc (default : α) default = ∅ := by simp + rw [← this, AddContent.onIocAux_eq le_rfl] + simp + +/-- The additive content on the set of open-closed intervals, associating to an interval `Ioc u v` +the difference `f v - f u`. -/ +noncomputable def AddContent.onIoc (f : α → G) : + AddContent G {s : Set α | ∃ u v, u ≤ v ∧ s = Set.Ioc u v} where + toFun := AddContent.onIocAux f + empty' := AddContent.onIocAux_empty f + sUnion' := by + classical + /- Consider a finite union of open-closed intervals whose union is again an open-closed + interval `(u, v]`. We have to show that the sum of `f b - f a` over the intervals gives + `f v - f u`. Informally, `(u, v]` is an ordered + union `(a₀, a₁] ∪ (a₁, a₂] ∪ ... ∪ (a_{n-1}, aₙ]` and there is a telescoping sum. + For the formal argument, we argue by induction on the number of intervals, and remove the + right-most one (i.e., the one that contains `v`) to reduce to one interval less. Denoting + this right-most interval by `(u', v]`, then the union of the other intervals + is exactly `(u, u']`. From this and the induction assumption, the conclusion follows. -/ + intro I hI h'I h''I + induction hn : Finset.card I generalizing I with + | zero => + have : I = ∅ := by grind + simp [this, AddContent.onIocAux_empty f] + | succ n ih => + rcases h''I with ⟨u, v, huv, h'uv⟩ + -- If the interval `(u, v]` is empty, i.e., `u = v`, then the result is easy. + rcases huv.eq_or_lt with rfl | huv + · rw [h'uv] + simp only [lt_self_iff_false, not_false_eq_true, Set.Ioc_eq_empty, sUnion_eq_empty, + SetLike.mem_coe] at h'uv + have : onIocAux f (Set.Ioc u u) = ∑ u ∈ I, 0 := by simp [onIocAux_empty f] + rw [this] + apply Finset.sum_congr rfl (fun i hi ↦ ?_) + simp [h'uv i hi, onIocAux_empty] + -- otherwise, `v` is in `(u, v]`, therefore it belongs to some interval `(u', v']` + -- featuring in the union. + have : v ∈ ⋃₀ ↑I := by simp [h'uv, huv] + obtain ⟨t, tI, ht⟩ : ∃ t ∈ I, v ∈ t := by simpa using this + rcases hI tI with ⟨u', v', hu'v', rfl⟩ + -- we have `v' = v` since `(u', v']` is part of the union, and therefore + -- contained in `(u, v]`. + have : v = v' := by + apply le_antisymm ht.2 + suffices v' ∈ Ioc u v from this.2 + rw [← h'uv] + simp only [mem_sUnion, SetLike.mem_coe] + exact ⟨_, tI, ht.1.trans_le ht.2, le_rfl⟩ + subst this + -- also `u ≤ u'` for the same reason. + have uu' : u ≤ u' := by + by_contra! hu'u + have : u ∈ Set.Ioc u v := by + simp only [← h'uv, mem_sUnion, SetLike.mem_coe] + exact ⟨_, tI, hu'u, huv.le⟩ + simp at this + rw [h'uv, onIocAux_eq huv.le] + -- let us remove the right-most interval `(u', v]` from the union, and let `I'` be the + -- remaining set of intervals. + let I' := I.erase (Set.Ioc u' v) + have I'I : I' ⊆ I := erase_subset (Set.Ioc u' v) I + have I_eq_insert : I = insert (Set.Ioc u' v) I' := by simp [I', tI] + -- the intervals in `I'` cover exactly `(u, u']`. + have UI' : ⋃₀ ↑I' = Set.Ioc u u' := by + simp only [I_eq_insert, coe_insert, sUnion_insert] at h'uv + have : (Set.Ioc u' v ∪ ⋃₀ ↑I') \ Ioc u' v = ⋃₀ ↑I' := by + refine union_diff_cancel_left ?_ + rintro x ⟨hx, h'x⟩ + obtain ⟨s, sI', hxs⟩ : ∃ s ∈ I', x ∈ s := by simpa using h'x + simp only [mem_erase, ne_eq, I'] at sI' + have := h'I sI'.2 tI sI'.1 + grind + rw [h'uv] at this + rw [← this] + grind + -- by the inductive assumption, the sum over `I'` is exactly `f u' - f u`. + have IH : onIocAux f (⋃₀ ↑I') = ∑ u ∈ I', onIocAux f u := by + apply ih _ (Subset.trans I'I hI) (h'I.subset I'I) + · exact ⟨u, u', uu', UI'⟩ + · have := card_erase_add_one tI + grind + -- the conclusion follows. + rw [I_eq_insert, sum_insert, ← IH, UI', onIocAux_eq hu'v', onIocAux_eq uu'] + · simp + · simp [I'] + +end OnIoc + section AddContentExtend /-- An additive content obtained from another one on the same semiring of sets by setting the value diff --git a/Mathlib/MeasureTheory/SetSemiring.lean b/Mathlib/MeasureTheory/SetSemiring.lean index 3dcefa238f34d5..f90304a76e9dc8 100644 --- a/Mathlib/MeasureTheory/SetSemiring.lean +++ b/Mathlib/MeasureTheory/SetSemiring.lean @@ -438,6 +438,58 @@ lemma sUnion_disjointOfUnion (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) : end disjointOfUnion +/-- Finite disjoint unions of elements of a set of sets. -/ +def _root_.Set.finiteUnions (C : Set (Set α)) : Set (Set α) := + {s | ∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J} + +lemma _root_.Set.self_subset_finiteUnions (C : Set (Set α)) : C ⊆ C.finiteUnions := + fun s hs ↦ ⟨{s}, by simp [hs], by simp, by simp⟩ + +/-- Given a semi-ring of sets, finite unions of these also form a semi-ring of sets. -/ +lemma finiteUnions (hC : IsSetSemiring C) : + IsSetSemiring C.finiteUnions where + empty_mem := ⟨∅, by simp⟩ + inter_mem := by + classical + rintro s ⟨I, IC, Idisj, rfl⟩ t ⟨J, JC, Jdisj, rfl⟩ + refine ⟨(I ×ˢ J).image (fun p ↦ p.1 ∩ p.2), ?_, ?_, ?_⟩ + · simp only [coe_image, coe_product, image_prod, image2_subset_iff, SetLike.mem_coe] + intro i hi j hj + apply hC.inter_mem _ (IC hi) _ (JC hj) + · intro p hp q hq hpq + simp only [coe_image, coe_product, image_prod, mem_image2, SetLike.mem_coe] at hp hq + rcases hp with ⟨ip, hip, jp, hjp, rfl⟩ + rcases hq with ⟨iq, hiq, jq, hjq, rfl⟩ + rcases eq_or_ne ip iq with rfl | hipq + · exact (Jdisj hjp hjq (by grind)).mono inter_subset_right inter_subset_right + · exact (Idisj hip hiq hipq).mono inter_subset_left inter_subset_left + · ext; simp; grind + diff_eq_sUnion' := by + classical + rintro s ⟨I, IC, Idisj, rfl⟩ t ⟨J, JC, Jdisj, rfl⟩ + have A (i) (hi : i ∈ I) : ∃ J' : Finset (Set α), ↑J' ⊆ C ∧ + PairwiseDisjoint (J' : Set (Set α)) id ∧ i \ ⋃₀ J = ⋃₀ J' := + hC.exists_disjoint_finset_diff_eq (IC hi) JC + choose! J' hJ'C hJ'disj hiJ' using A + have H {a i} (hi : i ∈ I) (ha : a ∈ J' i) : a ⊆ i \ ⋃₀ ↑J := by + rw [hiJ' i hi] + simp only [sUnion_eq_biUnion, SetLike.mem_coe] + exact Set.subset_biUnion_of_mem (u := id) ha + refine ⟨I.biUnion J', ?_, ?_, ?_⟩ + · exact Subset.trans (by simp; grind) C.self_subset_finiteUnions + · intro s hs t ht hst + simp only [coe_biUnion, SetLike.mem_coe, mem_iUnion, exists_prop] at hs ht + rcases hs with ⟨i, iI, hi⟩ + rcases ht with ⟨j, jI, hj⟩ + rcases eq_or_ne i j with rfl | hij + · exact hJ'disj i iI hi hj hst + · exact (Idisj iI jI hij).mono ((H iI hi).trans diff_subset) + ((H jI hj).trans diff_subset) + · simp only [sUnion_eq_biUnion, SetLike.mem_coe, iUnion_diff, coe_biUnion, mem_iUnion, + exists_prop, iUnion_exists, biUnion_and'] + apply iUnion_congr (fun i ↦ iUnion_congr (fun hi ↦ ?_)) + simpa [sUnion_eq_biUnion] using hiJ' i hi + end IsSetSemiring /-- A ring of sets `C` is a family of sets containing `∅`, stable by union and set difference.