diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean index 83750ccb4074b1..08e617852cdc3c 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] @@ -784,6 +793,21 @@ 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 : 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 + 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 κ} (hn : n ∈ I) (hf : (I : Set κ).Pairwise fun i j ↦ f i = f j → g (f i) = 1) : 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/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..5c279d18e4feff 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,27 @@ 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 [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 by_cases hs_empty : s = ∅ @@ -118,9 +141,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 +163,154 @@ 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 +/-- 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.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.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 [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 + +lemma AddContent.extendUnionFun_eq_of_mem (hC : IsSetSemiring C) + (m : AddContent G C) {s : Set α} (hs : s ∈ C) : + 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] + +/-- 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 + 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.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 + · exact (h'I iI jI hij).mono (H iI hi) (H jI hj) + simp only [K] + 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 + + + + +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 +331,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 +356,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 +377,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 +405,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 +420,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 +431,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 +452,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 +468,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 +480,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 +503,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 +576,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 +593,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/Topology/Instances/ENNReal/Lemmas.lean b/Mathlib/Topology/Instances/ENNReal/Lemmas.lean index 70207c765aecb6..a65ddae563677b 100644 --- a/Mathlib/Topology/Instances/ENNReal/Lemmas.lean +++ b/Mathlib/Topology/Instances/ENNReal/Lemmas.lean @@ -1489,3 +1489,22 @@ 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 + +set_option linter.style.longFile 1700 diff --git a/Mathlib/test.lean b/Mathlib/test.lean new file mode 100644 index 00000000000000..e9b08a810fafa2 --- /dev/null +++ b/Mathlib/test.lean @@ -0,0 +1,368 @@ +/- +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 NNReal + +variable {α : Type*} [MeasurableSpace α] {E : Type*} [NormedAddCommGroup E] +[CompleteSpace E] + +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} + +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 + +open scoped ENNReal + +/-- 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) < ε) + (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 + 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 + /- 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 + 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 _ (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 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 + 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 + /- 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 * δ = ε := + ⟨ε / 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 + 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' + -- `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 <;> + 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 + -- 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 + μ (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'' + -- `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') := + 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 + -- 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 + _ ≤ ‖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δ + -- 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] + + + + + + + + + + +#exit