working…

Nevanlinna/holomorphic.primitive.lean

@@ -1,5 +1,6 @@
 import Mathlib.Analysis.Complex.TaylorSeries
 import Mathlib.MeasureTheory.Integral.DivergenceTheorem
+import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Nevanlinna.cauchyRiemann
 import Nevanlinna.partialDeriv
@@ -166,8 +167,8 @@ theorem primitive_lem1
     rw [this, ← add_smul]
     simp
   rw [this]
-  
-  have hc : HasDerivAt (fun (w : ℂ) ↦ w) 1 0 := by 
+
+  have hc : HasDerivAt (fun (w : ℂ) ↦ w) 1 0 := by
     apply hasDerivAt_id'
   nth_rewrite 2 [← (one_smul ℂ v)]
   exact HasDerivAt.smul_const hc v
@@ -176,7 +177,7 @@ theorem primitive_lem1
 
 theorem primitive_fderivAtBasepoint
   {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
-  (f : ℂ  → E) 
+  (f : ℂ  → E)
   (hf : Continuous f) :
   HasDerivAt (primitive 0 f) (f 0) 0 := by
   unfold primitive
@@ -186,7 +187,7 @@ theorem primitive_fderivAtBasepoint
   rw [Asymptotics.isLittleO_iff]
   intro c hc
 
-  have {z : ℂ} {e : E} : z • e = (∫ (x : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (x : ℝ) in (0)..(z.im), e:= by 
+  have {z : ℂ} {e : E} : z • e = (∫ (x : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (x : ℝ) in (0)..(z.im), e:= by
     simp
     rw [smul_comm]
     rw [← smul_assoc]
@@ -201,7 +202,7 @@ theorem primitive_fderivAtBasepoint
     arg 1
     arg 2
     rw [this]
-  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by 
+  have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
     abel
   have t₀ {r : ℝ} : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by sorry
   have t₁ {r : ℝ} :IntervalIntegrable (fun x => f 0) MeasureTheory.volume 0 r := by sorry
@@ -219,48 +220,51 @@ theorem primitive_fderivAtBasepoint
   rw [Filter.eventually_iff_exists_mem]
 
   let s := f⁻¹' Metric.ball (f 0) c
-  have : IsOpen s := by
-    apply IsOpen.mem_nhds
-    apply IsOpen.preimage hf
-    exact Metric.isOpen_ball
-  
-
-  --sorry
-  --apply isOpen_iff_ball_subset
-
-  use s
-  constructor
-  · apply IsOpen.mem_nhds
-    apply IsOpen.preimage hf
-    exact Metric.isOpen_ball
-    apply Set.mem_preimage.mpr 
+  have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball
+  have h₂s : 0 ∈ s := by
+    apply Set.mem_preimage.mpr
     exact Metric.mem_ball_self hc
+
+  obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s
+
+  have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < c := by
+    intro y hy
+    exact mem_ball_iff_norm.mp (h₂ε hy)
+
+  use Metric.ball 0 ε
+  constructor
+  · exact Metric.ball_mem_nhds 0 h₁ε
   · intro y hy
-    have : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ c * |y.re| := by
-      let A := intervalIntegral.norm_integral_le_of_norm_le_const_ae
-      
+    have h₁y : |y.re| < ε := by
 
       sorry
 
+    have : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ c * |y.re - 0| := by
+      apply intervalIntegral.norm_integral_le_of_norm_le_const
+      intro x hx
+      have h₁x : |x| < ε := by sorry
+      apply le_of_lt
+      apply h₃ε { re := x, im := 0 }
+      simp
+      have : { re := x, im := 0 } = (x : ℂ) := by rfl
+      rw [this]
+      rw [Complex.abs_ofReal]
+      exact h₁x
+
+    sorry
+    /-
     calc ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
       _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by apply norm_add_le
-      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by 
+      _ ≤ ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
         simp
         rw [norm_smul]
         simp
-      _ ≤ |(∫ (x : ℝ) in (0)..(y.re), ‖f { re := x, im := 0 } - f 0‖)| + |∫ (x : ℝ) in (0)..(y.im), ‖f { re := y.re, im := x } - f 0‖| := by 
+      _ ≤ |(∫ (x : ℝ) in (0)..(y.re), ‖f { re := x, im := 0 } - f 0‖)| + |∫ (x : ℝ) in (0)..(y.im), ‖f { re := y.re, im := x } - f 0‖| := by
         apply add_le_add
         apply intervalIntegral.norm_integral_le_abs_integral_norm
         apply intervalIntegral.norm_integral_le_abs_integral_norm
-      _ ≤ 
-        
-
-
-
-  
-
-
-
+      _ ≤
+    -/
 
 
   sorry

Nevanlinna/smulImprovement.lean

@@ -0,0 +1,40 @@
+import Mathlib.Analysis.Complex.CauchyIntegral
+--import Mathlib.Analysis.Complex.Module
+
+
+
+example simplificationTest₁
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E]
+  {v : E}
+  {z : ℂ} :
+  z • v =  z.re • v + Complex.I • z.im • v := by
+
+  /-
+  An attempt to write  "rw [add_smul]" will fail with "did not find instance of
+  the pattern in the target -- expression (?r + ?s) • ?x".
+  -/
+  sorry
+
+
+theorem add_smul'
+  (𝕜₁ : Type*) [NontriviallyNormedField ℝ]
+  {𝕜₂ : Type*} [NontriviallyNormedField ℂ] [NormedAlgebra ℝ ℂ]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
+  {v : E}
+  {r s : ℂ} :
+  (r + s) • v = r • v + s • v :=
+  Module.add_smul r s v
+
+
+theorem smul_add' (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂ :=
+  DistribSMul.smul_add _ _ _
+#align smul_add smul_add
+
+
+
+
+example simplificationTest₂
+  {v : E}
+  {z : ℂ} :
+  z • v =  z.re • v + Complex.I • z.im • v := by
+  sorry