From a689675ed1345b6edf14d089907e1e2b4c5142ae Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 22 Jul 2024 20:30:06 +0200 Subject: [PATCH] Remove now-superfluous open statements; fix one proof in Unused/. --- SphereEversion/InductiveConstructions.lean | 3 --- SphereEversion/Loops/DeltaMollifier.lean | 5 ++--- SphereEversion/Loops/Reparametrization.lean | 3 +-- SphereEversion/Loops/Surrounding.lean | 9 ++------- SphereEversion/ToMathlib/Analysis/ContDiff.lean | 3 --- .../ToMathlib/Analysis/Convex/Basic.lean | 5 +---- SphereEversion/ToMathlib/ExistsOfConvex.lean | 2 +- .../Geometry/Manifold/Algebra/SmoothGerm.lean | 2 +- SphereEversion/ToMathlib/Partition.lean | 3 +-- .../ToMathlib/Topology/Algebra/Module.lean | 4 ---- SphereEversion/ToMathlib/Topology/Path.lean | 4 ++-- .../ToMathlib/Unused/IntervalIntegral.lean | 15 +++++++-------- 12 files changed, 18 insertions(+), 40 deletions(-) diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index 3428052d..a6539a13 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -11,7 +11,6 @@ import SphereEversion.Notations attribute [gcongr] nhdsSet_mono open Set Filter Function - open scoped Topology unitInterval /-! @@ -252,8 +251,6 @@ section Htpy private noncomputable def T : ℕ → ℝ := fun n ↦ Nat.rec 0 (fun k x ↦ x + 1 / (2 : ℝ) ^ (k + 1)) n -open scoped BigOperators - -- Note this is more painful than Patrick hoped for. Maybe this should be the definition of T. private theorem T_eq (n : ℕ) : T n = 1 - (1 / 2 : ℝ) ^ n := by unfold T diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean index 3d147e79..41883e21 100644 --- a/SphereEversion/Loops/DeltaMollifier.lean +++ b/SphereEversion/Loops/DeltaMollifier.lean @@ -29,9 +29,8 @@ convolutions. noncomputable section -open Set Function MeasureTheory.MeasureSpace ContinuousLinearMap Filter - -open scoped Topology BigOperators Filter Convolution +open Set Function MeasureTheory.MeasureSpace ContinuousLinearMap +open scoped Topology Filter Convolution variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 24d7cdd6..623e6fc9 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -48,8 +48,7 @@ existence of delta mollifiers, partitions of unity, and the inverse function the noncomputable section open Set Function MeasureTheory intervalIntegral Filter - -open scoped Topology unitInterval Manifold BigOperators +open scoped Topology Manifold variable {E F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index 9070b3d6..e66e7853 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -32,14 +32,9 @@ The key results are: * `exists_surrounding_loops` -/ - --- to obtain that normed spaces are locally connected --- to obtain that normed spaces are locally connected -- to obtain that normed spaces are locally connected --- to obtain that normed spaces are locally connected -open Set Function FiniteDimensional Int Prod Function Path Filter TopologicalSpace - -open scoped Classical Topology unitInterval BigOperators +open Set Function FiniteDimensional Int Prod Path Filter +open scoped Topology unitInterval namespace IsPathConnected diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean index e253fcf5..760a6dd0 100644 --- a/SphereEversion/ToMathlib/Analysis/ContDiff.lean +++ b/SphereEversion/ToMathlib/Analysis/ContDiff.lean @@ -8,7 +8,6 @@ import SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm noncomputable section open scoped Topology Filter - open Function section @@ -288,8 +287,6 @@ end Arithmetic section -open scoped BigOperators - variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean index bb00c91d..22024d97 100644 --- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean +++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean @@ -2,11 +2,9 @@ import Mathlib.Analysis.Convex.Combination import Mathlib.Algebra.Module.BigOperators import Mathlib.Algebra.Order.Hom.Ring -open scoped BigOperators - open Function Set --- move +-- TODO: move this lemma and the following one theorem map_finsum {β α γ : Type*} [AddCommMonoid β] [AddCommMonoid γ] {G : Type*} [FunLike G β γ] [AddMonoidHomClass G β γ] (g : G) {f : α → β} (hf : (Function.support f).Finite) : g (∑ᶠ i, f i) = ∑ᶠ i, g (f i) := @@ -17,7 +15,6 @@ theorem finprod_eq_prod_of_mulSupport_subset_of_finite {α M} [CommMonoid M] (f (h : mulSupport f ⊆ s) (hs : s.Finite) : ∏ᶠ i, f i = ∏ i in hs.toFinset, f i := by apply finprod_eq_prod_of_mulSupport_subset f; rwa [Set.Finite.coe_toFinset] --- end move section variable {𝕜 𝕜' : Type*} {E : Type*} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index acbee541..623533d8 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -2,7 +2,7 @@ import SphereEversion.ToMathlib.Partition noncomputable section -open scoped Topology Filter Manifold BigOperators +open scoped Topology Manifold open Set Function Filter diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean index e2d4079f..22441160 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean @@ -21,7 +21,7 @@ noncomputable section open Filter Set -open scoped Manifold Topology BigOperators +open scoped Manifold Topology -- FIXME: move to `Manifold/Algebra/SmoothFunctions`, around line 46 section diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean index b247622e..29e49824 100644 --- a/SphereEversion/ToMathlib/Partition.lean +++ b/SphereEversion/ToMathlib/Partition.lean @@ -4,8 +4,7 @@ import SphereEversion.ToMathlib.Geometry.Manifold.Algebra.SmoothGerm noncomputable section -open scoped Topology Filter BigOperators - +open scoped Topology open Set Function Filter variable {ι : Type*} diff --git a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean index 43dca399..dfcb90e9 100644 --- a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean +++ b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean @@ -1,9 +1,5 @@ import Mathlib.Topology.Algebra.Module.Basic -open Filter ContinuousLinearMap Function - -open scoped Topology BigOperators Filter - namespace ContinuousLinearMap variable {R₁ M₁ M₂ M₃ : Type*} [Semiring R₁] diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean index 626303c5..6056f7a1 100644 --- a/SphereEversion/ToMathlib/Topology/Path.lean +++ b/SphereEversion/ToMathlib/Topology/Path.lean @@ -1,9 +1,9 @@ import Mathlib.Topology.Connected.PathConnected import Mathlib.Analysis.Normed.Field.Basic -open Set Function Int TopologicalSpace +open Set Function -open scoped BigOperators Topology unitInterval +open scoped Topology unitInterval noncomputable section diff --git a/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean b/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean index 00e6d803..2f8b9970 100644 --- a/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean +++ b/SphereEversion/ToMathlib/Unused/IntervalIntegral.lean @@ -3,9 +3,7 @@ import Mathlib.MeasureTheory.Integral.Periodic noncomputable section -open TopologicalSpace MeasureTheory Filter FirstCountableTopology Metric Set Function - -open scoped Topology Filter NNReal BigOperators Interval +open MeasureTheory Set section @@ -47,7 +45,7 @@ theorem integral_mono_of_le {f g : ℝ → ℝ} {a b : ℝ} {μ : Measure ℝ} ( (hfg : f ≤ᵐ[μ.restrict (Ι a b)] g) : ∫ u in a..b, f u ∂μ ≤ ∫ u in a..b, g u ∂μ := by rw [uIoc_of_le hab] at hfg let H := hfg.filter_mono (ae_mono le_rfl) - simpa only [integral_of_le hab] using set_integral_mono_ae_restrict hf.1 hg.1 H + simpa only [integral_of_le hab] using setIntegral_mono_ae_restrict hf.1 hg.1 H theorem integral_mono_of_le_of_nonneg {f g : ℝ → ℝ} {a b : ℝ} {μ : Measure ℝ} (hab : a ≤ b) (hf : AEStronglyMeasurable f <| μ.restrict (Ι a b)) @@ -62,12 +60,13 @@ theorem integral_antimono_of_le {f g : ℝ → ℝ} {a b : ℝ} {μ : Measure (hfg : f ≤ᵐ[μ.restrict (Ι a b)] g) : ∫ u in a..b, g u ∂μ ≤ ∫ u in a..b, f u ∂μ := by cases' hab.eq_or_lt with hab hab · simp [hab] - · rw [uIoc_of_lt hab] at hfg - rw [integral_symm b a] - rw [integral_symm b a] + · rw [uIoc_of_ge hab.le] at hfg + rw [integral_symm b a, integral_symm b a] apply neg_le_neg apply integral_mono_of_le hab.le hf.symm hg.symm - rwa [uIoc_swap, uIoc_of_lt hab] + have : Ioc b a = uIoc b a := by rw [uIoc_of_le hab.le] + rw [← this] + exact hfg theorem integral_antimono_of_le_of_nonneg {f g : ℝ → ℝ} {a b : ℝ} {μ : Measure ℝ} (hab : b ≤ a) (hf : AEStronglyMeasurable f <| μ.restrict (Ι a b))