Update Mathlib

2024-08-23 09:26:58 +02:00 · 2024-08-23 09:26:58 +02:00 · 2ec1335521
parent 42a6c439a9
commit 2ec1335521
14 changed files with 27 additions and 34 deletions
--- 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
--- 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 :=
--- 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
--- 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) :
--- 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]
--- 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
--- 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

--- 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
--- 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⁻¹
    }
--- 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₁
--- 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
--- 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₅
--- 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,
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0-rc2