From 4e3fd1ae9518ed2894bfc00592c81a3ee2b6180e Mon Sep 17 00:00:00 2001 From: mathlib4-update-dependencies-bot <150093616+mathlib-bors@users.noreply.github.com> Date: Thu, 26 Sep 2024 00:03:37 +0000 Subject: [PATCH 1/9] chore: update Mathlib dependencies 2024-09-25 (#17143) This PR updates the Mathlib dependencies. --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0cedc34894a16..f82a37b5c0c11 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6d5e1c81277e960372c94f19172440e39b3c5980", + "rev": "c57ab80c8dd20b345b29c81c446c78a6b3677d20", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From 3874c4e1905a870816d44fb4873869a99637ed73 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 26 Sep 2024 00:13:21 +0000 Subject: [PATCH 2/9] feat: generalize normed instances on `UniformSpace.Completion` (#17059) Notably, `NormedSpace.to_uniformContinuousConstSMul` is generalized to `BoundedSMul` on `PseudoMetricSpace`s, relaxing the scalar considerably from normed fields. Co-authored-by: Eric Wieser --- .../Analysis/Normed/Module/Completion.lean | 78 ++++++++----------- Mathlib/Analysis/Normed/MulAction.lean | 1 + .../PiTensorProduct/InjectiveSeminorm.lean | 3 +- Mathlib/Topology/MetricSpace/Algebra.lean | 6 ++ Mathlib/Topology/MetricSpace/Completion.lean | 23 ++++++ 5 files changed, 64 insertions(+), 47 deletions(-) diff --git a/Mathlib/Analysis/Normed/Module/Completion.lean b/Mathlib/Analysis/Normed/Module/Completion.lean index bb143e6302377..c4377b5b2a68a 100644 --- a/Mathlib/Analysis/Normed/Module/Completion.lean +++ b/Mathlib/Analysis/Normed/Module/Completion.lean @@ -27,20 +27,16 @@ namespace UniformSpace namespace Completion -variable (𝕜 E : Type*) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] +variable (𝕜 E : Type*) -instance (priority := 100) NormedSpace.to_uniformContinuousConstSMul : - UniformContinuousConstSMul 𝕜 E := - ⟨fun c => (lipschitzWith_smul c).uniformContinuous⟩ +instance [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : + NormedSpace 𝕜 (Completion E) where + norm_smul_le := norm_smul_le -instance : NormedSpace 𝕜 (Completion E) := - { Completion.instModule with - norm_smul_le := fun c x => - induction_on x - (isClosed_le (continuous_const_smul _).norm (continuous_const.mul continuous_norm)) fun y => - by simp only [← coe_smul, norm_coe, norm_smul, le_rfl] } +section Module variable {𝕜 E} +variable [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] /-- Embedding of a normed space to its completion as a linear isometry. -/ def toComplₗᵢ : E →ₗᵢ[𝕜] Completion E := @@ -66,46 +62,38 @@ theorem norm_toComplL {𝕜 E : Type*} [NontriviallyNormedField 𝕜] [NormedAdd [NormedSpace 𝕜 E] [Nontrivial E] : ‖(toComplL : E →L[𝕜] Completion E)‖ = 1 := (toComplₗᵢ : E →ₗᵢ[𝕜] Completion E).norm_toContinuousLinearMap +end Module + section Algebra -variable (𝕜) (A : Type*) - -instance [SeminormedRing A] : NormedRing (Completion A) := - { Completion.ring, - Completion.instMetricSpace with - dist_eq := fun x y => by - refine Completion.induction_on₂ x y ?_ ?_ <;> clear x y - · refine isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous ?_ - exact Continuous.comp Completion.continuous_extension continuous_sub - · intro x y - rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm] - norm_mul := fun x y => by - refine Completion.induction_on₂ x y ?_ ?_ <;> clear x y - · exact - isClosed_le (Continuous.comp continuous_norm continuous_mul) - (Continuous.comp _root_.continuous_mul - (Continuous.prod_map continuous_norm continuous_norm)) - · intro x y - simp only [← coe_mul, norm_coe] - exact norm_mul_le x y } - -instance [SeminormedCommRing A] [NormedAlgebra 𝕜 A] [UniformContinuousConstSMul 𝕜 A] : - NormedAlgebra 𝕜 (Completion A) := - { Completion.algebra A 𝕜 with - norm_smul_le := fun r x => by - refine Completion.induction_on x ?_ ?_ <;> clear x - · exact - isClosed_le (Continuous.comp continuous_norm (continuous_const_smul r)) - (Continuous.comp (continuous_mul_left _) continuous_norm) - · intro x - simp only [← coe_smul, norm_coe] - exact norm_smul_le r x } +variable (A : Type*) + +instance [SeminormedRing A] : NormedRing (Completion A) where + __ : NormedAddCommGroup (Completion A) := inferInstance + __ : Ring (Completion A) := inferInstance + norm_mul x y := by + induction x, y using induction_on₂ with + | hp => + exact + isClosed_le (Continuous.comp continuous_norm continuous_mul) + (Continuous.comp _root_.continuous_mul + (Continuous.prod_map continuous_norm continuous_norm)) + | ih x y => + simp only [← coe_mul, norm_coe] + exact norm_mul_le x y + +instance [SeminormedCommRing A] : NormedCommRing (Completion A) where + __ : CommRing (Completion A) := inferInstance + __ : NormedRing (Completion A) := inferInstance + +instance [NormedField 𝕜] [SeminormedCommRing A] [NormedAlgebra 𝕜 A] : + NormedAlgebra 𝕜 (Completion A) where + norm_smul_le := norm_smul_le instance [NormedField A] [CompletableTopField A] : NormedField (UniformSpace.Completion A) where - dist_eq x y := by - refine induction_on₂ x y ?_ (by simp [← coe_sub, dist_eq_norm]) - exact isClosed_eq (uniformContinuous_extension₂ _).continuous (by fun_prop) + __ : NormedCommRing (Completion A) := inferInstance + __ : Field (Completion A) := inferInstance norm_mul' x y := induction_on₂ x y (isClosed_eq (by fun_prop) (by fun_prop)) (by simp [← coe_mul]) end Algebra diff --git a/Mathlib/Analysis/Normed/MulAction.lean b/Mathlib/Analysis/Normed/MulAction.lean index 1c42cc236b1e9..2c9c706fdb6c1 100644 --- a/Mathlib/Analysis/Normed/MulAction.lean +++ b/Mathlib/Analysis/Normed/MulAction.lean @@ -5,6 +5,7 @@ Authors: Eric Wieser -/ import Mathlib.Analysis.Normed.Field.Basic import Mathlib.Topology.MetricSpace.Algebra +import Mathlib.Topology.Algebra.UniformMulAction /-! # Lemmas for `BoundedSMul` over normed additive groups diff --git a/Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean b/Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean index 1ddd022c490b2..299585582989c 100644 --- a/Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean +++ b/Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean @@ -211,8 +211,7 @@ theorem injectiveSeminorm_le_projectiveSeminorm : existsi PUnit, inferInstance, inferInstance ext x simp only [Seminorm.zero_apply, Seminorm.comp_apply, coe_normSeminorm] - have heq : toDualContinuousMultilinearMap PUnit x = 0 := by ext _ - rw [heq, norm_zero] + rw [Subsingleton.elim (toDualContinuousMultilinearMap PUnit x) 0, norm_zero] · intro p hp simp only [Set.mem_setOf_eq] at hp obtain ⟨G, _, _, h⟩ := hp diff --git a/Mathlib/Topology/MetricSpace/Algebra.lean b/Mathlib/Topology/MetricSpace/Algebra.lean index c2d744b24f070..724512392f31b 100644 --- a/Mathlib/Topology/MetricSpace/Algebra.lean +++ b/Mathlib/Topology/MetricSpace/Algebra.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Heather Macbeth -/ import Mathlib.Topology.Algebra.MulAction +import Mathlib.Topology.Algebra.UniformMulAction import Mathlib.Topology.MetricSpace.Lipschitz /-! @@ -143,6 +144,11 @@ instance (priority := 100) BoundedSMul.continuousSMul : ContinuousSMul α β whe gcongr _ < ε := hδε +instance (priority := 100) BoundedSMul.toUniformContinuousConstSMul : + UniformContinuousConstSMul α β := + ⟨fun c => ((lipschitzWith_iff_dist_le_mul (K := nndist c 0)).2 fun _ _ => + dist_smul_pair c _ _).uniformContinuous⟩ + -- this instance could be deduced from `NormedSpace.boundedSMul`, but we prove it separately -- here so that it is available earlier in the hierarchy instance Real.boundedSMul : BoundedSMul ℝ ℝ where diff --git a/Mathlib/Topology/MetricSpace/Completion.lean b/Mathlib/Topology/MetricSpace/Completion.lean index 1ffdfa1fba1b7..97c5f07d31c6e 100644 --- a/Mathlib/Topology/MetricSpace/Completion.lean +++ b/Mathlib/Topology/MetricSpace/Completion.lean @@ -6,6 +6,8 @@ Authors: Sébastien Gouëzel import Mathlib.Topology.UniformSpace.Completion import Mathlib.Topology.MetricSpace.Isometry import Mathlib.Topology.MetricSpace.Lipschitz +import Mathlib.Topology.MetricSpace.Algebra +import Mathlib.Topology.Algebra.GroupCompletion import Mathlib.Topology.Instances.Real /-! @@ -168,6 +170,27 @@ theorem coe_isometry : Isometry ((↑) : α → Completion α) := protected theorem edist_eq (x y : α) : edist (x : Completion α) y = edist x y := coe_isometry x y +instance {M} [Zero M] [Zero α] [SMul M α] [PseudoMetricSpace M] [BoundedSMul M α] : + BoundedSMul M (Completion α) where + dist_smul_pair' c x₁ x₂ := by + induction x₁, x₂ using induction_on₂ with + | hp => + exact isClosed_le + ((continuous_fst.const_smul _).dist (continuous_snd.const_smul _)) + (continuous_const.mul (continuous_fst.dist continuous_snd)) + | ih x₁ x₂ => + rw [← coe_smul, ← coe_smul, Completion.dist_eq, Completion.dist_eq] + exact dist_smul_pair c x₁ x₂ + dist_pair_smul' c₁ c₂ x := by + induction x using induction_on with + | hp => + exact isClosed_le + ((continuous_const_smul _).dist (continuous_const_smul _)) + (continuous_const.mul (continuous_id.dist continuous_const)) + | ih x => + rw [← coe_smul, ← coe_smul, Completion.dist_eq, ← coe_zero, Completion.dist_eq] + exact dist_pair_smul c₁ c₂ x + end UniformSpace.Completion open UniformSpace Completion NNReal From 9678fd7fe516e300382ea1c0dfec4cab4700b340 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 26 Sep 2024 00:42:50 +0000 Subject: [PATCH 3/9] chore: split Algebra.Bounds and Algebra.Order.Pointwise (#16986) Delete `Algebra.Bounds` and `Algebra.Order.Pointwise`. Create * `Algebra.Order.Field.Pointwise` for lemmas about pointwise operations in linear ordered fields * `Algebra.Order.Group.CompleteLattice` for distributivity of group operations over supremum/infimum * `Algebra.Order.Group.Pointwise.Bounds` for boundedness of pointwise-defined sets * `Algebra.Order.Group.Pointwise.CompleteLattice` for lemmas about the supremum/infimum of pointwise-defined sets. --- Mathlib.lean | 6 +- Mathlib/Algebra/Bounds.lean | 167 ------------ Mathlib/Algebra/Order/CompleteField.lean | 2 +- Mathlib/Algebra/Order/Field/Pointwise.lean | 126 +++++++++ .../Algebra/Order/Group/CompleteLattice.lean | 49 ++++ .../Algebra/Order/Group/Pointwise/Bounds.lean | 117 ++++++++ .../Group/Pointwise/CompleteLattice.lean | 117 ++++++++ Mathlib/Algebra/Order/Pointwise.lean | 250 ------------------ Mathlib/Data/Real/Archimedean.lean | 2 +- .../Constructions/HaarToSphere.lean | 2 +- 10 files changed, 416 insertions(+), 422 deletions(-) delete mode 100644 Mathlib/Algebra/Bounds.lean create mode 100644 Mathlib/Algebra/Order/Field/Pointwise.lean create mode 100644 Mathlib/Algebra/Order/Group/CompleteLattice.lean create mode 100644 Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean create mode 100644 Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean delete mode 100644 Mathlib/Algebra/Order/Pointwise.lean diff --git a/Mathlib.lean b/Mathlib.lean index 2f1502803917a..8f564f4f1e5de 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -56,7 +56,6 @@ import Mathlib.Algebra.BigOperators.Ring.Multiset import Mathlib.Algebra.BigOperators.Ring.Nat import Mathlib.Algebra.BigOperators.RingEquiv import Mathlib.Algebra.BigOperators.WithTop -import Mathlib.Algebra.Bounds import Mathlib.Algebra.Category.AlgebraCat.Basic import Mathlib.Algebra.Category.AlgebraCat.Limits import Mathlib.Algebra.Category.AlgebraCat.Monoidal @@ -566,6 +565,7 @@ import Mathlib.Algebra.Order.Field.Canonical.Defs import Mathlib.Algebra.Order.Field.Defs import Mathlib.Algebra.Order.Field.InjSurj import Mathlib.Algebra.Order.Field.Pi +import Mathlib.Algebra.Order.Field.Pointwise import Mathlib.Algebra.Order.Field.Power import Mathlib.Algebra.Order.Field.Rat import Mathlib.Algebra.Order.Field.Subfield @@ -577,6 +577,7 @@ import Mathlib.Algebra.Order.Group.Action import Mathlib.Algebra.Order.Group.Action.Synonym import Mathlib.Algebra.Order.Group.Basic import Mathlib.Algebra.Order.Group.Bounds +import Mathlib.Algebra.Order.Group.CompleteLattice import Mathlib.Algebra.Order.Group.Cone import Mathlib.Algebra.Order.Group.Defs import Mathlib.Algebra.Order.Group.DenselyOrdered @@ -589,6 +590,8 @@ import Mathlib.Algebra.Order.Group.MinMax import Mathlib.Algebra.Order.Group.Nat import Mathlib.Algebra.Order.Group.OrderIso import Mathlib.Algebra.Order.Group.PiLex +import Mathlib.Algebra.Order.Group.Pointwise.Bounds +import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice import Mathlib.Algebra.Order.Group.PosPart import Mathlib.Algebra.Order.Group.Prod import Mathlib.Algebra.Order.Group.Synonym @@ -644,7 +647,6 @@ import Mathlib.Algebra.Order.Nonneg.Floor import Mathlib.Algebra.Order.Nonneg.Module import Mathlib.Algebra.Order.Nonneg.Ring import Mathlib.Algebra.Order.Pi -import Mathlib.Algebra.Order.Pointwise import Mathlib.Algebra.Order.Positive.Field import Mathlib.Algebra.Order.Positive.Ring import Mathlib.Algebra.Order.Rearrangement diff --git a/Mathlib/Algebra/Bounds.lean b/Mathlib/Algebra/Bounds.lean deleted file mode 100644 index 8c9ff1cb53079..0000000000000 --- a/Mathlib/Algebra/Bounds.lean +++ /dev/null @@ -1,167 +0,0 @@ -/- -Copyright (c) 2021 Yury Kudryashov. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Yury Kudryashov --/ -import Mathlib.Algebra.Group.Pointwise.Set -import Mathlib.Algebra.Order.Group.OrderIso -import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual -import Mathlib.Order.Bounds.OrderIso -import Mathlib.Order.ConditionallyCompleteLattice.Basic - -/-! -# Upper/lower bounds in ordered monoids and groups - -In this file we prove a few facts like “`-s` is bounded above iff `s` is bounded below” -(`bddAbove_neg`). --/ - - -open Function Set - -open Pointwise - -section InvNeg - -variable {G : Type*} [Group G] [Preorder G] [CovariantClass G G (· * ·) (· ≤ ·)] - [CovariantClass G G (swap (· * ·)) (· ≤ ·)] {s : Set G} {a : G} - -@[to_additive (attr := simp)] -theorem bddAbove_inv : BddAbove s⁻¹ ↔ BddBelow s := - (OrderIso.inv G).bddAbove_preimage - -@[to_additive (attr := simp)] -theorem bddBelow_inv : BddBelow s⁻¹ ↔ BddAbove s := - (OrderIso.inv G).bddBelow_preimage - -@[to_additive] -theorem BddAbove.inv (h : BddAbove s) : BddBelow s⁻¹ := - bddBelow_inv.2 h - -@[to_additive] -theorem BddBelow.inv (h : BddBelow s) : BddAbove s⁻¹ := - bddAbove_inv.2 h - -@[to_additive (attr := simp)] -theorem isLUB_inv : IsLUB s⁻¹ a ↔ IsGLB s a⁻¹ := - (OrderIso.inv G).isLUB_preimage - -@[to_additive] -theorem isLUB_inv' : IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a := - (OrderIso.inv G).isLUB_preimage' - -@[to_additive] -theorem IsGLB.inv (h : IsGLB s a) : IsLUB s⁻¹ a⁻¹ := - isLUB_inv'.2 h - -@[to_additive (attr := simp)] -theorem isGLB_inv : IsGLB s⁻¹ a ↔ IsLUB s a⁻¹ := - (OrderIso.inv G).isGLB_preimage - -@[to_additive] -theorem isGLB_inv' : IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a := - (OrderIso.inv G).isGLB_preimage' - -@[to_additive] -theorem IsLUB.inv (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹ := - isGLB_inv'.2 h - -@[to_additive] -lemma BddBelow.range_inv {α : Type*} {f : α → G} (hf : BddBelow (range f)) : - BddAbove (range (fun x => (f x)⁻¹)) := - hf.range_comp (OrderIso.inv G).monotone - -@[to_additive] -lemma BddAbove.range_inv {α : Type*} {f : α → G} (hf : BddAbove (range f)) : - BddBelow (range (fun x => (f x)⁻¹)) := - BddBelow.range_inv (G := Gᵒᵈ) hf - -end InvNeg - -section mul_add - -variable {M : Type*} [Mul M] [Preorder M] [CovariantClass M M (· * ·) (· ≤ ·)] - [CovariantClass M M (swap (· * ·)) (· ≤ ·)] - -@[to_additive] -theorem mul_mem_upperBounds_mul {s t : Set M} {a b : M} (ha : a ∈ upperBounds s) - (hb : b ∈ upperBounds t) : a * b ∈ upperBounds (s * t) := - forall_image2_iff.2 fun _ hx _ hy => mul_le_mul' (ha hx) (hb hy) - -@[to_additive] -theorem subset_upperBounds_mul (s t : Set M) : - upperBounds s * upperBounds t ⊆ upperBounds (s * t) := - image2_subset_iff.2 fun _ hx _ hy => mul_mem_upperBounds_mul hx hy - -@[to_additive] -theorem mul_mem_lowerBounds_mul {s t : Set M} {a b : M} (ha : a ∈ lowerBounds s) - (hb : b ∈ lowerBounds t) : a * b ∈ lowerBounds (s * t) := - mul_mem_upperBounds_mul (M := Mᵒᵈ) ha hb - -@[to_additive] -theorem subset_lowerBounds_mul (s t : Set M) : - lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t) := - subset_upperBounds_mul (M := Mᵒᵈ) _ _ - -@[to_additive] -theorem BddAbove.mul {s t : Set M} (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) := - (Nonempty.mul hs ht).mono (subset_upperBounds_mul s t) - -@[to_additive] -theorem BddBelow.mul {s t : Set M} (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) := - (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t) - -@[to_additive] -lemma BddAbove.range_mul {α : Type*} {f g : α → M} (hf : BddAbove (range f)) - (hg : BddAbove (range g)) : BddAbove (range (fun x => f x * g x)) := - BddAbove.range_comp (f := fun x => (⟨f x, g x⟩ : M × M)) - (bddAbove_range_prod.mpr ⟨hf, hg⟩) (Monotone.mul' monotone_fst monotone_snd) - -@[to_additive] -lemma BddBelow.range_mul {α : Type*} {f g : α → M} (hf : BddBelow (range f)) - (hg : BddBelow (range g)) : BddBelow (range (fun x => f x * g x)) := - BddAbove.range_mul (M := Mᵒᵈ) hf hg - -end mul_add - -section ConditionallyCompleteLattice - -section Right - -variable {ι G : Type*} [Group G] [ConditionallyCompleteLattice G] - [CovariantClass G G (Function.swap (· * ·)) (· ≤ ·)] [Nonempty ι] {f : ι → G} - -@[to_additive] -theorem ciSup_mul (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a := - (OrderIso.mulRight a).map_ciSup hf - -@[to_additive] -theorem ciSup_div (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by - simp only [div_eq_mul_inv, ciSup_mul hf] - -@[to_additive] -theorem ciInf_mul (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) * a = ⨅ i, f i * a := - (OrderIso.mulRight a).map_ciInf hf - -@[to_additive] -theorem ciInf_div (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f i / a := by - simp only [div_eq_mul_inv, ciInf_mul hf] - -end Right - -section Left - -variable {ι : Sort*} {G : Type*} [Group G] [ConditionallyCompleteLattice G] - [CovariantClass G G (· * ·) (· ≤ ·)] [Nonempty ι] {f : ι → G} - -@[to_additive] -theorem mul_ciSup (hf : BddAbove (range f)) (a : G) : (a * ⨆ i, f i) = ⨆ i, a * f i := - (OrderIso.mulLeft a).map_ciSup hf - -@[to_additive] -theorem mul_ciInf (hf : BddBelow (range f)) (a : G) : (a * ⨅ i, f i) = ⨅ i, a * f i := - (OrderIso.mulLeft a).map_ciInf hf - -end Left - -end ConditionallyCompleteLattice diff --git a/Mathlib/Algebra/Order/CompleteField.lean b/Mathlib/Algebra/Order/CompleteField.lean index 2c8942e53c15c..680ebceb3f631 100644 --- a/Mathlib/Algebra/Order/CompleteField.lean +++ b/Mathlib/Algebra/Order/CompleteField.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Alex J. Best, Yaël Dillies -/ import Mathlib.Algebra.Order.Archimedean.Hom -import Mathlib.Algebra.Order.Pointwise +import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice import Mathlib.Analysis.SpecialFunctions.Pow.Real /-! diff --git a/Mathlib/Algebra/Order/Field/Pointwise.lean b/Mathlib/Algebra/Order/Field/Pointwise.lean new file mode 100644 index 0000000000000..8f2b1867f0d73 --- /dev/null +++ b/Mathlib/Algebra/Order/Field/Pointwise.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2021 Alex J. Best. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Alex J. Best, Yaël Dillies +-/ +import Mathlib.Algebra.Group.Pointwise.Set +import Mathlib.Algebra.Order.Field.Basic +import Mathlib.Algebra.SMulWithZero + +/-! +# Pointwise operations on ordered algebraic objects + +This file contains lemmas about the effect of pointwise operations on sets with an order structure. +-/ + +open Function Set +open scoped Pointwise + +variable {α : Type*} + +namespace LinearOrderedField + +variable {K : Type*} [LinearOrderedField K] {a b r : K} (hr : 0 < r) +include hr + +theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by + ext x + simp only [mem_smul_set, smul_eq_mul, mem_Ioo] + constructor + · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩ + constructor + · exact (mul_lt_mul_left hr).mpr a_h_left_left + · exact (mul_lt_mul_left hr).mpr a_h_left_right + · rintro ⟨a_left, a_right⟩ + use x / r + refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩ + rw [mul_div_cancel₀ _ (ne_of_gt hr)] + +theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by + ext x + simp only [mem_smul_set, smul_eq_mul, mem_Icc] + constructor + · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩ + constructor + · exact (mul_le_mul_left hr).mpr a_h_left_left + · exact (mul_le_mul_left hr).mpr a_h_left_right + · rintro ⟨a_left, a_right⟩ + use x / r + refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩ + rw [mul_div_cancel₀ _ (ne_of_gt hr)] + +theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by + ext x + simp only [mem_smul_set, smul_eq_mul, mem_Ico] + constructor + · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩ + constructor + · exact (mul_le_mul_left hr).mpr a_h_left_left + · exact (mul_lt_mul_left hr).mpr a_h_left_right + · rintro ⟨a_left, a_right⟩ + use x / r + refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩ + rw [mul_div_cancel₀ _ (ne_of_gt hr)] + +theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by + ext x + simp only [mem_smul_set, smul_eq_mul, mem_Ioc] + constructor + · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩ + constructor + · exact (mul_lt_mul_left hr).mpr a_h_left_left + · exact (mul_le_mul_left hr).mpr a_h_left_right + · rintro ⟨a_left, a_right⟩ + use x / r + refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩ + rw [mul_div_cancel₀ _ (ne_of_gt hr)] + +theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by + ext x + simp only [mem_smul_set, smul_eq_mul, mem_Ioi] + constructor + · rintro ⟨a_w, a_h_left, rfl⟩ + exact (mul_lt_mul_left hr).mpr a_h_left + · rintro h + use x / r + constructor + · exact (lt_div_iff' hr).mpr h + · exact mul_div_cancel₀ _ (ne_of_gt hr) + +theorem smul_Iio : r • Iio a = Iio (r • a) := by + ext x + simp only [mem_smul_set, smul_eq_mul, mem_Iio] + constructor + · rintro ⟨a_w, a_h_left, rfl⟩ + exact (mul_lt_mul_left hr).mpr a_h_left + · rintro h + use x / r + constructor + · exact (div_lt_iff' hr).mpr h + · exact mul_div_cancel₀ _ (ne_of_gt hr) + +theorem smul_Ici : r • Ici a = Ici (r • a) := by + ext x + simp only [mem_smul_set, smul_eq_mul, mem_Ioi] + constructor + · rintro ⟨a_w, a_h_left, rfl⟩ + exact (mul_le_mul_left hr).mpr a_h_left + · rintro h + use x / r + constructor + · exact (le_div_iff₀' hr).mpr h + · exact mul_div_cancel₀ _ (ne_of_gt hr) + +theorem smul_Iic : r • Iic a = Iic (r • a) := by + ext x + simp only [mem_smul_set, smul_eq_mul, mem_Iio] + constructor + · rintro ⟨a_w, a_h_left, rfl⟩ + exact (mul_le_mul_left hr).mpr a_h_left + · rintro h + use x / r + constructor + · exact (div_le_iff₀' hr).mpr h + · exact mul_div_cancel₀ _ (ne_of_gt hr) + +end LinearOrderedField diff --git a/Mathlib/Algebra/Order/Group/CompleteLattice.lean b/Mathlib/Algebra/Order/Group/CompleteLattice.lean new file mode 100644 index 0000000000000..19c8f5fda8e68 --- /dev/null +++ b/Mathlib/Algebra/Order/Group/CompleteLattice.lean @@ -0,0 +1,49 @@ +/- +Copyright (c) 2021 Yury G. Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury G. Kudryashov +-/ +import Mathlib.Algebra.Order.Group.OrderIso +import Mathlib.Order.ConditionallyCompleteLattice.Basic + +/-! +# Distributivity of group operations over supremum/infimum +-/ + +open Function Set + +variable {ι G : Type*} [Group G] [ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G} + +section Right +variable [CovariantClass G G (swap (· * ·)) (· ≤ ·)] + +@[to_additive] +lemma ciSup_mul (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) * a = ⨆ i, f i * a := + (OrderIso.mulRight a).map_ciSup hf + +@[to_additive] +lemma ciSup_div (hf : BddAbove (range f)) (a : G) : (⨆ i, f i) / a = ⨆ i, f i / a := by + simp only [div_eq_mul_inv, ciSup_mul hf] + +@[to_additive] +lemma ciInf_mul (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) * a = ⨅ i, f i * a := + (OrderIso.mulRight a).map_ciInf hf + +@[to_additive] +lemma ciInf_div (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f i / a := by + simp only [div_eq_mul_inv, ciInf_mul hf] + +end Right + +section Left +variable [CovariantClass G G (· * ·) (· ≤ ·)] + +@[to_additive] +lemma mul_ciSup (hf : BddAbove (range f)) (a : G) : (a * ⨆ i, f i) = ⨆ i, a * f i := + (OrderIso.mulLeft a).map_ciSup hf + +@[to_additive] +lemma mul_ciInf (hf : BddBelow (range f)) (a : G) : (a * ⨅ i, f i) = ⨅ i, a * f i := + (OrderIso.mulLeft a).map_ciInf hf + +end Left diff --git a/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean new file mode 100644 index 0000000000000..e6a5407931b80 --- /dev/null +++ b/Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) 2021 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov +-/ +import Mathlib.Algebra.Group.Pointwise.Set +import Mathlib.Algebra.Order.Group.OrderIso +import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual +import Mathlib.Order.Bounds.OrderIso + +/-! +# Upper/lower bounds in ordered monoids and groups + +In this file we prove a few facts like “`-s` is bounded above iff `s` is bounded below” +(`bddAbove_neg`). +-/ + +open Function Set +open scoped Pointwise + +variable {ι G M : Type*} + +section Mul +variable [Mul M] [Preorder M] [CovariantClass M M (· * ·) (· ≤ ·)] + [CovariantClass M M (swap (· * ·)) (· ≤ ·)] {f g : ι → M} {s t : Set M} {a b : M} + +@[to_additive] +lemma mul_mem_upperBounds_mul (ha : a ∈ upperBounds s) (hb : b ∈ upperBounds t) : + a * b ∈ upperBounds (s * t) := forall_image2_iff.2 fun _ hx _ hy => mul_le_mul' (ha hx) (hb hy) + +@[to_additive] +lemma subset_upperBounds_mul (s t : Set M) : upperBounds s * upperBounds t ⊆ upperBounds (s * t) := + image2_subset_iff.2 fun _ hx _ hy => mul_mem_upperBounds_mul hx hy + +@[to_additive] +lemma mul_mem_lowerBounds_mul (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) : + a * b ∈ lowerBounds (s * t) := mul_mem_upperBounds_mul (M := Mᵒᵈ) ha hb + +@[to_additive] +lemma subset_lowerBounds_mul (s t : Set M) : lowerBounds s * lowerBounds t ⊆ lowerBounds (s * t) := + subset_upperBounds_mul (M := Mᵒᵈ) _ _ + +@[to_additive] +lemma BddAbove.mul (hs : BddAbove s) (ht : BddAbove t) : BddAbove (s * t) := + (Nonempty.mul hs ht).mono (subset_upperBounds_mul s t) + +@[to_additive] +lemma BddBelow.mul (hs : BddBelow s) (ht : BddBelow t) : BddBelow (s * t) := + (Nonempty.mul hs ht).mono (subset_lowerBounds_mul s t) + +@[to_additive] +lemma BddAbove.range_mul (hf : BddAbove (range f)) (hg : BddAbove (range g)) : + BddAbove (range fun i ↦ f i * g i) := + .range_comp (f := fun i ↦ (f i, g i)) (bddAbove_range_prod.2 ⟨hf, hg⟩) + (monotone_fst.mul' monotone_snd) + +@[to_additive] +lemma BddBelow.range_mul (hf : BddBelow (range f)) (hg : BddBelow (range g)) : + BddBelow (range fun i ↦ f i * g i) := BddAbove.range_mul (M := Mᵒᵈ) hf hg + +end Mul + +section InvNeg +variable [Group G] [Preorder G] [CovariantClass G G (· * ·) (· ≤ ·)] + [CovariantClass G G (swap (· * ·)) (· ≤ ·)] {s : Set G} {a : G} + +@[to_additive (attr := simp)] +theorem bddAbove_inv : BddAbove s⁻¹ ↔ BddBelow s := + (OrderIso.inv G).bddAbove_preimage + +@[to_additive (attr := simp)] +theorem bddBelow_inv : BddBelow s⁻¹ ↔ BddAbove s := + (OrderIso.inv G).bddBelow_preimage + +@[to_additive] +theorem BddAbove.inv (h : BddAbove s) : BddBelow s⁻¹ := + bddBelow_inv.2 h + +@[to_additive] +theorem BddBelow.inv (h : BddBelow s) : BddAbove s⁻¹ := + bddAbove_inv.2 h + +@[to_additive (attr := simp)] +theorem isLUB_inv : IsLUB s⁻¹ a ↔ IsGLB s a⁻¹ := + (OrderIso.inv G).isLUB_preimage + +@[to_additive] +theorem isLUB_inv' : IsLUB s⁻¹ a⁻¹ ↔ IsGLB s a := + (OrderIso.inv G).isLUB_preimage' + +@[to_additive] +theorem IsGLB.inv (h : IsGLB s a) : IsLUB s⁻¹ a⁻¹ := + isLUB_inv'.2 h + +@[to_additive (attr := simp)] +theorem isGLB_inv : IsGLB s⁻¹ a ↔ IsLUB s a⁻¹ := + (OrderIso.inv G).isGLB_preimage + +@[to_additive] +theorem isGLB_inv' : IsGLB s⁻¹ a⁻¹ ↔ IsLUB s a := + (OrderIso.inv G).isGLB_preimage' + +@[to_additive] +theorem IsLUB.inv (h : IsLUB s a) : IsGLB s⁻¹ a⁻¹ := + isGLB_inv'.2 h + +@[to_additive] +lemma BddBelow.range_inv {α : Type*} {f : α → G} (hf : BddBelow (range f)) : + BddAbove (range (fun x => (f x)⁻¹)) := + hf.range_comp (OrderIso.inv G).monotone + +@[to_additive] +lemma BddAbove.range_inv {α : Type*} {f : α → G} (hf : BddAbove (range f)) : + BddBelow (range (fun x => (f x)⁻¹)) := + BddBelow.range_inv (G := Gᵒᵈ) hf + +end InvNeg diff --git a/Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean b/Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean new file mode 100644 index 0000000000000..6f09d373cffd4 --- /dev/null +++ b/Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) 2021 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov +-/ +import Mathlib.Algebra.Order.Group.Pointwise.Bounds +import Mathlib.Order.ConditionallyCompleteLattice.Basic + +/-! +# Infima/suprema in ordered monoids and groups + +In this file we prove a few facts like “The infimum of `-s` is `-` the supremum of `s`”. + +## TODO + +`sSup (s • t) = sSup s • sSup t` and `sInf (s • t) = sInf s • sInf t` hold as well but +`CovariantClass` is currently not polymorphic enough to state it. +-/ + +open Function Set +open scoped Pointwise + +variable {ι G M : Type*} + +section ConditionallyCompleteLattice +variable [ConditionallyCompleteLattice M] + +section One +variable [One M] + +@[to_additive (attr := simp)] lemma csSup_one : sSup (1 : Set M) = 1 := csSup_singleton _ +@[to_additive (attr := simp)] lemma csInf_one : sInf (1 : Set M) = 1 := csInf_singleton _ + +end One + +section Group +variable [Group M] [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)] + {s t : Set M} + +@[to_additive] +lemma csSup_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : sSup s⁻¹ = (sInf s)⁻¹ := by + rw [← image_inv] + exact ((OrderIso.inv _).map_csInf' hs₀ hs₁).symm + +@[to_additive] +lemma csInf_inv (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sInf s⁻¹ = (sSup s)⁻¹ := by + rw [← image_inv] + exact ((OrderIso.inv _).map_csSup' hs₀ hs₁).symm + +@[to_additive] +lemma csSup_mul (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : + sSup (s * t) = sSup s * sSup t := + csSup_image2_eq_csSup_csSup (fun _ => (OrderIso.mulRight _).to_galoisConnection) + (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs₀ hs₁ ht₀ ht₁ + +@[to_additive] +lemma csInf_mul (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : + sInf (s * t) = sInf s * sInf t := + csInf_image2_eq_csInf_csInf (fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) + (fun _ => (OrderIso.mulLeft _).symm.to_galoisConnection) hs₀ hs₁ ht₀ ht₁ + +@[to_additive] +lemma csSup_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : + sSup (s / t) = sSup s / sInf t := by + rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv] + +@[to_additive] +lemma csInf_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : + sInf (s / t) = sInf s / sSup t := by + rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv] + +end Group +end ConditionallyCompleteLattice + +section CompleteLattice +variable [CompleteLattice M] + +section One +variable [One M] + +@[to_additive] lemma sSup_one : sSup (1 : Set M) = 1 := sSup_singleton +@[to_additive] lemma sInf_one : sInf (1 : Set M) = 1 := sInf_singleton + +end One + +section Group +variable [Group M] [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)] + (s t : Set M) + +@[to_additive] +lemma sSup_inv (s : Set M) : sSup s⁻¹ = (sInf s)⁻¹ := by + rw [← image_inv, sSup_image] + exact ((OrderIso.inv M).map_sInf _).symm + +@[to_additive] +lemma sInf_inv (s : Set M) : sInf s⁻¹ = (sSup s)⁻¹ := by + rw [← image_inv, sInf_image] + exact ((OrderIso.inv M).map_sSup _).symm + +@[to_additive] +lemma sSup_mul : sSup (s * t) = sSup s * sSup t := + (sSup_image2_eq_sSup_sSup fun _ => (OrderIso.mulRight _).to_galoisConnection) fun _ => + (OrderIso.mulLeft _).to_galoisConnection + +@[to_additive] +lemma sInf_mul : sInf (s * t) = sInf s * sInf t := + (sInf_image2_eq_sInf_sInf fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) fun _ => + (OrderIso.mulLeft _).symm.to_galoisConnection + +@[to_additive] +lemma sSup_div : sSup (s / t) = sSup s / sInf t := by simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv] + +@[to_additive] +lemma sInf_div : sInf (s / t) = sInf s / sSup t := by simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv] + +end Group +end CompleteLattice diff --git a/Mathlib/Algebra/Order/Pointwise.lean b/Mathlib/Algebra/Order/Pointwise.lean deleted file mode 100644 index 5a6d4539414dd..0000000000000 --- a/Mathlib/Algebra/Order/Pointwise.lean +++ /dev/null @@ -1,250 +0,0 @@ -/- -Copyright (c) 2021 Alex J. Best. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alex J. Best, Yaël Dillies --/ -import Mathlib.Algebra.Bounds -import Mathlib.Algebra.Order.Field.Basic -- Porting note: `LinearOrderedField`, etc -import Mathlib.Algebra.SMulWithZero - -/-! -# Pointwise operations on ordered algebraic objects - -This file contains lemmas about the effect of pointwise operations on sets with an order structure. - -## TODO - -`sSup (s • t) = sSup s • sSup t` and `sInf (s • t) = sInf s • sInf t` hold as well but -`CovariantClass` is currently not polymorphic enough to state it. --/ - - -open Function Set - -open Pointwise - -variable {α : Type*} - --- Porting note: Swapped the place of `CompleteLattice` and `ConditionallyCompleteLattice` --- due to simpNF problem between `sSup_xx` `csSup_xx`. - -section CompleteLattice - -variable [CompleteLattice α] - -section One - -variable [One α] - -@[to_additive (attr := simp)] -theorem sSup_one : sSup (1 : Set α) = 1 := - sSup_singleton - -@[to_additive (attr := simp)] -theorem sInf_one : sInf (1 : Set α) = 1 := - sInf_singleton - -end One - -section Group - -variable [Group α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)] - (s t : Set α) - -@[to_additive] -theorem sSup_inv (s : Set α) : sSup s⁻¹ = (sInf s)⁻¹ := by - rw [← image_inv, sSup_image] - exact ((OrderIso.inv α).map_sInf _).symm - -@[to_additive] -theorem sInf_inv (s : Set α) : sInf s⁻¹ = (sSup s)⁻¹ := by - rw [← image_inv, sInf_image] - exact ((OrderIso.inv α).map_sSup _).symm - -@[to_additive] -theorem sSup_mul : sSup (s * t) = sSup s * sSup t := - (sSup_image2_eq_sSup_sSup fun _ => (OrderIso.mulRight _).to_galoisConnection) fun _ => - (OrderIso.mulLeft _).to_galoisConnection - -@[to_additive] -theorem sInf_mul : sInf (s * t) = sInf s * sInf t := - (sInf_image2_eq_sInf_sInf fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) fun _ => - (OrderIso.mulLeft _).symm.to_galoisConnection - -@[to_additive] -theorem sSup_div : sSup (s / t) = sSup s / sInf t := by simp_rw [div_eq_mul_inv, sSup_mul, sSup_inv] - -@[to_additive] -theorem sInf_div : sInf (s / t) = sInf s / sSup t := by simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv] - -end Group - -end CompleteLattice - -section ConditionallyCompleteLattice - -variable [ConditionallyCompleteLattice α] - -section One - -variable [One α] - -@[to_additive (attr := simp)] -theorem csSup_one : sSup (1 : Set α) = 1 := - csSup_singleton _ - -@[to_additive (attr := simp)] -theorem csInf_one : sInf (1 : Set α) = 1 := - csInf_singleton _ - -end One - -section Group - -variable [Group α] [CovariantClass α α (· * ·) (· ≤ ·)] [CovariantClass α α (swap (· * ·)) (· ≤ ·)] - {s t : Set α} - -@[to_additive] -theorem csSup_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : sSup s⁻¹ = (sInf s)⁻¹ := by - rw [← image_inv] - exact ((OrderIso.inv α).map_csInf' hs₀ hs₁).symm - -@[to_additive] -theorem csInf_inv (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sInf s⁻¹ = (sSup s)⁻¹ := by - rw [← image_inv] - exact ((OrderIso.inv α).map_csSup' hs₀ hs₁).symm - -@[to_additive] -theorem csSup_mul (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : - sSup (s * t) = sSup s * sSup t := - csSup_image2_eq_csSup_csSup (fun _ => (OrderIso.mulRight _).to_galoisConnection) - (fun _ => (OrderIso.mulLeft _).to_galoisConnection) hs₀ hs₁ ht₀ ht₁ - -@[to_additive] -theorem csInf_mul (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : - sInf (s * t) = sInf s * sInf t := - csInf_image2_eq_csInf_csInf (fun _ => (OrderIso.mulRight _).symm.to_galoisConnection) - (fun _ => (OrderIso.mulLeft _).symm.to_galoisConnection) hs₀ hs₁ ht₀ ht₁ - -@[to_additive] -theorem csSup_div (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : - sSup (s / t) = sSup s / sInf t := by - rw [div_eq_mul_inv, csSup_mul hs₀ hs₁ ht₀.inv ht₁.inv, csSup_inv ht₀ ht₁, div_eq_mul_inv] - -@[to_additive] -theorem csInf_div (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : - sInf (s / t) = sInf s / sSup t := by - rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv] - -end Group - -end ConditionallyCompleteLattice - -namespace LinearOrderedField - -variable {K : Type*} [LinearOrderedField K] {a b r : K} (hr : 0 < r) -include hr - -open Set - -theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by - ext x - simp only [mem_smul_set, smul_eq_mul, mem_Ioo] - constructor - · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩ - constructor - · exact (mul_lt_mul_left hr).mpr a_h_left_left - · exact (mul_lt_mul_left hr).mpr a_h_left_right - · rintro ⟨a_left, a_right⟩ - use x / r - refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩ - rw [mul_div_cancel₀ _ (ne_of_gt hr)] - -theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by - ext x - simp only [mem_smul_set, smul_eq_mul, mem_Icc] - constructor - · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩ - constructor - · exact (mul_le_mul_left hr).mpr a_h_left_left - · exact (mul_le_mul_left hr).mpr a_h_left_right - · rintro ⟨a_left, a_right⟩ - use x / r - refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩ - rw [mul_div_cancel₀ _ (ne_of_gt hr)] - -theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by - ext x - simp only [mem_smul_set, smul_eq_mul, mem_Ico] - constructor - · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩ - constructor - · exact (mul_le_mul_left hr).mpr a_h_left_left - · exact (mul_lt_mul_left hr).mpr a_h_left_right - · rintro ⟨a_left, a_right⟩ - use x / r - refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩ - rw [mul_div_cancel₀ _ (ne_of_gt hr)] - -theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by - ext x - simp only [mem_smul_set, smul_eq_mul, mem_Ioc] - constructor - · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩ - constructor - · exact (mul_lt_mul_left hr).mpr a_h_left_left - · exact (mul_le_mul_left hr).mpr a_h_left_right - · rintro ⟨a_left, a_right⟩ - use x / r - refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩ - rw [mul_div_cancel₀ _ (ne_of_gt hr)] - -theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by - ext x - simp only [mem_smul_set, smul_eq_mul, mem_Ioi] - constructor - · rintro ⟨a_w, a_h_left, rfl⟩ - exact (mul_lt_mul_left hr).mpr a_h_left - · rintro h - use x / r - constructor - · exact (lt_div_iff' hr).mpr h - · exact mul_div_cancel₀ _ (ne_of_gt hr) - -theorem smul_Iio : r • Iio a = Iio (r • a) := by - ext x - simp only [mem_smul_set, smul_eq_mul, mem_Iio] - constructor - · rintro ⟨a_w, a_h_left, rfl⟩ - exact (mul_lt_mul_left hr).mpr a_h_left - · rintro h - use x / r - constructor - · exact (div_lt_iff' hr).mpr h - · exact mul_div_cancel₀ _ (ne_of_gt hr) - -theorem smul_Ici : r • Ici a = Ici (r • a) := by - ext x - simp only [mem_smul_set, smul_eq_mul, mem_Ioi] - constructor - · rintro ⟨a_w, a_h_left, rfl⟩ - exact (mul_le_mul_left hr).mpr a_h_left - · rintro h - use x / r - constructor - · exact (le_div_iff₀' hr).mpr h - · exact mul_div_cancel₀ _ (ne_of_gt hr) - -theorem smul_Iic : r • Iic a = Iic (r • a) := by - ext x - simp only [mem_smul_set, smul_eq_mul, mem_Iio] - constructor - · rintro ⟨a_w, a_h_left, rfl⟩ - exact (mul_le_mul_left hr).mpr a_h_left - · rintro h - use x / r - constructor - · exact (div_le_iff₀' hr).mpr h - · exact mul_div_cancel₀ _ (ne_of_gt hr) - -end LinearOrderedField diff --git a/Mathlib/Data/Real/Archimedean.lean b/Mathlib/Data/Real/Archimedean.lean index 320d601909bab..4df84980d7abb 100644 --- a/Mathlib/Data/Real/Archimedean.lean +++ b/Mathlib/Data/Real/Archimedean.lean @@ -3,8 +3,8 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Floris van Doorn -/ -import Mathlib.Algebra.Bounds import Mathlib.Algebra.Order.Archimedean.Basic +import Mathlib.Algebra.Order.Group.Pointwise.Bounds import Mathlib.Data.Real.Basic import Mathlib.Order.Interval.Set.Disjoint diff --git a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean index 9326504897129..76566b1a9cc1e 100644 --- a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean +++ b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean @@ -3,7 +3,7 @@ Copyright (c) 2023 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury Kudryashov -/ -import Mathlib.Algebra.Order.Pointwise +import Mathlib.Algebra.Order.Field.Pointwise import Mathlib.Analysis.NormedSpace.SphereNormEquiv import Mathlib.Analysis.SpecialFunctions.Integrals import Mathlib.MeasureTheory.Constructions.Prod.Integral From 3488c1c235662ef6ff164df38d9cadd6a1e48888 Mon Sep 17 00:00:00 2001 From: Emily Riehl Date: Thu, 26 Sep 2024 00:42:52 +0000 Subject: [PATCH 4/9] feat(CategoryTheory): the internal hom with the monoidal unit is the identity (#17065) In a closed monoidal category, the internal hom defined by mapping out of the monoidal unit is naturally isomorphic to the identity. This specializes to an analogous result about exponentiating with the terminal object in a cartesian closed category. Co-authored-by: [Dagur Asgeirsson](https://github.com/dagurtomas) --- Mathlib/CategoryTheory/Closed/Cartesian.lean | 20 +++++++------------- Mathlib/CategoryTheory/Closed/Monoidal.lean | 4 ++++ 2 files changed, 11 insertions(+), 13 deletions(-) diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean index c4ac634c52efb..e25efebbe63d0 100644 --- a/Mathlib/CategoryTheory/Closed/Cartesian.lean +++ b/Mathlib/CategoryTheory/Closed/Cartesian.lean @@ -226,21 +226,15 @@ end CartesianClosed open CartesianClosed -/-- Show that the exponential of the terminal object is isomorphic to itself, i.e. `X^1 ≅ X`. +/-- The exponential with the terminal object is naturally isomorphic to the identity. The typeclass +argument is explicit: any instance can be used.-/ +def expTerminalNatIso [Exponentiable (⊤_ C)] : 𝟭 C ≅ exp (⊤_ C) := + MonoidalClosed.unitNatIso (C := C) -The typeclass argument is explicit: any instance can be used. --/ +/-- The exponential of any object with the terminal object is isomorphic to itself, i.e. `X^1 ≅ X`. +The typeclass argument is explicit: any instance can be used.-/ def expTerminalIsoSelf [Exponentiable (⊤_ C)] : (⊤_ C) ⟹ X ≅ X := - Yoneda.ext ((⊤_ C) ⟹ X) X - (fun {Y} f => (Limits.prod.leftUnitor Y).inv ≫ CartesianClosed.uncurry f) - (fun {Y} f => CartesianClosed.curry ((Limits.prod.leftUnitor Y).hom ≫ f)) - (fun g => by - rw [curry_eq_iff, Iso.hom_inv_id_assoc]) - (fun g => by simp) - (fun f g => by - -- Porting note: `rw` is a bit brittle here, requiring the `dsimp` rule cancellation. - dsimp [-prod.leftUnitor_inv] - rw [uncurry_natural_left, prod.leftUnitor_inv_naturality_assoc f]) + (expTerminalNatIso.app X).symm /-- The internal element which points at the given morphism. -/ def internalizeHom (f : A ⟶ Y) : ⊤_ C ⟶ A ⟹ Y := diff --git a/Mathlib/CategoryTheory/Closed/Monoidal.lean b/Mathlib/CategoryTheory/Closed/Monoidal.lean index 8309157796ab1..43af4d461c0de 100644 --- a/Mathlib/CategoryTheory/Closed/Monoidal.lean +++ b/Mathlib/CategoryTheory/Closed/Monoidal.lean @@ -196,6 +196,10 @@ theorem curry_id_eq_coev : curry (𝟙 _) = (ihom.coev A).app X := by rw [curry_eq, (ihom A).map_id (A ⊗ _)] apply comp_id +/-- The internal hom out of the unit is naturally isomorphic to the identity functor.-/ +def unitNatIso [Closed (𝟙_ C)] : 𝟭 C ≅ ihom (𝟙_ C) := + conjugateIsoEquiv (Adjunction.id (C := C)) (ihom.adjunction (𝟙_ C)) + (leftUnitorNatIso C) section Pre variable {A B} From b272ab87df83543439885eb390ff5aa07a78777d Mon Sep 17 00:00:00 2001 From: Ira Fesefeldt Date: Thu, 26 Sep 2024 02:42:15 +0000 Subject: [PATCH 5/9] feat: monotonicity lemmas for OrdinalApprox (#15522) This PR adds two lemmas about monotonicity for `lfpApprox` and `gfpApprox` each. I found them helpful when working with the API. Co-authored-by: Ira Fesefeldt Co-authored-by: Ira Fesefeldt <9974411+PhoenixIra@users.noreply.github.com> --- .../Ordinal/FixedPointApproximants.lean | 58 +++++++++++++++---- 1 file changed, 48 insertions(+), 10 deletions(-) diff --git a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean index e7baa70d5b32b..ddec8ac7b3058 100644 --- a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean +++ b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean @@ -54,8 +54,6 @@ theorem not_injective_limitation_set : ¬ InjOn g (Iio (ord <| succ #α)) := by rw [mk_initialSeg_subtype, lift_lift, lift_le] at h exact not_le_of_lt (Order.lt_succ #α) h - - end Cardinal namespace OrdinalApprox @@ -76,7 +74,8 @@ termination_by a decreasing_by exact h theorem lfpApprox_monotone : Monotone (lfpApprox f x) := by - unfold Monotone; intros a b h; unfold lfpApprox + intros a b h + rw [lfpApprox, lfpApprox] refine sSup_le_sSup ?h apply sup_le_sup_right simp only [exists_prop, Set.le_eq_subset, Set.setOf_subset_setOf, forall_exists_index, and_imp, @@ -86,14 +85,14 @@ theorem lfpApprox_monotone : Monotone (lfpApprox f x) := by exact ⟨lt_of_lt_of_le h' h, rfl⟩ theorem le_lfpApprox {a : Ordinal} : x ≤ lfpApprox f x a := by - unfold lfpApprox + rw [lfpApprox] apply le_sSup simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, true_or] theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) : lfpApprox f x (a+1) = f (lfpApprox f x a) := by apply le_antisymm - · conv => left; unfold lfpApprox + · conv => left; rw [lfpApprox] apply sSup_le simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, forall_eq_or_imp, forall_exists_index, and_imp, @@ -104,7 +103,7 @@ theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) : exact le_lfpApprox f x · intros a' h apply f.2; apply lfpApprox_monotone; exact h - · conv => right; unfold lfpApprox + · conv => right; rw [lfpApprox] apply le_sSup simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop] rw [Set.mem_union] @@ -112,13 +111,46 @@ theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) : simp only [Set.mem_setOf_eq] use a +theorem lfpApprox_mono_left : Monotone (lfpApprox : (α →o α) → _) := by + intro f g h x a + induction a using Ordinal.induction with + | h i ih => + rw [lfpApprox, lfpApprox] + apply sSup_le + simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, sSup_insert, + forall_eq_or_imp, le_sup_left, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, + true_and] + intro i' h_lt + apply le_sup_of_le_right + apply le_sSup_of_le + · use i' + · apply le_trans (h _) + simp only [OrderHom.toFun_eq_coe] + exact g.monotone (ih i' h_lt) + +theorem lfpApprox_mono_mid : Monotone (lfpApprox f) := by + intro x₁ x₂ h a + induction a using Ordinal.induction with + | h i ih => + rw [lfpApprox, lfpApprox] + apply sSup_le + simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, sSup_insert, + forall_eq_or_imp, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] + constructor + · exact le_sup_of_le_left h + · intro i' h_i' + apply le_sup_of_le_right + apply le_sSup_of_le + · use i' + · exact f.monotone (ih i' h_i') + /-- The approximations of the least fixed point stabilize at a fixed point of `f` -/ theorem lfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : x ≤ f x) (h_ab : a ≤ b) (h : lfpApprox f x a ∈ fixedPoints f) : lfpApprox f x b = lfpApprox f x a := by rw [mem_fixedPoints_iff] at h induction b using Ordinal.induction with | h b IH => apply le_antisymm - · conv => left; unfold lfpApprox + · conv => left; rw [lfpApprox] apply sSup_le simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, forall_eq_or_imp, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] @@ -178,7 +210,7 @@ theorem lfpApprox_le_of_mem_fixedPoints {a : α} (h_a : a ∈ fixedPoints f) (h_le_init : x ≤ a) (i : Ordinal) : lfpApprox f x i ≤ a := by induction i using Ordinal.induction with | h i IH => - unfold lfpApprox + rw [lfpApprox] apply sSup_le simp only [exists_prop] intro y h_y @@ -187,8 +219,7 @@ theorem lfpApprox_le_of_mem_fixedPoints {a : α} | inl h_y => let ⟨j, h_j_lt, h_j⟩ := h_y rw [← h_j, ← h_a] - apply f.monotone' - exact IH j h_j_lt + exact f.monotone' (IH j h_j_lt) | inr h_y => rw [h_y] exact h_le_init @@ -234,6 +265,13 @@ theorem gfpApprox_add_one (h : f x ≤ x) (a : Ordinal) : gfpApprox f x (a+1) = f (gfpApprox f x a) := lfpApprox_add_one (OrderHom.dual f) x h a +theorem gfpApprox_mono_left : Monotone (gfpApprox : (α →o α) → _) := by + intro f g h + have : OrderHom.dual g ≤ OrderHom.dual f := h + exact lfpApprox_mono_left this + +theorem gfpApprox_mono_mid : Monotone (gfpApprox f) := + fun _ _ h => lfpApprox_mono_mid (OrderHom.dual f) h /-- The approximations of the greatest fixed point stabilize at a fixed point of `f` -/ theorem gfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : f x ≤ x) (h_ab : a ≤ b) From facf1f9c421d71ca630462709b7a4bd20638d451 Mon Sep 17 00:00:00 2001 From: Ahmad Alkhalawi Date: Thu, 26 Sep 2024 03:24:14 +0000 Subject: [PATCH 6/9] feat(LinearAlgebra/Matrix): Woodbury Identity (#16325) This adds the [Woodbury Identity](https://en.wikipedia.org/wiki/Woodbury_matrix_identity). [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Woodbury.20identity/near/462245284) Also corrects some bad deprecations introduced in #16590, which affected development of this PR. Co-authored-by: Mohanad Ahmad Co-authored-by: Eric Wieser --- Mathlib/Data/Matrix/Invertible.lean | 77 +++++++++++++++++-- .../Matrix/NonsingularInverse.lean | 18 +++++ 2 files changed, 90 insertions(+), 5 deletions(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index 5b38bcb33b6e3..b68c2fb925d3d 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -1,9 +1,10 @@ /- Copyright (c) 2023 Eric Wieser. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Eric Wieser +Authors: Eric Wieser, Ahmad Alkhalawi -/ import Mathlib.Data.Matrix.Basic +import Mathlib.Tactic.Abel /-! # Extra lemmas about invertible matrices @@ -47,10 +48,12 @@ protected theorem invOf_mul_cancel_right (A : Matrix m n α) (B : Matrix n n α) protected theorem mul_invOf_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] : A * B * ⅟ B = A := by rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one] -@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc := invOf_mul_cancel_left -@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc := mul_invOf_cancel_left -@[deprecated (since := "2024-09-07")] alias mul_invOf_mul_self_cancel := invOf_mul_cancel_right -@[deprecated (since := "2024-09-07")] alias mul_mul_invOf_self_cancel := mul_invOf_cancel_right +@[deprecated (since := "2024-09-07")] alias invOf_mul_self_assoc := Matrix.invOf_mul_cancel_left +@[deprecated (since := "2024-09-07")] alias mul_invOf_self_assoc := Matrix.mul_invOf_cancel_left +@[deprecated (since := "2024-09-07")] +alias mul_invOf_mul_self_cancel := Matrix.invOf_mul_cancel_right +@[deprecated (since := "2024-09-07")] +alias mul_mul_invOf_self_cancel := Matrix.mul_invOf_cancel_right section ConjTranspose variable [StarRing α] (A : Matrix n n α) @@ -106,4 +109,68 @@ def transposeInvertibleEquivInvertible : Invertible Aᵀ ≃ Invertible A where end CommSemiring +section Ring + +section Woodbury + +variable [Fintype m] [DecidableEq m] [Ring α] + (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) + [Invertible A] [Invertible C] [Invertible (⅟C + V * ⅟A * U)] + +-- No spaces around multiplication signs for better clarity +lemma add_mul_mul_invOf_mul_eq_one : + (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) = 1 := by + calc + (A + U*C*V)*(⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) + _ = A*⅟A - A*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A - U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by + simp_rw [add_sub_assoc, add_mul, mul_sub, Matrix.mul_assoc] + _ = (1 + U*C*V*⅟A) - (U*⅟(⅟C + V*⅟A*U)*V*⅟A + U*C*V*⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A) := by + rw [mul_invOf_self, Matrix.one_mul] + abel + _ = 1 + U*C*V*⅟A - (U + U*C*V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by + rw [sub_right_inj, Matrix.add_mul, Matrix.add_mul, Matrix.add_mul] + _ = 1 + U*C*V*⅟A - U*C*(⅟C + V*⅟A*U)*⅟(⅟C + V*⅟A*U)*V*⅟A := by + congr + simp only [Matrix.mul_add, Matrix.mul_invOf_cancel_right, ← Matrix.mul_assoc] + _ = 1 := by + rw [Matrix.mul_invOf_cancel_right] + abel + +/-- Like `add_mul_mul_invOf_mul_eq_one`, but with multiplication reversed. -/ +lemma add_mul_mul_invOf_mul_eq_one' : + (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V) = 1 := by + calc + (⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A)*(A + U*C*V) + _ = ⅟A*A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*A + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V := by + simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc] + _ = (1 + ⅟A*U*C*V) - (⅟A*U*⅟(⅟C + V*⅟A*U)*V + ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A*U*C*V) := by + rw [invOf_mul_self, Matrix.invOf_mul_cancel_right] + abel + _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(V + V*⅟A*U*C*V) := by + rw [sub_right_inj, Matrix.mul_add] + simp_rw [Matrix.mul_assoc] + _ = 1 + ⅟A*U*C*V - ⅟A*U*⅟(⅟C + V*⅟A*U)*(⅟C + V*⅟A*U)*C*V := by + congr 1 + simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc, + Matrix.invOf_mul_cancel_right] + _ = 1 := by + rw [Matrix.invOf_mul_cancel_right] + abel + +/-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A + U * C * V`-/ +def invertibleAddMulMul : Invertible (A + U*C*V) where + invOf := ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A + invOf_mul_self := add_mul_mul_invOf_mul_eq_one' _ _ _ _ + mul_invOf_self := add_mul_mul_invOf_mul_eq_one _ _ _ _ + +/-- The **Woodbury Identity** (`⅟` version). -/ +theorem invOf_add_mul_mul [Invertible (A + U*C*V)] : + ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A := by + letI := invertibleAddMulMul A U C V + convert (rfl : ⅟(A + U*C*V) = _) + +end Woodbury + +end Ring + end Matrix diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 0ba84d9e908d0..1482f940cd82d 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -607,6 +607,24 @@ theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse end Diagonal +section Woodbury + +variable [Fintype m] [DecidableEq m] +variable (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α) + +/-- The **Woodbury Identity** (`⁻¹` version). -/ +theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) : + (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹ := by + obtain ⟨_⟩ := hA.nonempty_invertible + obtain ⟨_⟩ := hC.nonempty_invertible + obtain ⟨iAC⟩ := hAC.nonempty_invertible + simp only [← invOf_eq_nonsing_inv] at iAC + letI := invertibleAddMulMul A U C V + simp only [← invOf_eq_nonsing_inv] + apply invOf_add_mul_mul + +end Woodbury + @[simp] theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ := by by_cases h : IsUnit A.det From c52d5a96ad8b3b9e7809cef5dd9eb3e4de7055ed Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Thu, 26 Sep 2024 04:36:13 +0000 Subject: [PATCH 7/9] =?UTF-8?q?chore:=20fix=20type=20class=20assumptions?= =?UTF-8?q?=20for=20`NonUnitalStarAlgHom.map=5Fcfc=E2=82=99`=20(#17111)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean index e5c7cea5ca34e..2895a56f474d3 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean @@ -428,9 +428,9 @@ open scoped ContinuousMapZero variable {F R S A B : Type*} {p : A → Prop} {q : B → Prop} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [TopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S] - [Ring A] [StarRing A] [TopologicalSpace A] [Module R A] + [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] - [Ring B] [StarRing B] [TopologicalSpace B] [Module R B] + [NonUnitalRing B] [StarRing B] [TopologicalSpace B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [Module S A] [Module S B] [IsScalarTower R S A] [IsScalarTower R S B] [NonUnitalContinuousFunctionalCalculus R p] [NonUnitalContinuousFunctionalCalculus R q] From 78a0b2f466ea466316f4a918ecdc26aab4a38cd9 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 26 Sep 2024 08:03:57 +0000 Subject: [PATCH 8/9] ci: add --nightlysha to create-adaptation-pr.sh (#17148) --- .github/workflows/nightly_detect_failure.yml | 2 +- scripts/create-adaptation-pr.sh | 16 +++++++++++----- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/.github/workflows/nightly_detect_failure.yml b/.github/workflows/nightly_detect_failure.yml index e1cfd9147086b..140f115408e95 100644 --- a/.github/workflows/nightly_detect_failure.yml +++ b/.github/workflows/nightly_detect_failure.yml @@ -210,7 +210,7 @@ jobs: bump_branch_suffix = bump_branch.replace('bump/', '') payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. " payload += "To do so semi-automatically, run the following script from mathlib root:\n\n" - payload += f"```bash\n./scripts/create-adaptation-pr.sh {bump_branch_suffix} {current_version}\n```\n" + payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n" # Only post if the message is different # We compare the first 160 characters, since that includes the date and bump version if not messages or messages[0]['content'][:160] != payload[:160]: diff --git a/scripts/create-adaptation-pr.sh b/scripts/create-adaptation-pr.sh index 2e7d69f7916d8..4fb326cfac9d6 100755 --- a/scripts/create-adaptation-pr.sh +++ b/scripts/create-adaptation-pr.sh @@ -21,9 +21,10 @@ AUTO="no" usage() { echo "Usage: $0 " echo " or" - echo " $0 --bumpversion= --nightlydate= [--auto=]" + echo " $0 --bumpversion= --nightlydate= --nightlysha= [--auto=]" echo "BUMPVERSION: The upcoming release that we are targeting, e.g., 'v4.10.0'" echo "NIGHTLYDATE: The date of the nightly toolchain currently used on 'nightly-testing'" + echo "NIGHTLYSHA: The SHA of the nightly toolchain that we want to adapt to" echo "AUTO: Optional flag to specify automatic mode, default is 'no'" exit 1 } @@ -43,6 +44,10 @@ elif [ $# -ge 2 ]; then NIGHTLYDATE="${arg#*=}" shift ;; + --nightlysha=*) + NIGHTLYSHA="${arg#*=}" + shift + ;; --auto=*) AUTO="${arg#*=}" shift @@ -148,15 +153,14 @@ echo echo "### [auto] create a new branch 'bump/nightly-$NIGHTLYDATE' and merge the latest changes from 'origin/nightly-testing'" git checkout -b "bump/nightly-$NIGHTLYDATE" -git merge origin/nightly-testing || true # ignore error if there are conflicts +git merge $NIGHTLYSHA || true # ignore error if there are conflicts # Check if there are merge conflicts if git diff --name-only --diff-filter=U | grep -q .; then echo echo "### [auto] Conflict resolution" - echo "### Automatically choosing 'lean-toolchain' and 'lake-manifest.json' from the newer branch" - echo "### In this case, the newer branch is 'origin/nightly-testing'" - git checkout origin/nightly-testing -- lean-toolchain lake-manifest.json + echo "### Automatically choosing 'lean-toolchain' and 'lake-manifest.json' from 'nightly-testing'" + git checkout $NIGHTLYSHA -- lean-toolchain lake-manifest.json git add lean-toolchain lake-manifest.json fi @@ -172,6 +176,8 @@ if git diff --name-only --diff-filter=U | grep -q .; then echo echo "### [user] Conflict resolution" echo "We are merging the latest changes from 'origin/nightly-testing' into 'bump/nightly-$NIGHTLYDATE'" + echo "Specifically, we are merging the following version of 'origin/nightly-testing':" + echo "$NIGHTLYSHA" echo "There seem to be conflicts: please resolve them" echo "" echo " 1) Open `pwd` in a new terminal and run 'git status'" From 5d4532a2dda173281ee2def1295c77f1e5104d77 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Thu, 26 Sep 2024 10:19:33 +0000 Subject: [PATCH 9/9] chore: rename `AnalyticOn` to `AnalyticOnNhd`, and `AnalyticWithinOn` to `AnalyticOn` (#17146) For coherence with `ContinuousOn`, `DifferentiableOn` and so on. See Zulip https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/Integrate.20analytic.20functions.20in.20the.20smooth.20hierarchy/near/471899268 This is 90% renaming all `AnalyticOn` to `AnalyticOnNhd` and then `AnalyticWithinOn` to `AnalyticOn`, and then adding deprecations. The 10% remaining is, when adding a deprecation `alias AnalyticOn.foo := AnalyticOnNhd.foo`, I noticed that `AnalyticOn.foo` would definitely make sense (with the new meaning of `AnalyticOn`), so I added the lemma with the new meaning instead of deprecating the old one. --- Archive/Hairer.lean | 2 +- Mathlib/Analysis/Analytic/Basic.lean | 100 +++++--- Mathlib/Analysis/Analytic/CPolynomial.lean | 39 ++- Mathlib/Analysis/Analytic/ChangeOrigin.lean | 21 +- Mathlib/Analysis/Analytic/Composition.lean | 30 ++- Mathlib/Analysis/Analytic/Constructions.lean | 236 +++++++++++------- Mathlib/Analysis/Analytic/IsolatedZeros.lean | 27 +- Mathlib/Analysis/Analytic/Linear.lean | 52 +++- Mathlib/Analysis/Analytic/Meromorphic.lean | 4 +- Mathlib/Analysis/Analytic/Polynomial.lean | 63 +++-- Mathlib/Analysis/Analytic/Uniqueness.lean | 22 +- Mathlib/Analysis/Analytic/Within.lean | 26 +- .../Analysis/Calculus/FDeriv/Analytic.lean | 54 ++-- Mathlib/Analysis/Complex/CauchyIntegral.lean | 31 ++- Mathlib/Analysis/Complex/OpenMapping.lean | 19 +- .../SpecialFunctions/Complex/Analytic.lean | 48 +++- .../Analysis/SpecialFunctions/Gamma/Beta.lean | 10 +- .../Geometry/Manifold/AnalyticManifold.lean | 42 ++-- Mathlib/NumberTheory/LSeries/Deriv.lean | 8 +- Mathlib/NumberTheory/LSeries/ZMod.lean | 22 +- docs/overview.yaml | 2 +- docs/undergrad.yaml | 2 +- scripts/no_lints_prime_decls.txt | 8 +- 23 files changed, 574 insertions(+), 294 deletions(-) diff --git a/Archive/Hairer.lean b/Archive/Hairer.lean index acd326c0b13bf..e9b91c32132a8 100644 --- a/Archive/Hairer.lean +++ b/Archive/Hairer.lean @@ -100,7 +100,7 @@ lemma inj_L : Injective (L ι) := fun g hg _h2g g_supp ↦ by simpa [mul_comm (g _), L] using congr($hp ⟨g, g_supp.trans ball_subset_closedBall, hg⟩) simp_rw [MvPolynomial.funext_iff, map_zero] - refine fun x ↦ AnalyticOn.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p + refine fun x ↦ AnalyticOnNhd.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p |>.eqOn_zero_of_preconnected_of_eventuallyEq_zero (preconnectedSpace_iff_univ.mp inferInstance) (z₀ := 0) trivial (Filter.mem_of_superset (Metric.ball_mem_nhds 0 zero_lt_one) ?_) trivial diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean index 1abdcf481ef99..b2a03d4aec9d9 100644 --- a/Mathlib/Analysis/Analytic/Basic.lean +++ b/Mathlib/Analysis/Analytic/Basic.lean @@ -49,13 +49,13 @@ Additionally, let `f` be a function from `E` to `F`. * `HasFPowerSeriesAt f p x`: on some ball of center `x` with positive radius, holds `HasFPowerSeriesOnBall f p x r`. * `AnalyticAt 𝕜 f x`: there exists a power series `p` such that holds `HasFPowerSeriesAt f p x`. -* `AnalyticOn 𝕜 f s`: the function `f` is analytic at every point of `s`. +* `AnalyticOnNhd 𝕜 f s`: the function `f` is analytic at every point of `s`. -We also define versions of `HasFPowerSeriesOnBall`, `AnalyticAt`, and `AnalyticOn` restricted to a -set, similar to `ContinuousWithinAt`. See `Mathlib.Analysis.Analytic.Within` for basic properties. +We also define versions of `HasFPowerSeriesOnBall`, `AnalyticAt`, and `AnalyticOnNhd` restricted to +a set, similar to `ContinuousWithinAt`. See `Mathlib.Analysis.Analytic.Within` for basic properties. * `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[s ∪ {x}] x`. -* `AnalyticWithinOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`. +* `AnalyticOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`. We develop the basic properties of these notions, notably: * If a function admits a power series, it is continuous (see @@ -384,14 +384,17 @@ def AnalyticWithinAt (f : E → F) (s : Set E) (x : E) : Prop := /-- Given a function `f : E → F`, we say that `f` is analytic on a set `s` if it is analytic around every point of `s`. -/ -def AnalyticOn (f : E → F) (s : Set E) := +def AnalyticOnNhd (f : E → F) (s : Set E) := ∀ x, x ∈ s → AnalyticAt 𝕜 f x /-- `f` is analytic within `s` if it is analytic within `s` at each point of `t`. Note that -this is weaker than `AnalyticOn 𝕜 f s`, as `f` is allowed to be arbitrary outside `s`. -/ -def AnalyticWithinOn (f : E → F) (s : Set E) : Prop := +this is weaker than `AnalyticOnNhd 𝕜 f s`, as `f` is allowed to be arbitrary outside `s`. -/ +def AnalyticOn (f : E → F) (s : Set E) : Prop := ∀ x ∈ s, AnalyticWithinAt 𝕜 f s x +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn := AnalyticOn + /-! ### `HasFPowerSeriesOnBall` and `HasFPowerSeriesWithinOnBall` -/ @@ -612,9 +615,12 @@ theorem HasFPowerSeriesAt.coeff_zero (hf : HasFPowerSeriesAt f pf x) (v : Fin 0 AnalyticWithinAt 𝕜 f univ x ↔ AnalyticAt 𝕜 f x := by simp [AnalyticWithinAt, AnalyticAt] -@[simp] lemma analyticWithinOn_univ {f : E → F} : - AnalyticWithinOn 𝕜 f univ ↔ AnalyticOn 𝕜 f univ := by - simp only [AnalyticWithinOn, analyticWithinAt_univ, AnalyticOn] +@[simp] lemma analyticOn_univ {f : E → F} : + AnalyticOn 𝕜 f univ ↔ AnalyticOnNhd 𝕜 f univ := by + simp only [AnalyticOn, analyticWithinAt_univ, AnalyticOnNhd] + +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn_univ := analyticOn_univ lemma AnalyticWithinAt.mono (hf : AnalyticWithinAt 𝕜 f s x) (h : t ⊆ s) : AnalyticWithinAt 𝕜 f t x := by @@ -625,25 +631,37 @@ lemma AnalyticAt.analyticWithinAt (hf : AnalyticAt 𝕜 f x) : AnalyticWithinAt rw [← analyticWithinAt_univ] at hf apply hf.mono (subset_univ _) -lemma AnalyticOn.analyticWithinOn (hf : AnalyticOn 𝕜 f s) : AnalyticWithinOn 𝕜 f s := +lemma AnalyticOnNhd.analyticOn (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOn 𝕜 f s := fun x hx ↦ (hf x hx).analyticWithinAt +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.analyticWithinOn := AnalyticOnNhd.analyticOn + lemma AnalyticWithinAt.congr_of_eventuallyEq {f g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[s] x] f) (hx : g x = f x) : AnalyticWithinAt 𝕜 g s x := by rcases hf with ⟨p, hp⟩ exact ⟨p, hp.congr hs hx⟩ +lemma AnalyticWithinAt.congr_of_eventuallyEq_insert {f g : E → F} {s : Set E} {x : E} + (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[𝓝[insert x s] x] f) : + AnalyticWithinAt 𝕜 g s x := by + apply hf.congr_of_eventuallyEq (nhdsWithin_mono x (subset_insert x s) hs) + apply mem_of_mem_nhdsWithin (mem_insert x s) hs + lemma AnalyticWithinAt.congr {f g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : EqOn g f s) (hx : g x = f x) : AnalyticWithinAt 𝕜 g s x := hf.congr_of_eventuallyEq hs.eventuallyEq_nhdsWithin hx -lemma AnalyticWithinOn.congr {f g : E → F} {s : Set E} - (hf : AnalyticWithinOn 𝕜 f s) (hs : EqOn g f s) : - AnalyticWithinOn 𝕜 g s := +lemma AnalyticOn.congr {f g : E → F} {s : Set E} + (hf : AnalyticOn 𝕜 f s) (hs : EqOn g f s) : + AnalyticOn 𝕜 g s := fun x m ↦ (hf x m).congr hs (hs m) +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.congr := AnalyticOn.congr + theorem AnalyticAt.congr (hf : AnalyticAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 g x := let ⟨_, hpf⟩ := hf (hpf.congr hg).analyticAt @@ -651,28 +669,41 @@ theorem AnalyticAt.congr (hf : AnalyticAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : An theorem analyticAt_congr (h : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 f x ↔ AnalyticAt 𝕜 g x := ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩ -theorem AnalyticOn.mono {s t : Set E} (hf : AnalyticOn 𝕜 f t) (hst : s ⊆ t) : AnalyticOn 𝕜 f s := +theorem AnalyticOnNhd.mono {s t : Set E} (hf : AnalyticOnNhd 𝕜 f t) (hst : s ⊆ t) : + AnalyticOnNhd 𝕜 f s := fun z hz => hf z (hst hz) -theorem AnalyticOn.congr' (hf : AnalyticOn 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) : - AnalyticOn 𝕜 g s := +theorem AnalyticOnNhd.congr' (hf : AnalyticOnNhd 𝕜 f s) (hg : f =ᶠ[𝓝ˢ s] g) : + AnalyticOnNhd 𝕜 g s := fun z hz => (hf z hz).congr (mem_nhdsSet_iff_forall.mp hg z hz) -theorem analyticOn_congr' (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOn 𝕜 f s ↔ AnalyticOn 𝕜 g s := +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.congr' := AnalyticOnNhd.congr' + +theorem analyticOnNhd_congr' (h : f =ᶠ[𝓝ˢ s] g) : AnalyticOnNhd 𝕜 f s ↔ AnalyticOnNhd 𝕜 g s := ⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩ -theorem AnalyticOn.congr (hs : IsOpen s) (hf : AnalyticOn 𝕜 f s) (hg : s.EqOn f g) : - AnalyticOn 𝕜 g s := +@[deprecated (since := "2024-09-26")] +alias analyticOn_congr' := analyticOnNhd_congr' + +theorem AnalyticOnNhd.congr (hs : IsOpen s) (hf : AnalyticOnNhd 𝕜 f s) (hg : s.EqOn f g) : + AnalyticOnNhd 𝕜 g s := hf.congr' <| mem_nhdsSet_iff_forall.mpr (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩) -theorem analyticOn_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOn 𝕜 f s ↔ - AnalyticOn 𝕜 g s := ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩ +theorem analyticOnNhd_congr (hs : IsOpen s) (h : s.EqOn f g) : AnalyticOnNhd 𝕜 f s ↔ + AnalyticOnNhd 𝕜 g s := ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩ -lemma AnalyticWithinOn.mono {f : E → F} {s t : Set E} (h : AnalyticWithinOn 𝕜 f t) - (hs : s ⊆ t) : AnalyticWithinOn 𝕜 f s := +@[deprecated (since := "2024-09-26")] +alias analyticOn_congr := analyticOnNhd_congr + +lemma AnalyticOn.mono {f : E → F} {s t : Set E} (h : AnalyticOn 𝕜 f t) + (hs : s ⊆ t) : AnalyticOn 𝕜 f s := fun _ m ↦ (h _ (hs m)).mono hs +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.mono := AnalyticOn.mono + /-! ### Composition with linear maps -/ @@ -691,12 +722,16 @@ theorem ContinuousLinearMap.comp_hasFPowerSeriesOnBall (g : F →L[𝕜] G) /-- If a function `f` is analytic on a set `s` and `g` is linear, then `g ∘ f` is analytic on `s`. -/ -theorem ContinuousLinearMap.comp_analyticOn {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOn 𝕜 f s) : - AnalyticOn 𝕜 (g ∘ f) s := by +theorem ContinuousLinearMap.comp_analyticOnNhd + {s : Set E} (g : F →L[𝕜] G) (h : AnalyticOnNhd 𝕜 f s) : + AnalyticOnNhd 𝕜 (g ∘ f) s := by rintro x hx rcases h x hx with ⟨p, r, hp⟩ exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesOnBall hp⟩ +@[deprecated (since := "2024-09-26")] +alias ContinuousLinearMap.comp_analyticOn := ContinuousLinearMap.comp_analyticOnNhd + /-! ### Relation between analytic function and the partial sums of its power series -/ @@ -1164,17 +1199,24 @@ protected theorem AnalyticAt.continuousAt (hf : AnalyticAt 𝕜 f x) : Continuou let ⟨_, hp⟩ := hf hp.continuousAt -protected theorem AnalyticOn.continuousOn {s : Set E} (hf : AnalyticOn 𝕜 f s) : ContinuousOn f s := +protected theorem AnalyticOnNhd.continuousOn {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) : + ContinuousOn f s := fun x hx => (hf x hx).continuousAt.continuousWithinAt -protected lemma AnalyticWithinOn.continuousOn {f : E → F} {s : Set E} (h : AnalyticWithinOn 𝕜 f s) : +protected lemma AnalyticOn.continuousOn {f : E → F} {s : Set E} (h : AnalyticOn 𝕜 f s) : ContinuousOn f s := fun x m ↦ (h x m).continuousWithinAt +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.continuousOn := AnalyticOn.continuousOn + /-- Analytic everywhere implies continuous -/ -theorem AnalyticOn.continuous {f : E → F} (fa : AnalyticOn 𝕜 f univ) : Continuous f := by +theorem AnalyticOnNhd.continuous {f : E → F} (fa : AnalyticOnNhd 𝕜 f univ) : Continuous f := by rw [continuous_iff_continuousOn_univ]; exact fa.continuousOn +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.continuous := AnalyticOnNhd.continuous + /-- In a complete space, the sum of a converging power series `p` admits `p` as a power series. This is not totally obvious as we need to check the convergence of the series. -/ protected theorem FormalMultilinearSeries.hasFPowerSeriesOnBall [CompleteSpace F] diff --git a/Mathlib/Analysis/Analytic/CPolynomial.lean b/Mathlib/Analysis/Analytic/CPolynomial.lean index bda50d02ecbfb..611b6258978a1 100644 --- a/Mathlib/Analysis/Analytic/CPolynomial.lean +++ b/Mathlib/Analysis/Analytic/CPolynomial.lean @@ -29,7 +29,7 @@ for `n : ℕ`, and let `f` be a function from `E` to `F`. We develop the basic properties of these notions, notably: * If a function is continuously polynomial, then it is analytic, see `HasFiniteFPowerSeriesOnBall.hasFPowerSeriesOnBall`, `HasFiniteFPowerSeriesAt.hasFPowerSeriesAt`, - `CPolynomialAt.analyticAt` and `CPolynomialOn.analyticOn`. + `CPolynomialAt.analyticAt` and `CPolynomialOn.analyticOnNhd`. * The sum of a finite formal power series with positive radius is well defined on the whole space, see `FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite`. * If a function admits a finite power series in a ball, then it is continuously polynomial at @@ -116,9 +116,16 @@ theorem CPolynomialAt.analyticAt (hf : CPolynomialAt 𝕜 f x) : AnalyticAt 𝕜 let ⟨p, _, hp⟩ := hf ⟨p, hp.toHasFPowerSeriesAt⟩ -theorem CPolynomialOn.analyticOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s := +theorem CPolynomialAt.analyticWithinAt {s : Set E} (hf : CPolynomialAt 𝕜 f x) : + AnalyticWithinAt 𝕜 f s x := + hf.analyticAt.analyticWithinAt + +theorem CPolynomialOn.analyticOnNhd {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOnNhd 𝕜 f s := fun x hx ↦ (hf x hx).analyticAt +theorem CPolynomialOn.analyticOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : AnalyticOn 𝕜 f s := + hf.analyticOnNhd.analyticOn + theorem HasFiniteFPowerSeriesOnBall.congr (hf : HasFiniteFPowerSeriesOnBall f p x n r) (hg : EqOn f g (EMetric.ball x r)) : HasFiniteFPowerSeriesOnBall g p x n r := ⟨hf.1.congr hg, hf.finite⟩ @@ -335,7 +342,7 @@ protected theorem CPolynomialAt.continuousAt (hf : CPolynomialAt 𝕜 f x) : Con protected theorem CPolynomialOn.continuousOn {s : Set E} (hf : CPolynomialOn 𝕜 f s) : ContinuousOn f s := - hf.analyticOn.continuousOn + hf.analyticOnNhd.continuousOn /-- Continuously polynomial everywhere implies continuous -/ theorem CPolynomialOn.continuous {f : E → F} (fa : CPolynomialOn 𝕜 f univ) : Continuous f := by @@ -571,10 +578,12 @@ lemma cpolynomialAt : CPolynomialAt 𝕜 f x := lemma cpolyomialOn : CPolynomialOn 𝕜 f s := fun _ _ ↦ f.cpolynomialAt -lemma analyticOn : AnalyticOn 𝕜 f s := f.cpolyomialOn.analyticOn +lemma analyticOnNhd : AnalyticOnNhd 𝕜 f s := f.cpolyomialOn.analyticOnNhd + +lemma analyticOn : AnalyticOn 𝕜 f s := f.analyticOnNhd.analyticOn -lemma analyticWithinOn : AnalyticWithinOn 𝕜 f s := - f.analyticOn.analyticWithinOn +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn := analyticOn lemma analyticAt : AnalyticAt 𝕜 f x := f.cpolynomialAt.analyticAt @@ -624,12 +633,16 @@ lemma cpolyomialOn_uncurry_of_multilinear : CPolynomialOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s := fun _ _ ↦ f.cpolynomialAt_uncurry_of_multilinear -lemma analyticOn_uncurry_of_multilinear : AnalyticOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s := - f.cpolyomialOn_uncurry_of_multilinear.analyticOn +lemma analyticOnNhd_uncurry_of_multilinear : + AnalyticOnNhd 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s := + f.cpolyomialOn_uncurry_of_multilinear.analyticOnNhd + +lemma analyticOn_uncurry_of_multilinear : + AnalyticOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s := + f.analyticOnNhd_uncurry_of_multilinear.analyticOn -lemma analyticWithinOn_uncurry_of_multilinear : - AnalyticWithinOn 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s := - f.analyticOn_uncurry_of_multilinear.analyticWithinOn +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn_uncurry_of_multilinear := analyticOn_uncurry_of_multilinear lemma analyticAt_uncurry_of_multilinear : AnalyticAt 𝕜 (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x := f.cpolynomialAt_uncurry_of_multilinear.analyticAt @@ -640,11 +653,11 @@ lemma analyticWithinAt_uncurry_of_multilinear : lemma continuousOn_uncurry_of_multilinear : ContinuousOn (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) s := - f.analyticOn_uncurry_of_multilinear.continuousOn + f.analyticOnNhd_uncurry_of_multilinear.continuousOn lemma continuous_uncurry_of_multilinear : Continuous (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) := - f.analyticOn_uncurry_of_multilinear.continuous + f.analyticOnNhd_uncurry_of_multilinear.continuous lemma continuousAt_uncurry_of_multilinear : ContinuousAt (fun (p : G × (Π i, Em i)) ↦ f p.1 p.2) x := diff --git a/Mathlib/Analysis/Analytic/ChangeOrigin.lean b/Mathlib/Analysis/Analytic/ChangeOrigin.lean index de0ca613e74d3..ea293a3262884 100644 --- a/Mathlib/Analysis/Analytic/ChangeOrigin.lean +++ b/Mathlib/Analysis/Analytic/ChangeOrigin.lean @@ -318,10 +318,13 @@ theorem HasFPowerSeriesOnBall.analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p rw [add_sub_cancel] at this exact this.analyticAt -theorem HasFPowerSeriesOnBall.analyticOn (hf : HasFPowerSeriesOnBall f p x r) : - AnalyticOn 𝕜 f (EMetric.ball x r) := +theorem HasFPowerSeriesOnBall.analyticOnNhd (hf : HasFPowerSeriesOnBall f p x r) : + AnalyticOnNhd 𝕜 f (EMetric.ball x r) := fun _y hy => hf.analyticAt_of_mem hy +@[deprecated (since := "2024-09-26")] +alias HasFPowerSeriesOnBall.analyticOn := HasFPowerSeriesOnBall.analyticOnNhd + variable (𝕜 f) in /-- For any function `f` from a normed vector space to a Banach space, the set of points `x` such that `f` is analytic at `x` is open. -/ @@ -334,13 +337,19 @@ theorem AnalyticAt.eventually_analyticAt (h : AnalyticAt 𝕜 f x) : ∀ᶠ y in 𝓝 x, AnalyticAt 𝕜 f y := (isOpen_analyticAt 𝕜 f).mem_nhds h -theorem AnalyticAt.exists_mem_nhds_analyticOn (h : AnalyticAt 𝕜 f x) : - ∃ s ∈ 𝓝 x, AnalyticOn 𝕜 f s := +theorem AnalyticAt.exists_mem_nhds_analyticOnNhd (h : AnalyticAt 𝕜 f x) : + ∃ s ∈ 𝓝 x, AnalyticOnNhd 𝕜 f s := h.eventually_analyticAt.exists_mem +@[deprecated (since := "2024-09-26")] +alias AnalyticAt.exists_mem_nhds_analyticOn := AnalyticAt.exists_mem_nhds_analyticOnNhd + /-- If we're analytic at a point, we're analytic in a nonempty ball -/ -theorem AnalyticAt.exists_ball_analyticOn (h : AnalyticAt 𝕜 f x) : - ∃ r : ℝ, 0 < r ∧ AnalyticOn 𝕜 f (Metric.ball x r) := +theorem AnalyticAt.exists_ball_analyticOnNhd (h : AnalyticAt 𝕜 f x) : + ∃ r : ℝ, 0 < r ∧ AnalyticOnNhd 𝕜 f (Metric.ball x r) := Metric.isOpen_iff.mp (isOpen_analyticAt _ _) _ h +@[deprecated (since := "2024-09-26")] +alias AnalyticAt.exists_ball_analyticOn := AnalyticAt.exists_ball_analyticOnNhd + end diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean index a6ee6bbde78ed..8b33f213f757e 100644 --- a/Mathlib/Analysis/Analytic/Composition.lean +++ b/Mathlib/Analysis/Analytic/Composition.lean @@ -830,11 +830,14 @@ theorem AnalyticWithinAt.comp_of_eq {g : F → G} {f : E → F} {y : F} {x : E} rw [← hy] at hg exact hg.comp hf h -lemma AnalyticWithinOn.comp {f : F → G} {g : E → F} {s : Set F} - {t : Set E} (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g t) (h : Set.MapsTo g t s) : - AnalyticWithinOn 𝕜 (f ∘ g) t := +lemma AnalyticOn.comp {f : F → G} {g : E → F} {s : Set F} + {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) : + AnalyticOn 𝕜 (f ∘ g) t := fun x m ↦ (hf _ (h m)).comp (hg x m) h +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.comp := AnalyticOn.comp + /-- If two functions `g` and `f` are analytic respectively at `f x` and `x`, then `g ∘ f` is analytic at `x`. -/ theorem AnalyticAt.comp {g : F → G} {f : E → F} {x : E} (hg : AnalyticAt 𝕜 g (f x)) @@ -862,19 +865,26 @@ theorem AnalyticAt.comp_analyticWithinAt_of_eq {g : F → G} {f : E → F} {x : /-- If two functions `g` and `f` are analytic respectively on `s.image f` and `s`, then `g ∘ f` is analytic on `s`. -/ -theorem AnalyticOn.comp' {s : Set E} {g : F → G} {f : E → F} (hg : AnalyticOn 𝕜 g (s.image f)) - (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (g ∘ f) s := +theorem AnalyticOnNhd.comp' {s : Set E} {g : F → G} {f : E → F} (hg : AnalyticOnNhd 𝕜 g (s.image f)) + (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (g ∘ f) s := fun z hz => (hg (f z) (Set.mem_image_of_mem f hz)).comp (hf z hz) -theorem AnalyticOn.comp {s : Set E} {t : Set F} {g : F → G} {f : E → F} (hg : AnalyticOn 𝕜 g t) - (hf : AnalyticOn 𝕜 f s) (st : Set.MapsTo f s t) : AnalyticOn 𝕜 (g ∘ f) s := +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.comp' := AnalyticOnNhd.comp' + +theorem AnalyticOnNhd.comp {s : Set E} {t : Set F} {g : F → G} {f : E → F} + (hg : AnalyticOnNhd 𝕜 g t) (hf : AnalyticOnNhd 𝕜 f s) (st : Set.MapsTo f s t) : + AnalyticOnNhd 𝕜 (g ∘ f) s := comp' (mono hg (Set.mapsTo'.mp st)) hf -lemma AnalyticOn.comp_analyticWithinOn {f : F → G} {g : E → F} {s : Set F} - {t : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g t) (h : Set.MapsTo g t s) : - AnalyticWithinOn 𝕜 (f ∘ g) t := +lemma AnalyticOnNhd.comp_analyticOn {f : F → G} {g : E → F} {s : Set F} + {t : Set E} (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOn 𝕜 g t) (h : Set.MapsTo g t s) : + AnalyticOn 𝕜 (f ∘ g) t := fun x m ↦ (hf _ (h m)).comp_analyticWithinAt (hg x m) +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.comp_analyticWithinOn := AnalyticOnNhd.comp_analyticOn + /-! ### Associativity of the composition of formal multilinear series diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean index 5b268c5b5d826..7ef5b6a75773b 100644 --- a/Mathlib/Analysis/Analytic/Constructions.lean +++ b/Mathlib/Analysis/Analytic/Constructions.lean @@ -48,14 +48,17 @@ theorem hasFPowerSeriesAt_const {c : F} {e : E} : theorem analyticAt_const {v : F} {x : E} : AnalyticAt 𝕜 (fun _ => v) x := ⟨constFormalMultilinearSeries 𝕜 E v, hasFPowerSeriesAt_const⟩ -theorem analyticOn_const {v : F} {s : Set E} : AnalyticOn 𝕜 (fun _ => v) s := +theorem analyticOnNhd_const {v : F} {s : Set E} : AnalyticOnNhd 𝕜 (fun _ => v) s := fun _ _ => analyticAt_const theorem analyticWithinAt_const {v : F} {s : Set E} {x : E} : AnalyticWithinAt 𝕜 (fun _ => v) s x := analyticAt_const.analyticWithinAt -theorem analyticWithinOn_const {v : F} {s : Set E} : AnalyticWithinOn 𝕜 (fun _ => v) s := - analyticOn_const.analyticWithinOn +theorem analyticOn_const {v : F} {s : Set E} : AnalyticOn 𝕜 (fun _ => v) s := + analyticOnNhd_const.analyticOn + +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn_const := analyticOn_const /-! ### Addition, negation, subtraction @@ -159,28 +162,37 @@ theorem AnalyticAt.sub (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) : AnalyticAt 𝕜 (f - g) x := by simpa only [sub_eq_add_neg] using hf.add hg.neg -theorem AnalyticWithinOn.add (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) : - AnalyticWithinOn 𝕜 (f + g) s := - fun z hz => (hf z hz).add (hg z hz) - theorem AnalyticOn.add (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (f + g) s := fun z hz => (hf z hz).add (hg z hz) -theorem AnalyticWithinOn.neg (hf : AnalyticWithinOn 𝕜 f s) : AnalyticWithinOn 𝕜 (-f) s := - fun z hz ↦ (hf z hz).neg +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.add := AnalyticOn.add + +theorem AnalyticOnNhd.add (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : + AnalyticOnNhd 𝕜 (f + g) s := + fun z hz => (hf z hz).add (hg z hz) theorem AnalyticOn.neg (hf : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (-f) s := fun z hz ↦ (hf z hz).neg -theorem AnalyticWithinOn.sub (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) : - AnalyticWithinOn 𝕜 (f - g) s := - fun z hz => (hf z hz).sub (hg z hz) +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.neg := AnalyticOn.neg + +theorem AnalyticOnNhd.neg (hf : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (-f) s := + fun z hz ↦ (hf z hz).neg theorem AnalyticOn.sub (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (f - g) s := fun z hz => (hf z hz).sub (hg z hz) +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.sub := AnalyticOn.sub + +theorem AnalyticOnNhd.sub (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : + AnalyticOnNhd 𝕜 (f - g) s := + fun z hz => (hf z hz).sub (hg z hz) + end /-! @@ -270,17 +282,20 @@ lemma AnalyticAt.prod {e : E} {f : E → F} {g : E → G} exact ⟨_, hf.prod hg⟩ /-- The Cartesian product of analytic functions within a set is analytic. -/ -lemma AnalyticWithinOn.prod {f : E → F} {g : E → G} {s : Set E} - (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) : - AnalyticWithinOn 𝕜 (fun x ↦ (f x, g x)) s := - fun x hx ↦ (hf x hx).prod (hg x hx) - -/-- The Cartesian product of analytic functions is analytic. -/ lemma AnalyticOn.prod {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : AnalyticOn 𝕜 (fun x ↦ (f x, g x)) s := fun x hx ↦ (hf x hx).prod (hg x hx) +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.prod := AnalyticOn.prod + +/-- The Cartesian product of analytic functions is analytic. -/ +lemma AnalyticOnNhd.prod {f : E → F} {g : E → G} {s : Set E} + (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : + AnalyticOnNhd 𝕜 (fun x ↦ (f x, g x)) s := + fun x hx ↦ (hf x hx).prod (hg x hx) + /-- `AnalyticAt.comp` for functions on product spaces -/ theorem AnalyticAt.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {x : E} (ha : AnalyticAt 𝕜 h (f x, g x)) (fa : AnalyticAt 𝕜 f x) @@ -304,20 +319,23 @@ theorem AnalyticAt.comp₂_analyticWithinAt AnalyticWithinAt 𝕜 (fun x ↦ h (f x, g x)) s x := AnalyticAt.comp_analyticWithinAt ha (fa.prod ga) -/-- `AnalyticOn.comp` for functions on product spaces -/ -theorem AnalyticOn.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E} - (ha : AnalyticOn 𝕜 h s) (fa : AnalyticOn 𝕜 f t) (ga : AnalyticOn 𝕜 g t) - (m : ∀ x, x ∈ t → (f x, g x) ∈ s) : AnalyticOn 𝕜 (fun x ↦ h (f x, g x)) t := +/-- `AnalyticOnNhd.comp` for functions on product spaces -/ +theorem AnalyticOnNhd.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E} + (ha : AnalyticOnNhd 𝕜 h s) (fa : AnalyticOnNhd 𝕜 f t) (ga : AnalyticOnNhd 𝕜 g t) + (m : ∀ x, x ∈ t → (f x, g x) ∈ s) : AnalyticOnNhd 𝕜 (fun x ↦ h (f x, g x)) t := fun _ xt ↦ (ha _ (m _ xt)).comp₂ (fa _ xt) (ga _ xt) -/-- `AnalyticWithinOn.comp` for functions on product spaces -/ -theorem AnalyticWithinOn.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} +/-- `AnalyticOn.comp` for functions on product spaces -/ +theorem AnalyticOn.comp₂ {h : F × G → H} {f : E → F} {g : E → G} {s : Set (F × G)} {t : Set E} - (ha : AnalyticWithinOn 𝕜 h s) (fa : AnalyticWithinOn 𝕜 f t) - (ga : AnalyticWithinOn 𝕜 g t) (m : Set.MapsTo (fun y ↦ (f y, g y)) t s) : - AnalyticWithinOn 𝕜 (fun x ↦ h (f x, g x)) t := + (ha : AnalyticOn 𝕜 h s) (fa : AnalyticOn 𝕜 f t) + (ga : AnalyticOn 𝕜 g t) (m : Set.MapsTo (fun y ↦ (f y, g y)) t s) : + AnalyticOn 𝕜 (fun x ↦ h (f x, g x)) t := fun x hx ↦ (ha _ (m hx)).comp₂ (fa x hx) (ga x hx) m +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.comp₂ := AnalyticOn.comp₂ + /-- Analytic functions on products are analytic in the first coordinate -/ theorem AnalyticAt.curry_left {f : E × F → G} {p : E × F} (fa : AnalyticAt 𝕜 f p) : AnalyticAt 𝕜 (fun x ↦ f (x, p.2)) p.1 := @@ -341,27 +359,41 @@ theorem AnalyticWithinAt.curry_right AnalyticWithinAt.comp₂ fa analyticWithinAt_const analyticWithinAt_id (fun _ hx ↦ hx) /-- Analytic functions on products are analytic in the first coordinate -/ -theorem AnalyticOn.curry_left {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticOn 𝕜 f s) : - AnalyticOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} := +theorem AnalyticOnNhd.curry_left {f : E × F → G} {s : Set (E × F)} {y : F} + (fa : AnalyticOnNhd 𝕜 f s) : + AnalyticOnNhd 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} := fun x m ↦ (fa (x, y) m).curry_left -alias AnalyticOn.along_fst := AnalyticOn.curry_left +alias AnalyticOnNhd.along_fst := AnalyticOnNhd.curry_left + +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.along_fst := AnalyticOnNhd.curry_left -theorem AnalyticWithinOn.curry_left - {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticWithinOn 𝕜 f s) : - AnalyticWithinOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} := +theorem AnalyticOn.curry_left + {f : E × F → G} {s : Set (E × F)} {y : F} (fa : AnalyticOn 𝕜 f s) : + AnalyticOn 𝕜 (fun x ↦ f (x, y)) {x | (x, y) ∈ s} := fun x m ↦ (fa (x, y) m).curry_left +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.curry_left := AnalyticOn.curry_left + /-- Analytic functions on products are analytic in the second coordinate -/ -theorem AnalyticOn.curry_right {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticOn 𝕜 f s) : - AnalyticOn 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} := +theorem AnalyticOnNhd.curry_right {f : E × F → G} {x : E} {s : Set (E × F)} + (fa : AnalyticOnNhd 𝕜 f s) : + AnalyticOnNhd 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} := fun y m ↦ (fa (x, y) m).curry_right -alias AnalyticOn.along_snd := AnalyticOn.curry_right +alias AnalyticOnNhd.along_snd := AnalyticOnNhd.curry_right -theorem AnalyticWithinOn.curry_right - {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticWithinOn 𝕜 f s) : - AnalyticWithinOn 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} := +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.along_snd := AnalyticOnNhd.curry_right + +theorem AnalyticOn.curry_right + {f : E × F → G} {x : E} {s : Set (E × F)} (fa : AnalyticOn 𝕜 f s) : + AnalyticOn 𝕜 (fun y ↦ f (x, y)) {y | (x, y) ∈ s} := fun y m ↦ (fa (x, y) m).curry_right +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.curry_right := AnalyticOn.curry_right + /-! ### Analyticity in Pi spaces @@ -491,20 +523,26 @@ lemma analyticAt_pi_iff : simp_rw [← analyticWithinAt_univ] exact analyticWithinAt_pi_iff -lemma AnalyticWithinOn.pi (hf : ∀ i, AnalyticWithinOn 𝕜 (f i) s) : - AnalyticWithinOn 𝕜 (fun x ↦ (f · x)) s := +lemma AnalyticOn.pi (hf : ∀ i, AnalyticOn 𝕜 (f i) s) : + AnalyticOn 𝕜 (fun x ↦ (f · x)) s := fun x hx ↦ AnalyticWithinAt.pi (fun i ↦ hf i x hx) -lemma analyticWithinOn_pi_iff : - AnalyticWithinOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticWithinOn 𝕜 (f i) s := +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.pi := AnalyticOn.pi + +lemma analyticOn_pi_iff : + AnalyticOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOn 𝕜 (f i) s := ⟨fun h i x hx ↦ analyticWithinAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩ -lemma AnalyticOn.pi (hf : ∀ i, AnalyticOn 𝕜 (f i) s) : - AnalyticOn 𝕜 (fun x ↦ (f · x)) s := +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn_pi_iff := analyticOn_pi_iff + +lemma AnalyticOnNhd.pi (hf : ∀ i, AnalyticOnNhd 𝕜 (f i) s) : + AnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s := fun x hx ↦ AnalyticAt.pi (fun i ↦ hf i x hx) -lemma analyticOn_pi_iff : - AnalyticOn 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOn 𝕜 (f i) s := +lemma analyticOnNhd_pi_iff : + AnalyticOnNhd 𝕜 (fun x ↦ (f · x)) s ↔ ∀ i, AnalyticOnNhd 𝕜 (f i) s := ⟨fun h i x hx ↦ analyticAt_pi_iff.1 (h x hx) i, fun h ↦ .pi h⟩ end @@ -540,16 +578,19 @@ lemma AnalyticAt.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E (analyticAt_smul _).comp₂ hf hg /-- Scalar multiplication of one analytic function by another. -/ -lemma AnalyticWithinOn.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] +lemma AnalyticOn.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E} - (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) : - AnalyticWithinOn 𝕜 (fun x ↦ f x • g x) s := + (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : + AnalyticOn 𝕜 (fun x ↦ f x • g x) s := fun _ m ↦ (hf _ m).smul (hg _ m) +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.smul := AnalyticOn.smul + /-- Scalar multiplication of one analytic function by another. -/ -lemma AnalyticOn.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E} - (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : - AnalyticOn 𝕜 (fun x ↦ f x • g x) s := +lemma AnalyticOnNhd.smul [NormedSpace 𝕝 F] [IsScalarTower 𝕜 𝕝 F] {f : E → 𝕝} {g : E → F} {s : Set E} + (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : + AnalyticOnNhd 𝕜 (fun x ↦ f x • g x) s := fun _ m ↦ (hf _ m).smul (hg _ m) /-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/ @@ -564,14 +605,18 @@ lemma AnalyticAt.mul {f g : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (hg : An (analyticAt_mul _).comp₂ hf hg /-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/ -lemma AnalyticWithinOn.mul {f g : E → A} {s : Set E} - (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) : - AnalyticWithinOn 𝕜 (fun x ↦ f x * g x) s := +lemma AnalyticOn.mul {f g : E → A} {s : Set E} + (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : + AnalyticOn 𝕜 (fun x ↦ f x * g x) s := fun _ m ↦ (hf _ m).mul (hg _ m) +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.mul := AnalyticOn.mul + /-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic. -/ -lemma AnalyticOn.mul {f g : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) : - AnalyticOn 𝕜 (fun x ↦ f x * g x) s := +lemma AnalyticOnNhd.mul {f g : E → A} {s : Set E} + (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) : + AnalyticOnNhd 𝕜 (fun x ↦ f x * g x) s := fun _ m ↦ (hf _ m).mul (hg _ m) /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/ @@ -592,13 +637,16 @@ lemma AnalyticAt.pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) exact hf.pow n /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/ -lemma AnalyticWithinOn.pow {f : E → A} {s : Set E} (hf : AnalyticWithinOn 𝕜 f s) (n : ℕ) : - AnalyticWithinOn 𝕜 (fun x ↦ f x ^ n) s := +lemma AnalyticOn.pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) : + AnalyticOn 𝕜 (fun x ↦ f x ^ n) s := fun _ m ↦ (hf _ m).pow n +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.pow := AnalyticOn.pow + /-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/ -lemma AnalyticOn.pow {f : E → A} {s : Set E} (hf : AnalyticOn 𝕜 f s) (n : ℕ) : - AnalyticOn 𝕜 (fun x ↦ f x ^ n) s := +lemma AnalyticOnNhd.pow {f : E → A} {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) (n : ℕ) : + AnalyticOnNhd 𝕜 (fun x ↦ f x ^ n) s := fun _ m ↦ (hf _ m).pow n section Geometric @@ -726,9 +774,12 @@ lemma analyticAt_inv {z : 𝕝} (hz : z ≠ 0) : AnalyticAt 𝕜 Inv.inv z := by exact Ring.inverse_eq_inv'.symm /-- `x⁻¹` is analytic away from zero -/ -lemma analyticOn_inv : AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} := by +lemma analyticOnNhd_inv : AnalyticOnNhd 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} := by intro z m; exact analyticAt_inv m +lemma analyticOn_inv : AnalyticOn 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0} := + analyticOnNhd_inv.analyticOn + /-- `(f x)⁻¹` is analytic away from `f x = 0` -/ theorem AnalyticWithinAt.inv {f : E → 𝕝} {x : E} {s : Set E} (fa : AnalyticWithinAt 𝕜 f s x) (f0 : f x ≠ 0) : @@ -741,14 +792,18 @@ theorem AnalyticAt.inv {f : E → 𝕝} {x : E} (fa : AnalyticAt 𝕜 f x) (f0 : (analyticAt_inv f0).comp fa /-- `(f x)⁻¹` is analytic away from `f x = 0` -/ -theorem AnalyticWithinOn.inv {f : E → 𝕝} {s : Set E} - (fa : AnalyticWithinOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) : - AnalyticWithinOn 𝕜 (fun x ↦ (f x)⁻¹) s := +theorem AnalyticOn.inv {f : E → 𝕝} {s : Set E} + (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) : + AnalyticOn 𝕜 (fun x ↦ (f x)⁻¹) s := fun x m ↦ (fa x m).inv (f0 x m) +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.inv := AnalyticOn.inv + /-- `(f x)⁻¹` is analytic away from `f x = 0` -/ -theorem AnalyticOn.inv {f : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) : - AnalyticOn 𝕜 (fun x ↦ (f x)⁻¹) s := +theorem AnalyticOnNhd.inv {f : E → 𝕝} {s : Set E} + (fa : AnalyticOnNhd 𝕜 f s) (f0 : ∀ x ∈ s, f x ≠ 0) : + AnalyticOnNhd 𝕜 (fun x ↦ (f x)⁻¹) s := fun x m ↦ (fa x m).inv (f0 x m) /-- `f x / g x` is analytic away from `g x = 0` -/ @@ -763,18 +818,21 @@ theorem AnalyticAt.div {f g : E → 𝕝} {x : E} AnalyticAt 𝕜 (fun x ↦ f x / g x) x := by simp_rw [div_eq_mul_inv]; exact fa.mul (ga.inv g0) -/-- `f x / g x` is analytic away from `g x = 0` -/ -theorem AnalyticWithinOn.div {f g : E → 𝕝} {s : Set E} - (fa : AnalyticWithinOn 𝕜 f s) (ga : AnalyticWithinOn 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) : - AnalyticWithinOn 𝕜 (fun x ↦ f x / g x) s := fun x m ↦ - (fa x m).div (ga x m) (g0 x m) - /-- `f x / g x` is analytic away from `g x = 0` -/ theorem AnalyticOn.div {f g : E → 𝕝} {s : Set E} (fa : AnalyticOn 𝕜 f s) (ga : AnalyticOn 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) : AnalyticOn 𝕜 (fun x ↦ f x / g x) s := fun x m ↦ (fa x m).div (ga x m) (g0 x m) +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.div := AnalyticOn.div + +/-- `f x / g x` is analytic away from `g x = 0` -/ +theorem AnalyticOnNhd.div {f g : E → 𝕝} {s : Set E} + (fa : AnalyticOnNhd 𝕜 f s) (ga : AnalyticOnNhd 𝕜 g s) (g0 : ∀ x ∈ s, g x ≠ 0) : + AnalyticOnNhd 𝕜 (fun x ↦ f x / g x) s := fun x m ↦ + (fa x m).div (ga x m) (g0 x m) + /-! ### Finite sums and products of analytic functions -/ @@ -797,16 +855,19 @@ theorem Finset.analyticAt_sum {f : α → E → F} {c : E} simp_rw [← analyticWithinAt_univ] at h ⊢ exact N.analyticWithinAt_sum h -/-- Finite sums of analytic functions are analytic -/ -theorem Finset.analyticWithinOn_sum {f : α → E → F} {s : Set E} - (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinOn 𝕜 (f n) s) : - AnalyticWithinOn 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s := - fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs) - /-- Finite sums of analytic functions are analytic -/ theorem Finset.analyticOn_sum {f : α → E → F} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) : AnalyticOn 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s := + fun z zs ↦ N.analyticWithinAt_sum (fun n m ↦ h n m z zs) + +@[deprecated (since := "2024-09-26")] +alias Finset.analyticWithinOn_sum := Finset.analyticOn_sum + +/-- Finite sums of analytic functions are analytic -/ +theorem Finset.analyticOnNhd_sum {f : α → E → F} {s : Set E} + (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) : + AnalyticOnNhd 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s := fun z zs ↦ N.analyticAt_sum (fun n m ↦ h n m z zs) /-- Finite products of analytic functions are analytic -/ @@ -827,14 +888,17 @@ theorem Finset.analyticAt_prod {A : Type*} [NormedCommRing A] [NormedAlgebra simp_rw [← analyticWithinAt_univ] at h ⊢ exact N.analyticWithinAt_prod h -/-- Finite products of analytic functions are analytic -/ -theorem Finset.analyticWithinOn_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] - {f : α → E → A} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticWithinOn 𝕜 (f n) s) : - AnalyticWithinOn 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s := - fun z zs ↦ N.analyticWithinAt_prod (fun n m ↦ h n m z zs) - /-- Finite products of analytic functions are analytic -/ theorem Finset.analyticOn_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) : AnalyticOn 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s := + fun z zs ↦ N.analyticWithinAt_prod (fun n m ↦ h n m z zs) + +@[deprecated (since := "2024-09-26")] +alias Finset.analyticWithinOn_prod := Finset.analyticOn_prod + +/-- Finite products of analytic functions are analytic -/ +theorem Finset.analyticOnNhd_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] + {f : α → E → A} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) : + AnalyticOnNhd 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s := fun z zs ↦ N.analyticAt_prod (fun n m ↦ h n m z zs) diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean index 00ccc0c8bbeea..1f37145b0dc28 100644 --- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean +++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean @@ -20,7 +20,7 @@ useful in this setup. * `AnalyticAt.eventually_eq_zero_or_eventually_ne_zero` is the main statement that if a function is analytic at `z₀`, then either it is identically zero in a neighborhood of `z₀`, or it does not vanish in a punctured neighborhood of `z₀`. -* `AnalyticOn.eqOn_of_preconnected_of_frequently_eq` is the identity theorem for analytic +* `AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq` is the identity theorem for analytic functions: if a function `f` is analytic on a connected set `U` and is zero on a set with an accumulation point in `U` then `f` is identically `0` on `U`. -/ @@ -221,7 +221,7 @@ lemma order_eq_nat_iff (hf : AnalyticAt 𝕜 f z₀) (n : ℕ) : hf.order = ↑n end AnalyticAt -namespace AnalyticOn +namespace AnalyticOnNhd variable {U : Set 𝕜} @@ -229,13 +229,13 @@ variable {U : Set 𝕜} analytic on a connected set `U` and vanishes in arbitrary neighborhoods of a point `z₀ ∈ U`, then it is identically zero in `U`. For higher-dimensional versions requiring that the function vanishes in a neighborhood of `z₀`, -see `AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero`. -/ -theorem eqOn_zero_of_preconnected_of_frequently_eq_zero (hf : AnalyticOn 𝕜 f U) +see `AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero`. -/ +theorem eqOn_zero_of_preconnected_of_frequently_eq_zero (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfw : ∃ᶠ z in 𝓝[≠] z₀, f z = 0) : EqOn f 0 U := hf.eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀ ((hf z₀ h₀).frequently_zero_iff_eventually_zero.1 hfw) -theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hU : IsPreconnected U) +theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfz₀ : z₀ ∈ closure ({z | f z = 0} \ {z₀})) : EqOn f 0 U := hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ (mem_closure_ne_iff_frequently_within.mp hfz₀) @@ -244,15 +244,15 @@ theorem eqOn_zero_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hU analytic on a connected set `U` and coincide at points which accumulate to a point `z₀ ∈ U`, then they coincide globally in `U`. For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`, -see `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`. -/ -theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOn 𝕜 f U) (hg : AnalyticOn 𝕜 g U) +see `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`. -/ +theorem eqOn_of_preconnected_of_frequently_eq (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : EqOn f g U := by have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 := hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self] simpa [sub_eq_zero] using fun z hz => (hf.sub hg).eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ hfg' hz -theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hg : AnalyticOn 𝕜 g U) +theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) (h₀ : z₀ ∈ U) (hfg : z₀ ∈ closure ({z | f z = g z} \ {z₀})) : EqOn f g U := hf.eqOn_of_preconnected_of_frequently_eq hg hU h₀ (mem_closure_ne_iff_frequently_within.mp hfg) @@ -261,10 +261,13 @@ theorem eqOn_of_preconnected_of_mem_closure (hf : AnalyticOn 𝕜 f U) (hg : Ana field `𝕜` are analytic everywhere and coincide at points which accumulate to a point `z₀`, then they coincide globally. For higher-dimensional versions requiring that the functions coincide in a neighborhood of `z₀`, -see `AnalyticOn.eq_of_eventuallyEq`. -/ -theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOn 𝕜 f univ) (hg : AnalyticOn 𝕜 g univ) - (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : f = g := +see `AnalyticOnNhd.eq_of_eventuallyEq`. -/ +theorem eq_of_frequently_eq [ConnectedSpace 𝕜] (hf : AnalyticOnNhd 𝕜 f univ) + (hg : AnalyticOnNhd 𝕜 g univ) (hfg : ∃ᶠ z in 𝓝[≠] z₀, f z = g z) : f = g := funext fun x => eqOn_of_preconnected_of_frequently_eq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x) -end AnalyticOn +@[deprecated (since := "2024-09-26")] +alias _root_.AnalyticOn.eq_of_frequently_eq := eq_of_frequently_eq + +end AnalyticOnNhd diff --git a/Mathlib/Analysis/Analytic/Linear.lean b/Mathlib/Analysis/Analytic/Linear.lean index ee4fa10f65092..e527cda45057c 100644 --- a/Mathlib/Analysis/Analytic/Linear.lean +++ b/Mathlib/Analysis/Analytic/Linear.lean @@ -44,15 +44,18 @@ protected theorem hasFPowerSeriesAt (f : E →L[𝕜] F) (x : E) : protected theorem analyticAt (f : E →L[𝕜] F) (x : E) : AnalyticAt 𝕜 f x := (f.hasFPowerSeriesAt x).analyticAt -protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s := +protected theorem analyticOnNhd (f : E →L[𝕜] F) (s : Set E) : AnalyticOnNhd 𝕜 f s := fun x _ ↦ f.analyticAt x protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x := (f.analyticAt x).analyticWithinAt -protected theorem analyticWithinOn (f : E →L[𝕜] F) (s : Set E) : AnalyticWithinOn 𝕜 f s := +protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s := fun x _ ↦ f.analyticWithinAt _ x +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn := ContinuousLinearMap.analyticOn + /-- Reinterpret a bilinear map `f : E →L[𝕜] F →L[𝕜] G` as a multilinear map `(E × F) [×2]→L[𝕜] G`. This multilinear map is the second term in the formal multilinear series expansion of `uncurry f`. It is given by @@ -121,9 +124,17 @@ protected theorem analyticAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E AnalyticAt 𝕜 (fun x : E × F => f x.1 x.2) x := (f.hasFPowerSeriesAt_bilinear x).analyticAt +protected theorem analyticWithinAt_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) (x : E × F) : + AnalyticWithinAt 𝕜 (fun x : E × F => f x.1 x.2) s x := + (f.analyticAt_bilinear x).analyticWithinAt + +protected theorem analyticOnNhd_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) : + AnalyticOnNhd 𝕜 (fun x : E × F => f x.1 x.2) s := + fun x _ ↦ f.analyticAt_bilinear x + protected theorem analyticOn_bilinear (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) : AnalyticOn 𝕜 (fun x : E × F => f x.1 x.2) s := - fun x _ ↦ f.analyticAt_bilinear x + (f.analyticOnNhd_bilinear s).analyticOn end ContinuousLinearMap @@ -136,12 +147,15 @@ lemma analyticWithinAt_id : AnalyticWithinAt 𝕜 (id : E → E) s z := analyticAt_id.analyticWithinAt /-- `id` is entire -/ -theorem analyticOn_id : AnalyticOn 𝕜 (fun x : E ↦ x) s := +theorem analyticOnNhd_id : AnalyticOnNhd 𝕜 (fun x : E ↦ x) s := fun _ _ ↦ analyticAt_id -theorem analyticWithinOn_id : AnalyticWithinOn 𝕜 (fun x : E ↦ x) s := +theorem analyticOn_id : AnalyticOn 𝕜 (fun x : E ↦ x) s := fun _ _ ↦ analyticWithinAt_id +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn_id := analyticOn_id + /-- `fst` is analytic -/ theorem analyticAt_fst : AnalyticAt 𝕜 (fun p : E × F ↦ p.fst) p := (ContinuousLinearMap.fst 𝕜 E F).analyticAt p @@ -157,19 +171,25 @@ theorem analyticWithinAt_snd : AnalyticWithinAt 𝕜 (fun p : E × F ↦ p.snd) analyticAt_snd.analyticWithinAt /-- `fst` is entire -/ -theorem analyticOn_fst : AnalyticOn 𝕜 (fun p : E × F ↦ p.fst) t := +theorem analyticOnNhd_fst : AnalyticOnNhd 𝕜 (fun p : E × F ↦ p.fst) t := fun _ _ ↦ analyticAt_fst -theorem analyticWithinOn_fst : AnalyticWithinOn 𝕜 (fun p : E × F ↦ p.fst) t := +theorem analyticOn_fst : AnalyticOn 𝕜 (fun p : E × F ↦ p.fst) t := fun _ _ ↦ analyticWithinAt_fst +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn_fst := analyticOn_fst + /-- `snd` is entire -/ -theorem analyticOn_snd : AnalyticOn 𝕜 (fun p : E × F ↦ p.snd) t := +theorem analyticOnNhd_snd : AnalyticOnNhd 𝕜 (fun p : E × F ↦ p.snd) t := fun _ _ ↦ analyticAt_snd -theorem analyticWithinOn_snd : AnalyticWithinOn 𝕜 (fun p : E × F ↦ p.snd) t := +theorem analyticOn_snd : AnalyticOn 𝕜 (fun p : E × F ↦ p.snd) t := fun _ _ ↦ analyticWithinAt_snd +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn_snd := analyticOn_snd + namespace ContinuousLinearEquiv variable (f : E ≃L[𝕜] F) (s : Set E) (x : E) @@ -177,15 +197,18 @@ variable (f : E ≃L[𝕜] F) (s : Set E) (x : E) protected theorem analyticAt : AnalyticAt 𝕜 f x := ((f : E →L[𝕜] F).hasFPowerSeriesAt x).analyticAt -protected theorem analyticOn : AnalyticOn 𝕜 f s := +protected theorem analyticOnNhd : AnalyticOnNhd 𝕜 f s := fun x _ ↦ f.analyticAt x protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x := (f.analyticAt x).analyticWithinAt -protected theorem analyticWithinOn (f : E →L[𝕜] F) (s : Set E) : AnalyticWithinOn 𝕜 f s := +protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s := fun x _ ↦ f.analyticWithinAt _ x +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn := ContinuousLinearEquiv.analyticOn + end ContinuousLinearEquiv namespace LinearIsometryEquiv @@ -195,13 +218,16 @@ variable (f : E ≃ₗᵢ[𝕜] F) (s : Set E) (x : E) protected theorem analyticAt : AnalyticAt 𝕜 f x := ((f : E →L[𝕜] F).hasFPowerSeriesAt x).analyticAt -protected theorem analyticOn : AnalyticOn 𝕜 f s := +protected theorem analyticOnNhd : AnalyticOnNhd 𝕜 f s := fun x _ ↦ f.analyticAt x protected theorem analyticWithinAt (f : E →L[𝕜] F) (s : Set E) (x : E) : AnalyticWithinAt 𝕜 f s x := (f.analyticAt x).analyticWithinAt -protected theorem analyticWithinOn (f : E →L[𝕜] F) (s : Set E) : AnalyticWithinOn 𝕜 f s := +protected theorem analyticOn (f : E →L[𝕜] F) (s : Set E) : AnalyticOn 𝕜 f s := fun x _ ↦ f.analyticWithinAt _ x +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn := LinearIsometryEquiv.analyticOn + end LinearIsometryEquiv diff --git a/Mathlib/Analysis/Analytic/Meromorphic.lean b/Mathlib/Analysis/Analytic/Meromorphic.lean index 1a29b6bb5cff9..4c3349d87d078 100644 --- a/Mathlib/Analysis/Analytic/Meromorphic.lean +++ b/Mathlib/Analysis/Analytic/Meromorphic.lean @@ -237,10 +237,12 @@ end MeromorphicAt /-- Meromorphy of a function on a set. -/ def MeromorphicOn (f : 𝕜 → E) (U : Set 𝕜) : Prop := ∀ x ∈ U, MeromorphicAt f x -lemma AnalyticOn.meromorphicOn {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOn 𝕜 f U) : +lemma AnalyticOnNhd.meromorphicOn {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) : MeromorphicOn f U := fun x hx ↦ (hf x hx).meromorphicAt +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.meromorphicOn := AnalyticOnNhd.meromorphicOn namespace MeromorphicOn diff --git a/Mathlib/Analysis/Analytic/Polynomial.lean b/Mathlib/Analysis/Analytic/Polynomial.lean index 74ea377c682ac..77e62fd5b542b 100644 --- a/Mathlib/Analysis/Analytic/Polynomial.lean +++ b/Mathlib/Analysis/Analytic/Polynomial.lean @@ -23,17 +23,28 @@ open Polynomial variable [NormedRing B] [NormedAlgebra 𝕜 B] [Algebra A B] {f : E → B} -theorem AnalyticAt.aeval_polynomial (hf : AnalyticAt 𝕜 f z) (p : A[X]) : - AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z := by +theorem AnalyticWithinAt.aeval_polynomial (hf : AnalyticWithinAt 𝕜 f s z) (p : A[X]) : + AnalyticWithinAt 𝕜 (fun x ↦ aeval (f x) p) s z := by refine p.induction_on (fun k ↦ ?_) (fun p q hp hq ↦ ?_) fun p i hp ↦ ?_ - · simp_rw [aeval_C]; apply analyticAt_const + · simp_rw [aeval_C]; apply analyticWithinAt_const · simp_rw [aeval_add]; exact hp.add hq · convert hp.mul hf simp_rw [pow_succ, aeval_mul, ← mul_assoc, aeval_X] +theorem AnalyticAt.aeval_polynomial (hf : AnalyticAt 𝕜 f z) (p : A[X]) : + AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z := by + rw [← analyticWithinAt_univ] at hf ⊢ + exact hf.aeval_polynomial p + +theorem AnalyticOnNhd.aeval_polynomial (hf : AnalyticOnNhd 𝕜 f s) (p : A[X]) : + AnalyticOnNhd 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ (hf x hx).aeval_polynomial p + theorem AnalyticOn.aeval_polynomial (hf : AnalyticOn 𝕜 f s) (p : A[X]) : AnalyticOn 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ (hf x hx).aeval_polynomial p +theorem AnalyticOnNhd.eval_polynomial {A} [NormedCommRing A] [NormedAlgebra 𝕜 A] (p : A[X]) : + AnalyticOnNhd 𝕜 (eval · p) Set.univ := analyticOnNhd_id.aeval_polynomial p + theorem AnalyticOn.eval_polynomial {A} [NormedCommRing A] [NormedAlgebra 𝕜 A] (p : A[X]) : AnalyticOn 𝕜 (eval · p) Set.univ := analyticOn_id.aeval_polynomial p @@ -51,27 +62,47 @@ theorem AnalyticAt.aeval_mvPolynomial (hf : ∀ i, AnalyticAt 𝕜 (f · i) z) ( · simp_rw [map_add]; exact hp.add hq · simp_rw [map_mul, aeval_X]; exact hp.mul (hf i) -theorem AnalyticOn.aeval_mvPolynomial (hf : ∀ i, AnalyticOn 𝕜 (f · i) s) (p : MvPolynomial σ A) : - AnalyticOn 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ .aeval_mvPolynomial (hf · x hx) p +theorem AnalyticOnNhd.aeval_mvPolynomial + (hf : ∀ i, AnalyticOnNhd 𝕜 (f · i) s) (p : MvPolynomial σ A) : + AnalyticOnNhd 𝕜 (fun x ↦ aeval (f x) p) s := fun x hx ↦ .aeval_mvPolynomial (hf · x hx) p + +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.aeval_mvPolynomial := AnalyticOnNhd.aeval_mvPolynomial -theorem AnalyticOn.eval_continuousLinearMap (f : E →L[𝕜] σ → B) (p : MvPolynomial σ B) : - AnalyticOn 𝕜 (fun x ↦ eval (f x) p) Set.univ := +theorem AnalyticOnNhd.eval_continuousLinearMap (f : E →L[𝕜] σ → B) (p : MvPolynomial σ B) : + AnalyticOnNhd 𝕜 (fun x ↦ eval (f x) p) Set.univ := fun x _ ↦ .aeval_mvPolynomial (fun i ↦ ((ContinuousLinearMap.proj i).comp f).analyticAt x) p -theorem AnalyticOn.eval_continuousLinearMap' (f : σ → E →L[𝕜] B) (p : MvPolynomial σ B) : - AnalyticOn 𝕜 (fun x ↦ eval (f · x) p) Set.univ := +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.eval_continuousLinearMap := AnalyticOnNhd.eval_continuousLinearMap + +theorem AnalyticOnNhd.eval_continuousLinearMap' (f : σ → E →L[𝕜] B) (p : MvPolynomial σ B) : + AnalyticOnNhd 𝕜 (fun x ↦ eval (f · x) p) Set.univ := fun x _ ↦ .aeval_mvPolynomial (fun i ↦ (f i).analyticAt x) p +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.eval_continuousLinearMap' := AnalyticOnNhd.eval_continuousLinearMap' + variable [CompleteSpace 𝕜] [T2Space E] [FiniteDimensional 𝕜 E] -theorem AnalyticOn.eval_linearMap (f : E →ₗ[𝕜] σ → B) (p : MvPolynomial σ B) : - AnalyticOn 𝕜 (fun x ↦ eval (f x) p) Set.univ := - AnalyticOn.eval_continuousLinearMap { f with cont := f.continuous_of_finiteDimensional } p +theorem AnalyticOnNhd.eval_linearMap (f : E →ₗ[𝕜] σ → B) (p : MvPolynomial σ B) : + AnalyticOnNhd 𝕜 (fun x ↦ eval (f x) p) Set.univ := + AnalyticOnNhd.eval_continuousLinearMap { f with cont := f.continuous_of_finiteDimensional } p + +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.eval_linearMap := AnalyticOnNhd.eval_linearMap + +theorem AnalyticOnNhd.eval_linearMap' (f : σ → E →ₗ[𝕜] B) (p : MvPolynomial σ B) : + AnalyticOnNhd 𝕜 (fun x ↦ eval (f · x) p) Set.univ := AnalyticOnNhd.eval_linearMap (.pi f) p + +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.eval_linearMap' := AnalyticOnNhd.eval_linearMap' -theorem AnalyticOn.eval_linearMap' (f : σ → E →ₗ[𝕜] B) (p : MvPolynomial σ B) : - AnalyticOn 𝕜 (fun x ↦ eval (f · x) p) Set.univ := AnalyticOn.eval_linearMap (.pi f) p +theorem AnalyticOnNhd.eval_mvPolynomial [Fintype σ] (p : MvPolynomial σ 𝕜) : + AnalyticOnNhd 𝕜 (eval · p) Set.univ := + AnalyticOnNhd.eval_linearMap (.id (R := 𝕜) (M := σ → 𝕜)) p -theorem AnalyticOn.eval_mvPolynomial [Fintype σ] (p : MvPolynomial σ 𝕜) : - AnalyticOn 𝕜 (eval · p) Set.univ := AnalyticOn.eval_linearMap (.id (R := 𝕜) (M := σ → 𝕜)) p +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.eval_mvPolynomial := AnalyticOnNhd.eval_mvPolynomial end MvPolynomial diff --git a/Mathlib/Analysis/Analytic/Uniqueness.lean b/Mathlib/Analysis/Analytic/Uniqueness.lean index 088cf07ea867d..6c836c8afcab6 100644 --- a/Mathlib/Analysis/Analytic/Uniqueness.lean +++ b/Mathlib/Analysis/Analytic/Uniqueness.lean @@ -13,7 +13,7 @@ import Mathlib.Analysis.Analytic.ChangeOrigin # Uniqueness principle for analytic functions We show that two analytic functions which coincide around a point coincide on whole connected sets, -in `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`. +in `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`. -/ @@ -154,13 +154,14 @@ theorem HasFPowerSeriesOnBall.r_eq_top_of_exists {f : 𝕜 → E} {r : ℝ≥0 end Uniqueness -namespace AnalyticOn +namespace AnalyticOnNhd /-- If an analytic function vanishes around a point, then it is uniformly zero along a connected set. Superseded by `eqOn_zero_of_preconnected_of_locally_zero` which does not assume completeness of the target space. -/ theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux [CompleteSpace F] {f : E → F} {U : Set E} - (hf : AnalyticOn 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) : + (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) + {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) : EqOn f 0 U := by /- Let `u` be the set of points around which `f` vanishes. It is clearly open. We have to show that its limit points in `U` still belong to it, from which the inclusion `U ⊆ u` will follow @@ -204,11 +205,12 @@ neighborhood of a point `z₀`, then it is uniformly zero along a connected set. version assuming only that the function vanishes at some points arbitrarily close to `z₀`, see `eqOn_zero_of_preconnected_of_frequently_eq_zero`. -/ theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero {f : E → F} {U : Set E} - (hf : AnalyticOn 𝕜 f U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) : + (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) + {z₀ : E} (h₀ : z₀ ∈ U) (hfz₀ : f =ᶠ[𝓝 z₀] 0) : EqOn f 0 U := by let F' := UniformSpace.Completion F set e : F →L[𝕜] F' := UniformSpace.Completion.toComplL - have : AnalyticOn 𝕜 (e ∘ f) U := fun x hx => (e.analyticAt _).comp (hf x hx) + have : AnalyticOnNhd 𝕜 (e ∘ f) U := fun x hx => (e.analyticAt _).comp (hf x hx) have A : EqOn (e ∘ f) 0 U := by apply eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux this hU h₀ filter_upwards [hfz₀] with x hx @@ -221,8 +223,8 @@ theorem eqOn_zero_of_preconnected_of_eventuallyEq_zero {f : E → F} {U : Set E} neighborhood of a point `z₀`, then they coincide globally along a connected set. For a one-dimensional version assuming only that the functions coincide at some points arbitrarily close to `z₀`, see `eqOn_of_preconnected_of_frequently_eq`. -/ -theorem eqOn_of_preconnected_of_eventuallyEq {f g : E → F} {U : Set E} (hf : AnalyticOn 𝕜 f U) - (hg : AnalyticOn 𝕜 g U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[𝓝 z₀] g) : +theorem eqOn_of_preconnected_of_eventuallyEq {f g : E → F} {U : Set E} (hf : AnalyticOnNhd 𝕜 f U) + (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U) {z₀ : E} (h₀ : z₀ ∈ U) (hfg : f =ᶠ[𝓝 z₀] g) : EqOn f g U := by have hfg' : f - g =ᶠ[𝓝 z₀] 0 := hfg.mono fun z h => by simp [h] simpa [sub_eq_zero] using fun z hz => @@ -232,9 +234,9 @@ theorem eqOn_of_preconnected_of_eventuallyEq {f g : E → F} {U : Set E} (hf : A coincide in a neighborhood of a point `z₀`, then they coincide everywhere. For a one-dimensional version assuming only that the functions coincide at some points arbitrarily close to `z₀`, see `eq_of_frequently_eq`. -/ -theorem eq_of_eventuallyEq {f g : E → F} [PreconnectedSpace E] (hf : AnalyticOn 𝕜 f univ) - (hg : AnalyticOn 𝕜 g univ) {z₀ : E} (hfg : f =ᶠ[𝓝 z₀] g) : f = g := +theorem eq_of_eventuallyEq {f g : E → F} [PreconnectedSpace E] (hf : AnalyticOnNhd 𝕜 f univ) + (hg : AnalyticOnNhd 𝕜 g univ) {z₀ : E} (hfg : f =ᶠ[𝓝 z₀] g) : f = g := funext fun x => eqOn_of_preconnected_of_eventuallyEq hf hg isPreconnected_univ (mem_univ z₀) hfg (mem_univ x) -end AnalyticOn +end AnalyticOnNhd diff --git a/Mathlib/Analysis/Analytic/Within.lean b/Mathlib/Analysis/Analytic/Within.lean index 7b1093877a659..7703eb9524ef0 100644 --- a/Mathlib/Analysis/Analytic/Within.lean +++ b/Mathlib/Analysis/Analytic/Within.lean @@ -11,7 +11,7 @@ import Mathlib.Analysis.Analytic.Constructions From `Mathlib.Analysis.Analytic.Basic`, we have the definitions 1. `AnalyticWithinAt 𝕜 f s x` means a power series at `x` converges to `f` on `𝓝[insert x s] x`. -2. `AnalyticWithinOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`. +2. `AnalyticOn 𝕜 f s t` means `∀ x ∈ t, AnalyticWithinAt 𝕜 f s x`. This means there exists an extension of `f` which is analytic and agrees with `f` on `s ∪ {x}`, but `f` is allowed to be arbitrary elsewhere. @@ -56,10 +56,10 @@ lemma analyticWithinAt_of_singleton_mem {f : E → F} {s : Set E} {x : E} (h : { apply (hasFPowerSeriesOnBall_const (e := 0)).hasSum simp only [Metric.emetric_ball_top, mem_univ] }⟩ -/-- If `f` is `AnalyticWithinOn` near each point in a set, it is `AnalyticWithinOn` the set -/ -lemma analyticWithinOn_of_locally_analyticWithinOn {f : E → F} {s : Set E} - (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticWithinOn 𝕜 f (s ∩ u)) : - AnalyticWithinOn 𝕜 f s := by +/-- If `f` is `AnalyticOn` near each point in a set, it is `AnalyticOn` the set -/ +lemma analyticOn_of_locally_analyticOn {f : E → F} {s : Set E} + (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)) : + AnalyticOn 𝕜 f s := by intro x m rcases h x m with ⟨u, ou, xu, fu⟩ rcases Metric.mem_nhds_iff.mp (ou.mem_nhds xu) with ⟨r, r0, ru⟩ @@ -79,10 +79,13 @@ lemma analyticWithinOn_of_locally_analyticWithinOn {f : E → F} {s : Set E} simp only [Metric.mem_ball, dist_self_add_left, yr] · simp only [EMetric.mem_ball, yr] }⟩ -/-- On open sets, `AnalyticOn` and `AnalyticWithinOn` coincide -/ -lemma IsOpen.analyticWithinOn_iff_analyticOn {f : E → F} {s : Set E} (hs : IsOpen s) : - AnalyticWithinOn 𝕜 f s ↔ AnalyticOn 𝕜 f s := by - refine ⟨?_, AnalyticOn.analyticWithinOn⟩ +@[deprecated (since := "2024-09-26")] +alias analyticWithinOn_of_locally_analyticWithinOn := analyticOn_of_locally_analyticOn + +/-- On open sets, `AnalyticOnNhd` and `AnalyticOn` coincide -/ +lemma IsOpen.analyticOn_iff_analyticOnNhd {f : E → F} {s : Set E} (hs : IsOpen s) : + AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s := by + refine ⟨?_, AnalyticOnNhd.analyticOn⟩ intro hf x m rcases Metric.mem_nhds_iff.mp (hs.mem_nhds m) with ⟨r, r0, rs⟩ rcases hf x m with ⟨p, t, fp⟩ @@ -97,13 +100,16 @@ lemma IsOpen.analyticWithinOn_iff_analyticOn {f : E → F} {s : Set E} (hs : IsO apply rs simp only [Metric.mem_ball, dist_self_add_left, ym.1] }⟩ +@[deprecated (since := "2024-09-26")] +alias IsOpen.analyticWithinOn_iff_analyticOn := IsOpen.analyticOn_iff_analyticOnNhd + /-! ### Equivalence to analyticity of a local extension We show that `HasFPowerSeriesWithinOnBall`, `HasFPowerSeriesWithinAt`, and `AnalyticWithinAt` are equivalent to the existence of a local extension with full analyticity. We do not yet show a -result for `AnalyticWithinOn`, as this requires a bit more work to show that local extensions can +result for `AnalyticOn`, as this requires a bit more work to show that local extensions can be stitched together. -/ diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean index ef38ec6312a71..896125484853c 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean @@ -68,9 +68,13 @@ theorem HasFPowerSeriesOnBall.differentiableOn [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (EMetric.ball x r) := fun _ hy => (h.analyticAt_of_mem hy).differentiableWithinAt -theorem AnalyticOn.differentiableOn (h : AnalyticOn 𝕜 f s) : DifferentiableOn 𝕜 f s := fun y hy => +theorem AnalyticOnNhd.differentiableOn (h : AnalyticOnNhd 𝕜 f s) : + DifferentiableOn 𝕜 f s := fun y hy => (h y hy).differentiableWithinAt +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.differentiableOn := AnalyticOnNhd.differentiableOn + theorem HasFPowerSeriesOnBall.hasFDerivAt [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) : HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p.changeOrigin y 1)) (x + y) := @@ -95,32 +99,38 @@ theorem HasFPowerSeriesOnBall.fderiv [CompleteSpace F] (h : HasFPowerSeriesOnBal simpa only [edist_eq_coe_nnnorm_sub, EMetric.mem_ball] using hz /-- If a function is analytic on a set `s`, so is its Fréchet derivative. -/ -theorem AnalyticOn.fderiv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) : - AnalyticOn 𝕜 (fderiv 𝕜 f) s := by +theorem AnalyticOnNhd.fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) : + AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s := by intro y hy rcases h y hy with ⟨p, r, hp⟩ exact hp.fderiv.analyticAt +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.fderiv := AnalyticOnNhd.fderiv + /-- If a function is analytic on a set `s`, so are its successive Fréchet derivative. -/ -theorem AnalyticOn.iteratedFDeriv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) (n : ℕ) : - AnalyticOn 𝕜 (iteratedFDeriv 𝕜 n f) s := by +theorem AnalyticOnNhd.iteratedFDeriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) : + AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s := by induction n with | zero => rw [iteratedFDeriv_zero_eq_comp] - exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F).comp_analyticOn h + exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F).comp_analyticOnNhd h | succ n IH => rw [iteratedFDeriv_succ_eq_comp_left] -- Porting note: for reasons that I do not understand at all, `?g` cannot be inlined. - convert ContinuousLinearMap.comp_analyticOn ?g IH.fderiv + convert ContinuousLinearMap.comp_analyticOnNhd ?g IH.fderiv case g => exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) ↦ E) F).symm simp +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.iteratedFDeriv := AnalyticOnNhd.iteratedFDeriv + /-- An analytic function is infinitely differentiable. -/ -theorem AnalyticOn.contDiffOn [CompleteSpace F] (h : AnalyticOn 𝕜 f s) {n : ℕ∞} : +theorem AnalyticOnNhd.contDiffOn [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s := let t := { x | AnalyticAt 𝕜 f x } suffices ContDiffOn 𝕜 n f t from this.mono h - have H : AnalyticOn 𝕜 f t := fun _x hx ↦ hx + have H : AnalyticOnNhd 𝕜 f t := fun _x hx ↦ hx have t_open : IsOpen t := isOpen_analyticAt 𝕜 f contDiffOn_of_continuousOn_differentiableOn (fun m _ ↦ (H.iteratedFDeriv m).continuousOn.congr @@ -130,7 +140,7 @@ theorem AnalyticOn.contDiffOn [CompleteSpace F] (h : AnalyticOn 𝕜 f s) {n : theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) {n : ℕ∞} : ContDiffAt 𝕜 n f x := by - obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOn + obtain ⟨s, hs, hf⟩ := h.exists_mem_nhds_analyticOnNhd exact hf.contDiffOn.contDiffAt hs lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E} @@ -138,10 +148,13 @@ lemma AnalyticWithinAt.contDiffWithinAt [CompleteSpace F] {f : E → F} {s : Set rcases h.exists_analyticAt with ⟨g, fx, fg, hg⟩ exact hg.contDiffAt.contDiffWithinAt.congr (fg.mono (subset_insert _ _)) fx -lemma AnalyticWithinOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E} - (h : AnalyticWithinOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s := +lemma AnalyticOn.contDiffOn [CompleteSpace F] {f : E → F} {s : Set E} + (h : AnalyticOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s := fun x m ↦ (h x m).contDiffWithinAt +@[deprecated (since := "2024-09-26")] +alias AnalyticWithinOn.contDiffOn := AnalyticOn.contDiffOn + end fderiv section deriv @@ -162,16 +175,23 @@ protected theorem HasFPowerSeriesAt.deriv (h : HasFPowerSeriesAt f p x) : h.hasDerivAt.deriv /-- If a function is analytic on a set `s`, so is its derivative. -/ -theorem AnalyticOn.deriv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) : AnalyticOn 𝕜 (deriv f) s := - (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOn h.fderiv +theorem AnalyticOnNhd.deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) : + AnalyticOnNhd 𝕜 (deriv f) s := + (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd h.fderiv + +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.deriv := AnalyticOnNhd.deriv /-- If a function is analytic on a set `s`, so are its successive derivatives. -/ -theorem AnalyticOn.iterated_deriv [CompleteSpace F] (h : AnalyticOn 𝕜 f s) (n : ℕ) : - AnalyticOn 𝕜 (_root_.deriv^[n] f) s := by +theorem AnalyticOnNhd.iterated_deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) : + AnalyticOnNhd 𝕜 (_root_.deriv^[n] f) s := by induction n with | zero => exact h | succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.iterated_deriv := AnalyticOnNhd.iterated_deriv + end deriv section fderiv @@ -258,7 +278,7 @@ theorem CPolynomialOn.contDiffOn (h : CPolynomialOn 𝕜 f s) {n : ℕ∞} : contDiffOn_of_continuousOn_differentiableOn (fun m _ ↦ (H.iteratedFDeriv m).continuousOn.congr fun _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx) - (fun m _ ↦ (H.iteratedFDeriv m).analyticOn.differentiableOn.congr + (fun m _ ↦ (H.iteratedFDeriv m).analyticOnNhd.differentiableOn.congr fun _ hx ↦ iteratedFDerivWithin_of_isOpen _ t_open hx) theorem CPolynomialAt.contDiffAt (h : CPolynomialAt 𝕜 f x) {n : ℕ∞} : diff --git a/Mathlib/Analysis/Complex/CauchyIntegral.lean b/Mathlib/Analysis/Complex/CauchyIntegral.lean index acb07715c395f..ebc991f8801e8 100644 --- a/Mathlib/Analysis/Complex/CauchyIntegral.lean +++ b/Mathlib/Analysis/Complex/CauchyIntegral.lean @@ -568,14 +568,18 @@ protected theorem _root_.DifferentiableOn.analyticAt {s : Set ℂ} {f : ℂ → lift R to ℝ≥0 using hR0.le exact ((hd.mono hRs).hasFPowerSeriesOnBall hR0).analyticAt +theorem _root_.DifferentiableOn.analyticOnNhd {s : Set ℂ} {f : ℂ → E} (hd : DifferentiableOn ℂ f s) + (hs : IsOpen s) : AnalyticOnNhd ℂ f s := fun _z hz => hd.analyticAt (hs.mem_nhds hz) + theorem _root_.DifferentiableOn.analyticOn {s : Set ℂ} {f : ℂ → E} (hd : DifferentiableOn ℂ f s) - (hs : IsOpen s) : AnalyticOn ℂ f s := fun _z hz => hd.analyticAt (hs.mem_nhds hz) + (hs : IsOpen s) : AnalyticOn ℂ f s := + (hd.analyticOnNhd hs).analyticOn /-- If `f : ℂ → E` is complex differentiable on some open set `s`, then it is continuously differentiable on `s`. -/ protected theorem _root_.DifferentiableOn.contDiffOn {s : Set ℂ} {f : ℂ → E} {n : ℕ} (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) : ContDiffOn ℂ n f s := - (hd.analyticOn hs).contDiffOn + (hd.analyticOnNhd hs).contDiffOn /-- A complex differentiable function `f : ℂ → E` is analytic at every point. -/ protected theorem _root_.Differentiable.analyticAt {f : ℂ → E} (hf : Differentiable ℂ f) (z : ℂ) : @@ -594,16 +598,27 @@ protected theorem _root_.Differentiable.hasFPowerSeriesOnBall {f : ℂ → E} (h (h.differentiableOn.hasFPowerSeriesOnBall hR).r_eq_top_of_exists fun _r hr => ⟨_, h.differentiableOn.hasFPowerSeriesOnBall hr⟩ +/-- On an open set, `f : ℂ → E` is analytic iff it is differentiable -/ +theorem analyticOnNhd_iff_differentiableOn {f : ℂ → E} {s : Set ℂ} (o : IsOpen s) : + AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s := + ⟨AnalyticOnNhd.differentiableOn, fun d _ zs ↦ d.analyticAt (o.mem_nhds zs)⟩ + /-- On an open set, `f : ℂ → E` is analytic iff it is differentiable -/ theorem analyticOn_iff_differentiableOn {f : ℂ → E} {s : Set ℂ} (o : IsOpen s) : - AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s := - ⟨AnalyticOn.differentiableOn, fun d _ zs ↦ d.analyticAt (o.mem_nhds zs)⟩ + AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s := by + rw [o.analyticOn_iff_analyticOnNhd] + exact analyticOnNhd_iff_differentiableOn o /-- `f : ℂ → E` is entire iff it's differentiable -/ +theorem analyticOnNhd_univ_iff_differentiable {f : ℂ → E} : + AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f := by + simp only [← differentiableOn_univ] + exact analyticOnNhd_iff_differentiableOn isOpen_univ + theorem analyticOn_univ_iff_differentiable {f : ℂ → E} : AnalyticOn ℂ f univ ↔ Differentiable ℂ f := by - simp only [← differentiableOn_univ] - exact analyticOn_iff_differentiableOn isOpen_univ + rw [analyticOn_univ] + exact analyticOnNhd_univ_iff_differentiable /-- `f : ℂ → E` is analytic at `z` iff it's differentiable near `z` -/ theorem analyticAt_iff_eventually_differentiableAt {f : ℂ → E} {c : ℂ} : @@ -614,8 +629,8 @@ theorem analyticAt_iff_eventually_differentiableAt {f : ℂ → E} {c : ℂ} : apply AnalyticAt.differentiableAt · intro d rcases _root_.eventually_nhds_iff.mp d with ⟨s, d, o, m⟩ - have h : AnalyticOn ℂ f s := by - refine DifferentiableOn.analyticOn ?_ o + have h : AnalyticOnNhd ℂ f s := by + refine DifferentiableOn.analyticOnNhd ?_ o intro z m exact (d z m).differentiableWithinAt exact h _ m diff --git a/Mathlib/Analysis/Complex/OpenMapping.lean b/Mathlib/Analysis/Complex/OpenMapping.lean index 9ce4d01945319..c37d82d1058c9 100644 --- a/Mathlib/Analysis/Complex/OpenMapping.lean +++ b/Mathlib/Analysis/Complex/OpenMapping.lean @@ -27,7 +27,7 @@ That second step is implemented in `DiffContOnCl.ball_subset_image_closedBall`. * `AnalyticAt.eventually_constant_or_nhds_le_map_nhds` is the local version of the open mapping theorem around a point; -* `AnalyticOn.is_constant_or_isOpen` is the open mapping theorem on a connected open set. +* `AnalyticOnNhd.is_constant_or_isOpen` is the open mapping theorem on a connected open set. -/ @@ -51,7 +51,7 @@ theorem DiffContOnCl.ball_subset_image_closedBall (h : DiffContOnCl ℂ f (ball have h1 : DiffContOnCl ℂ (fun z => f z - v) (ball z₀ r) := h.sub_const v have h2 : ContinuousOn (fun z => ‖f z - v‖) (closedBall z₀ r) := continuous_norm.comp_continuousOn (closure_ball z₀ hr.ne.symm ▸ h1.continuousOn) - have h3 : AnalyticOn ℂ f (ball z₀ r) := h.differentiableOn.analyticOn isOpen_ball + have h3 : AnalyticOnNhd ℂ f (ball z₀ r) := h.differentiableOn.analyticOnNhd isOpen_ball have h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖ := fun z hz => by linarith [hf z hz, show ‖v - f z₀‖ < ε / 2 from mem_ball.mp hv, norm_sub_sub_norm_sub_le_norm_sub (f z) v (f z₀)] @@ -64,7 +64,7 @@ theorem DiffContOnCl.ball_subset_image_closedBall (h : DiffContOnCl ℂ f (ball have h7 : ∀ᶠ w in 𝓝 z, f w = f z := by filter_upwards [key] with h; field_simp replace h7 : ∃ᶠ w in 𝓝[≠] z, f w = f z := (h7.filter_mono nhdsWithin_le_nhds).frequently have h8 : IsPreconnected (ball z₀ r) := (convex_ball z₀ r).isPreconnected - have h9 := h3.eqOn_of_preconnected_of_frequently_eq analyticOn_const h8 hz1 h7 + have h9 := h3.eqOn_of_preconnected_of_frequently_eq analyticOnNhd_const h8 hz1 h7 have h10 : f z = f z₀ := (h9 (mem_ball_self hr)).symm exact not_eventually.mpr hz₀ (mem_of_superset (ball_mem_nhds z₀ hr) (h10 ▸ h9)) @@ -83,7 +83,7 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux (hf : AnalyticAt have h1 := (hf.eventually_eq_or_eventually_ne analyticAt_const).resolve_left h have h2 : ∀ᶠ z in 𝓝 z₀, AnalyticAt ℂ f z := (isOpen_analyticAt ℂ f).eventually_mem hf obtain ⟨ρ, hρ, h3, h4⟩ : - ∃ ρ > 0, AnalyticOn ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀ := by + ∃ ρ > 0, AnalyticOnNhd ℂ f (closedBall z₀ ρ) ∧ ∀ z ∈ closedBall z₀ ρ, z ≠ z₀ → f z ≠ f z₀ := by simpa only [setOf_and, subset_inter_iff] using nhds_basis_closedBall.mem_iff.mp (h2.and (eventually_nhdsWithin_iff.mp h1)) replace h3 : DiffContOnCl ℂ f (ball z₀ ρ) := @@ -118,7 +118,7 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : Anal let ray : E → ℂ → E := fun z t => z₀ + t • z let gray : E → ℂ → ℂ := fun z => g ∘ ray z obtain ⟨r, hr, hgr⟩ := isOpen_iff.mp (isOpen_analyticAt ℂ g) z₀ hg - have h1 : ∀ z ∈ sphere (0 : E) 1, AnalyticOn ℂ (gray z) (ball 0 r) := by + have h1 : ∀ z ∈ sphere (0 : E) 1, AnalyticOnNhd ℂ (gray z) (ball 0 r) := by refine fun z hz t ht => AnalyticAt.comp ?_ ?_ · exact hgr (by simpa [ray, norm_smul, mem_sphere_zero_iff_norm.mp hz] using ht) · exact analyticAt_const.add @@ -134,7 +134,7 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : Anal have e1 : IsPreconnected (ball (0 : ℂ) r) := (convex_ball 0 r).isPreconnected have e2 : w ∈ sphere (0 : E) 1 := by simp [w, norm_smul, inv_mul_cancel₀ h'] specialize h1 w e2 - apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOn_const e1 (mem_ball_self hr) + apply h1.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const e1 (mem_ball_self hr) simpa [ray, gray] using h w e2 have h4 : ‖z - z₀‖ < r := by simpa [dist_eq_norm] using mem_ball.mp hz replace h4 : ↑‖z - z₀‖ ∈ ball (0 : ℂ) r := by @@ -156,13 +156,16 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : Anal /-- The *open mapping theorem* for holomorphic functions, global version: if a function `g : E → ℂ` is analytic on a connected set `U`, then either it is constant on `U`, or it is open on `U` (in the sense that it maps any open set contained in `U` to an open set in `ℂ`). -/ -theorem AnalyticOn.is_constant_or_isOpen (hg : AnalyticOn ℂ g U) (hU : IsPreconnected U) : +theorem AnalyticOnNhd.is_constant_or_isOpen (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) : (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s) := by by_cases h : ∃ z₀ ∈ U, ∀ᶠ z in 𝓝 z₀, g z = g z₀ · obtain ⟨z₀, hz₀, h⟩ := h - exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOn_const hU hz₀ h⟩ + exact Or.inl ⟨g z₀, hg.eqOn_of_preconnected_of_eventuallyEq analyticOnNhd_const hU hz₀ h⟩ · push_neg at h refine Or.inr fun s hs1 hs2 => isOpen_iff_mem_nhds.mpr ?_ rintro z ⟨w, hw1, rfl⟩ exact (hg w (hs1 hw1)).eventually_constant_or_nhds_le_map_nhds.resolve_left (h w (hs1 hw1)) (image_mem_map (hs2.mem_nhds hw1)) + +@[deprecated (since := "2024-09-26")] +alias AnalyticOn.is_constant_or_isOpen := AnalyticOnNhd.is_constant_or_isOpen diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean index 18ea3db3671d5..dfa5088bf9e96 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean @@ -21,21 +21,30 @@ variable {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] variable {f g : E → ℂ} {z : ℂ} {x : E} {s : Set E} /-- `exp` is entire -/ -theorem analyticOn_cexp : AnalyticOn ℂ exp univ := by - rw [analyticOn_univ_iff_differentiable]; exact differentiable_exp +theorem analyticOnNhd_cexp : AnalyticOnNhd ℂ exp univ := by + rw [analyticOnNhd_univ_iff_differentiable]; exact differentiable_exp + +theorem analyticOn_cexp : AnalyticOn ℂ exp univ := analyticOnNhd_cexp.analyticOn /-- `exp` is analytic at any point -/ theorem analyticAt_cexp : AnalyticAt ℂ exp z := - analyticOn_cexp z (mem_univ _) + analyticOnNhd_cexp z (mem_univ _) /-- `exp ∘ f` is analytic -/ theorem AnalyticAt.cexp (fa : AnalyticAt ℂ f x) : AnalyticAt ℂ (fun z ↦ exp (f z)) x := analyticAt_cexp.comp fa +theorem AnalyticWithinAt.cexp (fa : AnalyticWithinAt ℂ f s x) : + AnalyticWithinAt ℂ (fun z ↦ exp (f z)) s x := + analyticAt_cexp.comp_analyticWithinAt fa + /-- `exp ∘ f` is analytic -/ -theorem AnalyticOn.cexp (fs : AnalyticOn ℂ f s) : AnalyticOn ℂ (fun z ↦ exp (f z)) s := +theorem AnalyticOnNhd.cexp (fs : AnalyticOnNhd ℂ f s) : AnalyticOnNhd ℂ (fun z ↦ exp (f z)) s := fun z n ↦ analyticAt_cexp.comp (fs z n) +theorem AnalyticOn.cexp (fs : AnalyticOn ℂ f s) : AnalyticOn ℂ (fun z ↦ exp (f z)) s := + analyticOnNhd_cexp.comp_analyticOn fs (mapsTo_univ _ _) + /-- `log` is analytic away from nonpositive reals -/ theorem analyticAt_clog (m : z ∈ slitPlane) : AnalyticAt ℂ log z := by rw [analyticAt_iff_eventually_differentiableAt] @@ -48,21 +57,40 @@ theorem AnalyticAt.clog (fa : AnalyticAt ℂ f x) (m : f x ∈ slitPlane) : AnalyticAt ℂ (fun z ↦ log (f z)) x := (analyticAt_clog m).comp fa +theorem AnalyticWithinAt.clog (fa : AnalyticWithinAt ℂ f s x) (m : f x ∈ slitPlane) : + AnalyticWithinAt ℂ (fun z ↦ log (f z)) s x := + (analyticAt_clog m).comp_analyticWithinAt fa + /-- `log` is analytic away from nonpositive reals -/ +theorem AnalyticOnNhd.clog (fs : AnalyticOnNhd ℂ f s) (m : ∀ z ∈ s, f z ∈ slitPlane) : + AnalyticOnNhd ℂ (fun z ↦ log (f z)) s := + fun z n ↦ (analyticAt_clog (m z n)).comp (fs z n) + theorem AnalyticOn.clog (fs : AnalyticOn ℂ f s) (m : ∀ z ∈ s, f z ∈ slitPlane) : AnalyticOn ℂ (fun z ↦ log (f z)) s := - fun z n ↦ (analyticAt_clog (m z n)).comp (fs z n) + fun z n ↦ (analyticAt_clog (m z n)).analyticWithinAt.comp (fs z n) m /-- `f z ^ g z` is analytic if `f z` is not a nonpositive real -/ -theorem AnalyticAt.cpow (fa : AnalyticAt ℂ f x) (ga : AnalyticAt ℂ g x) - (m : f x ∈ slitPlane) : AnalyticAt ℂ (fun z ↦ f z ^ g z) x := by - have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝 x] fun z ↦ exp (log (f z) * g z) := by - filter_upwards [(fa.continuousAt.eventually_ne (slitPlane_ne_zero m))] +theorem AnalyticWithinAt.cpow (fa : AnalyticWithinAt ℂ f s x) (ga : AnalyticWithinAt ℂ g s x) + (m : f x ∈ slitPlane) : AnalyticWithinAt ℂ (fun z ↦ f z ^ g z) s x := by + have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝[insert x s] x] fun z ↦ exp (log (f z) * g z) := by + filter_upwards [(fa.continuousWithinAt_insert.eventually_ne (slitPlane_ne_zero m))] intro z fz simp only [fz, cpow_def, if_false] - rw [analyticAt_congr e] + apply AnalyticWithinAt.congr_of_eventuallyEq_insert _ e exact ((fa.clog m).mul ga).cexp +/-- `f z ^ g z` is analytic if `f z` is not a nonpositive real -/ +theorem AnalyticAt.cpow (fa : AnalyticAt ℂ f x) (ga : AnalyticAt ℂ g x) + (m : f x ∈ slitPlane) : AnalyticAt ℂ (fun z ↦ f z ^ g z) x := by + rw [← analyticWithinAt_univ] at fa ga ⊢ + exact fa.cpow ga m + +/-- `f z ^ g z` is analytic if `f z` avoids nonpositive reals -/ +theorem AnalyticOnNhd.cpow (fs : AnalyticOnNhd ℂ f s) (gs : AnalyticOnNhd ℂ g s) + (m : ∀ z ∈ s, f z ∈ slitPlane) : AnalyticOnNhd ℂ (fun z ↦ f z ^ g z) s := + fun z n ↦ (fs z n).cpow (gs z n) (m z n) + /-- `f z ^ g z` is analytic if `f z` avoids nonpositive reals -/ theorem AnalyticOn.cpow (fs : AnalyticOn ℂ f s) (gs : AnalyticOn ℂ g s) (m : ∀ z ∈ s, f z ∈ slitPlane) : AnalyticOn ℂ (fun z ↦ f z ^ g z) s := diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean index 8f72e2ec290e0..4d4cee818d69d 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean @@ -547,13 +547,13 @@ theorem Gamma_mul_Gamma_add_half (s : ℂ) : convert congr_arg Inv.inv (congr_fun this s) using 1 · rw [mul_inv, inv_inv, inv_inv] · rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub] - have h1 : AnalyticOn ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ := by - refine DifferentiableOn.analyticOn ?_ isOpen_univ + have h1 : AnalyticOnNhd ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ := by + refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ refine (differentiable_one_div_Gamma.mul ?_).differentiableOn exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _)) - have h2 : AnalyticOn ℂ + have h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π)) univ := by - refine DifferentiableOn.analyticOn ?_ isOpen_univ + refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn apply Differentiable.mul · exact differentiable_one_div_Gamma.comp (differentiable_id'.const_mul _) @@ -563,7 +563,7 @@ theorem Gamma_mul_Gamma_add_half (s : ℂ) : rw [tendsto_nhdsWithin_iff]; constructor · exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt · exact eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht) - refine AnalyticOn.eq_of_frequently_eq h1 h2 (h3.frequently ?_) + refine AnalyticOnNhd.eq_of_frequently_eq h1 h2 (h3.frequently ?_) refine ((Eventually.filter_mono nhdsWithin_le_nhds) ?_).frequently refine (eventually_gt_nhds zero_lt_one).mp (Eventually.of_forall fun t ht => ?_) rw [← mul_inv, Gamma_ofReal, (by norm_num : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ← diff --git a/Mathlib/Geometry/Manifold/AnalyticManifold.lean b/Mathlib/Geometry/Manifold/AnalyticManifold.lean index 442b24423f19a..8ef606a4540a1 100644 --- a/Mathlib/Geometry/Manifold/AnalyticManifold.lean +++ b/Mathlib/Geometry/Manifold/AnalyticManifold.lean @@ -17,7 +17,7 @@ interior and smooth everywhere (including at the boundary). The definition mirr analytic manifolds are smooth manifolds. Completeness is required throughout, but this is nonessential: it is due to many of the lemmas about -AnalyticWithinOn` requiring completeness for ease of proof. +AnalyticOn` requiring completeness for ease of proof. -/ noncomputable section @@ -42,10 +42,10 @@ analytic on the interior, and map the interior to itself. This allows us to def section analyticGroupoid /-- Given a model with corners `(E, H)`, we define the pregroupoid of analytic transformations of -`H` as the maps that are `AnalyticWithinOn` when read in `E` through `I`. Using `AnalyticWithinOn` -rather than `AnalyticOn` gives us meaningful definitions at boundary points. -/ +`H` as the maps that are `AnalyticOn` when read in `E` through `I`. Using `AnalyticOn` +rather than `AnalyticOnNhd` gives us meaningful definitions at boundary points. -/ def analyticPregroupoid : Pregroupoid H where - property f s := AnalyticWithinOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) + property f s := AnalyticOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) comp {f g u v} hf hg _ _ _ := by have : I ∘ (g ∘ f) ∘ I.symm = (I ∘ g ∘ I.symm) ∘ I ∘ f ∘ I.symm := by ext x; simp simp only [this] @@ -54,12 +54,12 @@ def analyticPregroupoid : Pregroupoid H where · rintro x ⟨hx1, _⟩ simpa only [mfld_simps] using hx1.2 id_mem := by - apply analyticWithinOn_id.congr + apply analyticOn_id.congr rintro x ⟨_, hx2⟩ obtain ⟨y, hy⟩ := mem_range.1 hx2 simp only [mfld_simps, ← hy] locality {f u} _ H := by - apply analyticWithinOn_of_locally_analyticWithinOn + apply analyticOn_of_locally_analyticOn rintro y ⟨hy1, hy2⟩ obtain ⟨x, hx⟩ := mem_range.1 hy2 simp only [mfld_simps, ← hx] at hy1 ⊢ @@ -75,8 +75,8 @@ def analyticPregroupoid : Pregroupoid H where rw [fg _ hy1] /-- Given a model with corners `(E, H)`, we define the groupoid of analytic transformations of -`H` as the maps that are `AnalyticWithinOn` when read in `E` through `I`. Using `AnalyticWithinOn` -rather than `AnalyticOn` gives us meaningful definitions at boundary points. -/ +`H` as the maps that are `AnalyticOn` when read in `E` through `I`. Using `AnalyticOn` +rather than `AnalyticOnNhd` gives us meaningful definitions at boundary points. -/ def analyticGroupoid : StructureGroupoid H := (analyticPregroupoid I).groupoid @@ -84,9 +84,9 @@ def analyticGroupoid : StructureGroupoid H := theorem ofSet_mem_analyticGroupoid {s : Set H} (hs : IsOpen s) : PartialHomeomorph.ofSet s hs ∈ analyticGroupoid I := by rw [analyticGroupoid, mem_groupoid_of_pregroupoid] - suffices h : AnalyticWithinOn 𝕜 (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by + suffices h : AnalyticOn 𝕜 (I ∘ I.symm) (I.symm ⁻¹' s ∩ range I) by simp [h, analyticPregroupoid] - have hi : AnalyticWithinOn 𝕜 id (univ : Set E) := analyticWithinOn_id + have hi : AnalyticOn 𝕜 id (univ : Set E) := analyticOn_id exact (hi.mono (subset_univ _)).congr (fun x hx ↦ I.right_inv hx.2) /-- The composition of a partial homeomorphism from `H` to `M` and its inverse belongs to @@ -108,17 +108,17 @@ instance : ClosedUnderRestriction (analyticGroupoid I) := /-- `f ∈ analyticGroupoid` iff it and its inverse are analytic within `range I`. -/ lemma mem_analyticGroupoid {I : ModelWithCorners 𝕜 E H} {f : PartialHomeomorph H H} : f ∈ analyticGroupoid I ↔ - AnalyticWithinOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' f.source ∩ range I) ∧ - AnalyticWithinOn 𝕜 (I ∘ f.symm ∘ I.symm) (I.symm ⁻¹' f.target ∩ range I) := by + AnalyticOn 𝕜 (I ∘ f ∘ I.symm) (I.symm ⁻¹' f.source ∩ range I) ∧ + AnalyticOn 𝕜 (I ∘ f.symm ∘ I.symm) (I.symm ⁻¹' f.target ∩ range I) := by rfl /-- The analytic groupoid on a boundaryless charted space modeled on a complete vector space consists of the partial homeomorphisms which are analytic and have analytic inverse. -/ theorem mem_analyticGroupoid_of_boundaryless [I.Boundaryless] (e : PartialHomeomorph H H) : - e ∈ analyticGroupoid I ↔ AnalyticOn 𝕜 (I ∘ e ∘ I.symm) (I '' e.source) ∧ - AnalyticOn 𝕜 (I ∘ e.symm ∘ I.symm) (I '' e.target) := by + e ∈ analyticGroupoid I ↔ AnalyticOnNhd 𝕜 (I ∘ e ∘ I.symm) (I '' e.source) ∧ + AnalyticOnNhd 𝕜 (I ∘ e.symm ∘ I.symm) (I '' e.target) := by simp only [mem_analyticGroupoid, I.range_eq_univ, inter_univ, I.image_eq] - rw [IsOpen.analyticWithinOn_iff_analyticOn, IsOpen.analyticWithinOn_iff_analyticOn] + rw [IsOpen.analyticOn_iff_analyticOnNhd, IsOpen.analyticOn_iff_analyticOnNhd] · exact I.continuous_symm.isOpen_preimage _ e.open_target · exact I.continuous_symm.isOpen_preimage _ e.open_source @@ -131,12 +131,12 @@ theorem analyticGroupoid_prod {E A : Type} [NormedAddCommGroup E] [NormedSpace f.prod g ∈ analyticGroupoid (I.prod J) := by have pe : range (I.prod J) = (range I).prod (range J) := I.range_prod simp only [mem_analyticGroupoid, Function.comp, image_subset_iff] at fa ga ⊢ - exact ⟨AnalyticWithinOn.prod - (fa.1.comp analyticWithinOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩) - (ga.1.comp analyticWithinOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩), - AnalyticWithinOn.prod - (fa.2.comp analyticWithinOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩) - (ga.2.comp analyticWithinOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩)⟩ + exact ⟨AnalyticOn.prod + (fa.1.comp analyticOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩) + (ga.1.comp analyticOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩), + AnalyticOn.prod + (fa.2.comp analyticOn_fst fun _ m ↦ ⟨m.1.1, (pe ▸ m.2).1⟩) + (ga.2.comp analyticOn_snd fun _ m ↦ ⟨m.1.2, (pe ▸ m.2).2⟩)⟩ end analyticGroupoid diff --git a/Mathlib/NumberTheory/LSeries/Deriv.lean b/Mathlib/NumberTheory/LSeries/Deriv.lean index d9a355faf2a9f..f8f5726a088aa 100644 --- a/Mathlib/NumberTheory/LSeries/Deriv.lean +++ b/Mathlib/NumberTheory/LSeries/Deriv.lean @@ -20,7 +20,7 @@ import Mathlib.Analysis.Complex.HalfPlane * We prove similar results for iterated derivatives (`LSeries.iteratedDeriv`). * We use this to show that `LSeries f` is holomorphic on the right half-plane of - absolute convergence (`LSeries.analyticOn`). + absolute convergence (`LSeries.analyticOnNhd`). ## Implementation notes @@ -151,6 +151,10 @@ lemma LSeries_differentiableOn (f : ℕ → ℂ) : fun _ hz ↦ (LSeries_hasDerivAt hz).differentiableAt.differentiableWithinAt /-- The L-series of `f` is holomorphic on its open half-plane of absolute convergence. -/ +lemma LSeries_analyticOnNhd (f : ℕ → ℂ) : + AnalyticOnNhd ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} := + (LSeries_differentiableOn f).analyticOnNhd <| isOpen_re_gt_EReal _ + lemma LSeries_analyticOn (f : ℕ → ℂ) : AnalyticOn ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} := - (LSeries_differentiableOn f).analyticOn <| isOpen_re_gt_EReal _ + (LSeries_analyticOnNhd f).analyticOn diff --git a/Mathlib/NumberTheory/LSeries/ZMod.lean b/Mathlib/NumberTheory/LSeries/ZMod.lean index 66dbde51f1f55..2ef6c910b132d 100644 --- a/Mathlib/NumberTheory/LSeries/ZMod.lean +++ b/Mathlib/NumberTheory/LSeries/ZMod.lean @@ -177,13 +177,13 @@ lemma LFunction_stdAddChar_eq_expZeta (j : ZMod N) (s : ℂ) (hjs : j ≠ 0 ∨ let g := expZeta (toAddCircle j) have hU {u} : u ∈ U ↔ u ≠ 1 ∨ j ≠ 0 := by simp only [mem_ite_univ_right, U]; tauto -- hypotheses for uniqueness of analytic continuation - have hf : AnalyticOn ℂ f U := by - refine DifferentiableOn.analyticOn (fun u hu ↦ ?_) hUo + have hf : AnalyticOnNhd ℂ f U := by + refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo refine (differentiableAt_LFunction _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt simp only [mul_comm j, AddChar.sum_mulShift _ (isPrimitive_stdAddChar _), h, ↓reduceIte, CharP.cast_eq_zero, or_true] - have hg : AnalyticOn ℂ g U := by - refine DifferentiableOn.analyticOn (fun u hu ↦ ?_) hUo + have hg : AnalyticOnNhd ℂ g U := by + refine DifferentiableOn.analyticOnNhd (fun u hu ↦ ?_) hUo refine (differentiableAt_expZeta _ _ ((hU.mp hu).imp_right fun h ↦ ?_)).differentiableWithinAt rwa [ne_eq, toAddCircle_eq_zero] have hUc : IsPreconnected U := by @@ -451,7 +451,7 @@ Functional equation for completed L-functions (even case), valid at all points o theorem completedLFunction_one_sub_even (hΦ : Φ.Even) (s : ℂ) (hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0) (hs₁ : s ≠ 1 ∨ Φ 0 = 0) : completedLFunction Φ (1 - s) = N ^ (s - 1) * completedLFunction (𝓕 Φ) s := by - -- We prove this using `AnalyticOn.eqOn_of_preconnected_of_eventuallyEq`, so we need to + -- We prove this using `AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq`, so we need to -- gather up the ingredients for this big theorem. -- First set up some notations: let F (t) := completedLFunction Φ (1 - t) @@ -477,12 +477,14 @@ theorem completedLFunction_one_sub_even (hΦ : Φ.Even) (s : ℂ) simp [U, Uc, h, h', and_comm] · simp only [rank_real_complex, Nat.one_lt_ofNat] -- Analyticity on U: - have hF : AnalyticOn ℂ F U := by - refine DifferentiableOn.analyticOn (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo + have hF : AnalyticOnNhd ℂ F U := by + refine DifferentiableOn.analyticOnNhd + (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo refine (differentiableAt_completedLFunction Φ _ ?_ ?_).comp t (differentiableAt_id.const_sub 1) exacts [ht.2.imp_left (sub_ne_zero.mpr ∘ Ne.symm), ht.1.imp_left sub_eq_self.not.mpr] - have hG : AnalyticOn ℂ G U := by - refine DifferentiableOn.analyticOn (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo + have hG : AnalyticOnNhd ℂ G U := by + refine DifferentiableOn.analyticOnNhd + (fun t ht ↦ DifferentiableAt.differentiableWithinAt ?_) hUo apply ((differentiableAt_id.sub_const 1).const_cpow (.inl (NeZero.ne _))).mul apply differentiableAt_completedLFunction _ _ (ht.1.imp_right fun h ↦ dft_apply_zero Φ ▸ h) exact ht.2.imp_right (fun h ↦ by simp only [← dft_apply_zero, dft_dft, neg_zero, h, smul_zero]) @@ -512,7 +514,7 @@ theorem completedLFunction_one_sub_odd (hΦ : Φ.Odd) (s : ℂ) : have hFG : F =ᶠ[𝓝 2] G := by filter_upwards [this] with t ht using completedLFunction_one_sub_of_one_lt_odd hΦ ht -- now apply the big hammer to finish - rw [← analyticOn_univ_iff_differentiable] at hF hG + rw [← analyticOnNhd_univ_iff_differentiable] at hF hG exact congr_fun (hF.eq_of_eventuallyEq hG hFG) s end signed diff --git a/docs/overview.yaml b/docs/overview.yaml index be28612dbf810..e1d21817d53b5 100644 --- a/docs/overview.yaml +++ b/docs/overview.yaml @@ -352,7 +352,7 @@ Analysis: Liouville theorem: 'Differentiable.apply_eq_apply_of_bounded' maximum modulus principle: 'Complex.eventually_eq_of_isLocalMax_norm' principle of isolated zeros: 'AnalyticAt.eventually_eq_zero_or_eventually_ne_zero' - principle of analytic continuation: 'AnalyticOn.eqOn_of_preconnected_of_frequently_eq' + principle of analytic continuation: 'AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq' analyticity of holomorphic functions: 'DifferentiableOn.analyticAt' Schwarz lemma: 'Complex.abs_le_abs_of_mapsTo_ball_self' removable singularity: 'Complex.differentiableOn_update_limUnder_insert_of_isLittleO' diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml index 21619980559e5..f1113456868a1 100644 --- a/docs/undergrad.yaml +++ b/docs/undergrad.yaml @@ -387,7 +387,7 @@ Single Variable Complex Analysis: Cauchy formulas: 'Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable' analyticity of a holomorphic function: 'DifferentiableOn.analyticAt' principle of isolated zeros: 'AnalyticAt.eventually_eq_zero_or_eventually_ne_zero' - principle of analytic continuation: 'AnalyticOn.eqOn_of_preconnected_of_frequently_eq' + principle of analytic continuation: 'AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq' maximum principle: 'Complex.eventually_eq_of_isLocalMax_norm' isolated singularities: '' Laurent series: '' diff --git a/scripts/no_lints_prime_decls.txt b/scripts/no_lints_prime_decls.txt index 048a285c74a49..5a3fa4e0c5ec5 100644 --- a/scripts/no_lints_prime_decls.txt +++ b/scripts/no_lints_prime_decls.txt @@ -162,10 +162,10 @@ AlgHom.coe_restrictScalars' AlgHom.toAddMonoidHom' AlgHom.toMonoidHom' AlternatingMap.domCoprod.summand_mk'' -analyticOn_congr' -AnalyticOn.congr' -AnalyticOn.eval_continuousLinearMap' -AnalyticOn.eval_linearMap' +analyticOnNhd_congr' +AnalyticOnNhd.congr' +AnalyticOnNhd.eval_continuousLinearMap' +AnalyticOnNhd.eval_linearMap' AntilipschitzWith.le_mul_nnnorm' AntilipschitzWith.le_mul_norm' AntilipschitzWith.to_rightInvOn'