From 2ec1335521cd76de470463e525b3d47d7331885c Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 23 Aug 2024 09:26:58 +0200 Subject: [PATCH] Update Mathlib --- Nevanlinna/analyticOn_zeroSet.lean | 4 ++-- Nevanlinna/harmonicAt.lean | 4 ++-- Nevanlinna/harmonicAt_meanValue.lean | 2 +- Nevanlinna/holomorphic.lean | 6 ++++-- Nevanlinna/holomorphicAt.lean | 1 - Nevanlinna/holomorphic_JensenFormula.lean | 2 +- Nevanlinna/holomorphic_primitive.lean | 2 +- Nevanlinna/laplace2.lean | 4 ++-- Nevanlinna/partialDeriv.lean | 6 +++--- Nevanlinna/periodic_integrability.lean | 8 -------- .../specialFunctions_CircleIntegral_affine.lean | 2 +- Nevanlinna/specialFunctions_Integral_log_sin.lean | 4 ++-- lake-manifest.json | 14 +++++++------- lean-toolchain | 2 +- 14 files changed, 27 insertions(+), 34 deletions(-) diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean index 63fcf34..4039eed 100644 --- a/Nevanlinna/analyticOn_zeroSet.lean +++ b/Nevanlinna/analyticOn_zeroSet.lean @@ -79,7 +79,7 @@ theorem AnalyticOn.order_eq_nat_iff exact h₃gloc.self_of_nhds · rw [(g_near_z₁ h₂z).self_of_nhds] simp [h₂z] - rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel] + rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀] simp; norm_num rw [sub_eq_zero] tauto @@ -89,7 +89,7 @@ theorem AnalyticOn.order_eq_nat_iff obtain ⟨g, h₁g, h₂g, h₃g⟩ := h rw [AnalyticAt.order_eq_nat_iff] use g - exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.eventually_of_forall h₃g⟩⟩ + exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩ theorem AnalyticAt.order_mul diff --git a/Nevanlinna/harmonicAt.lean b/Nevanlinna/harmonicAt.lean index 14744e5..76d9f0d 100644 --- a/Nevanlinna/harmonicAt.lean +++ b/Nevanlinna/harmonicAt.lean @@ -1,9 +1,9 @@ import Nevanlinna.laplace variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] -variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁] +variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] -variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [CompleteSpace G₁] +variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] def Harmonic (f : ℂ → F) : Prop := diff --git a/Nevanlinna/harmonicAt_meanValue.lean b/Nevanlinna/harmonicAt_meanValue.lean index 8a41b01..ffb1e81 100644 --- a/Nevanlinna/harmonicAt_meanValue.lean +++ b/Nevanlinna/harmonicAt_meanValue.lean @@ -63,7 +63,7 @@ theorem harmonic_meanValue nth_rw 1 [mul_comm] rw [← mul_assoc] simp - apply inv_mul_cancel + apply inv_mul_cancel₀ apply circleMap_ne_center exact Ne.symm (ne_of_lt hR) have t'₁ {θ : ℝ} : circleMap 0 R θ = circleMap z R θ - z := by diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean index 58f76d5..93e6672 100644 --- a/Nevanlinna/holomorphic.lean +++ b/Nevanlinna/holomorphic.lean @@ -2,8 +2,8 @@ import Mathlib.Analysis.Complex.TaylorSeries import Nevanlinna.cauchyRiemann variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] -variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] -variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G] +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] +variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] def HolomorphicAt (f : E → F) (x : E) : Prop := ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z @@ -34,6 +34,7 @@ theorem HolomorphicAt_iff theorem HolomorphicAt_analyticAt + [CompleteSpace F] {f : ℂ → F} {x : ℂ} : HolomorphicAt f x → AnalyticAt ℂ f x := by @@ -119,6 +120,7 @@ theorem HolomorphicAt_neg theorem HolomorphicAt_contDiffAt + [CompleteSpace F] {f : ℂ → F} {z : ℂ} (hf : HolomorphicAt f z) : diff --git a/Nevanlinna/holomorphicAt.lean b/Nevanlinna/holomorphicAt.lean index fe77785..ba34592 100644 --- a/Nevanlinna/holomorphicAt.lean +++ b/Nevanlinna/holomorphicAt.lean @@ -1,5 +1,4 @@ import Mathlib.Analysis.Complex.CauchyIntegral ---import Mathlib.Analysis.Complex.TaylorSeries import Nevanlinna.cauchyRiemann variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean index 01d6eb7..96b36a0 100644 --- a/Nevanlinna/holomorphic_JensenFormula.lean +++ b/Nevanlinna/holomorphic_JensenFormula.lean @@ -110,7 +110,7 @@ theorem jensen_case_R_eq_one simp have {w : ℝ} : Real.pi⁻¹ * 2⁻¹ * (2 * Real.pi * w) = w := by ring_nf - simp [mul_inv_cancel Real.pi_ne_zero] + simp [mul_inv_cancel₀ Real.pi_ne_zero] rw [this] simp rfl diff --git a/Nevanlinna/holomorphic_primitive.lean b/Nevanlinna/holomorphic_primitive.lean index 640ee43..c132007 100644 --- a/Nevanlinna/holomorphic_primitive.lean +++ b/Nevanlinna/holomorphic_primitive.lean @@ -669,7 +669,7 @@ theorem primitive_additivity' apply (inv_mul_lt_iff zero_lt_two).mpr linarith have h₁ε' : 0 < ε' := by - apply Real.mul_pos _ h₁ε + apply mul_pos _ h₁ε apply inv_pos.mpr exact zero_lt_two diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean index c641bae..f9bfe69 100644 --- a/Nevanlinna/laplace2.lean +++ b/Nevanlinna/laplace2.lean @@ -4,8 +4,8 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 --import Mathlib.Algebra.BigOperators.Basic import Mathlib.Analysis.Calculus.ContDiff.Bounds import Mathlib.Analysis.Calculus.FDeriv.Symmetric -import Mathlib.LinearAlgebra.Basis -import Mathlib.LinearAlgebra.Contraction +--import Mathlib.LinearAlgebra.Basis +--import Mathlib.LinearAlgebra.Contraction open BigOperators open Finset diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index 2b3e1c9..8890e01 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -78,7 +78,7 @@ theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv let ZZ := DifferentiableAt.const_smul contra a⁻¹ have : (fun y => a⁻¹ • a • f y) = f := by funext i - rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha] + rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel₀ ha] simp rw [this] at ZZ exact hf ZZ @@ -356,11 +356,11 @@ theorem partialDeriv_smul'₂ left_inv := by intro x simp - rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul] + rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel₀ ha, one_smul] right_inv := by intro x simp - rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul] + rw [← smul_assoc, smul_eq_mul, mul_inv_cancel₀ ha, one_smul] continuous_toFun := continuous_const_smul a continuous_invFun := continuous_const_smul a⁻¹ } diff --git a/Nevanlinna/periodic_integrability.lean b/Nevanlinna/periodic_integrability.lean index 7e26451..bd382dd 100644 --- a/Nevanlinna/periodic_integrability.lean +++ b/Nevanlinna/periodic_integrability.lean @@ -1,12 +1,4 @@ import Mathlib.MeasureTheory.Integral.Periodic -import Mathlib.MeasureTheory.Integral.CircleIntegral -import Nevanlinna.specialFunctions_Integral_log_sin -import Nevanlinna.harmonicAt_examples -import Nevanlinna.harmonicAt_meanValue -import Mathlib.Algebra.Periodic - -open scoped Interval Topology -open Real Filter MeasureTheory intervalIntegral theorem periodic_integrability₁ diff --git a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean index 69f381e..17a43ee 100644 --- a/Nevanlinna/specialFunctions_CircleIntegral_affine.lean +++ b/Nevanlinna/specialFunctions_CircleIntegral_affine.lean @@ -107,7 +107,7 @@ lemma int₀ exact norm_pos_iff'.mpr h₁a _ = 1 := by dsimp [ρ] - apply inv_mul_cancel + apply inv_mul_cancel₀ exact (AbsoluteValue.ne_zero_iff Complex.abs).mpr h₁a rw [← h] at this simp at this diff --git a/Nevanlinna/specialFunctions_Integral_log_sin.lean b/Nevanlinna/specialFunctions_Integral_log_sin.lean index 55db7c0..ca37f2f 100644 --- a/Nevanlinna/specialFunctions_Integral_log_sin.lean +++ b/Nevanlinna/specialFunctions_Integral_log_sin.lean @@ -69,7 +69,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log (( exact (Set.mem_Icc.1 hx).2 apply inv_nonneg.mpr (div_nonneg pi_nonneg zero_le_two) _ = 1 := by - apply inv_mul_cancel + apply inv_mul_cancel₀ apply div_ne_zero_iff.mpr constructor · exact pi_ne_zero @@ -87,7 +87,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log (( let B := strictConcaveOn_sin_Icc.concaveOn.2 i₀ i₁ i₂ i₃ i₄ simp [Real.sin_pi_div_two] at B - rw [(by ring_nf; rw [mul_inv_cancel pi_ne_zero, one_mul] : 2 / π * x * (π / 2) = x)] at B + rw [(by ring_nf; rw [mul_inv_cancel₀ pi_ne_zero, one_mul] : 2 / π * x * (π / 2) = x)] at B simpa apply log_le_log l₅ diff --git a/lake-manifest.json b/lake-manifest.json index 54aeae5..a1cb342 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "41bc768e2224d6c75128a877f1d6e198859b3178", + "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5", + "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6058ab8d938c5104eace7d0fb5ac17b21cb067b1", + "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c87908619cccadda23f71262e6898b9893bffa36", + "rev": "a96aee5245720f588876021b6a0aa73efee49c76", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.40", + "inputRev": "v0.0.41", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58", + "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d56e389960165aa122e7c97c098d67e4def09470", + "rev": "cae1b27ace5330f372b57f1051e228fe9b264d57", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 7f0ea50..e7a4f40 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0 +leanprover/lean4:v4.11.0-rc2