From a1f96806a1a35d113de373091fc4bdf53c4ba753 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 1 Aug 2024 12:38:33 +0200 Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/holomorphic_primitive2.lean | 456 +++++++++++++++++++++++++ 1 file changed, 456 insertions(+) create mode 100644 Nevanlinna/holomorphic_primitive2.lean diff --git a/Nevanlinna/holomorphic_primitive2.lean b/Nevanlinna/holomorphic_primitive2.lean new file mode 100644 index 0000000..5a820e2 --- /dev/null +++ b/Nevanlinna/holomorphic_primitive2.lean @@ -0,0 +1,456 @@ +import Mathlib.Analysis.Complex.TaylorSeries + + +noncomputable def primitive + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] : + ℂ → (ℂ → E) → (ℂ → E) := by + intro z₀ + intro f + exact fun z ↦ (∫ (x : ℝ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ℝ) in z₀.im..z.im, f ⟨z.re, x⟩ + + +theorem primitive_zeroAtBasepoint + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + (f : ℂ → E) + (z₀ : ℂ) : + (primitive z₀ f) z₀ = 0 := by + unfold primitive + simp + + +theorem primitive_fderivAtBasepointZero + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + (f : ℂ → E) + (hf : Continuous f) : + HasDerivAt (primitive 0 f) (f 0) 0 := by + unfold primitive + simp + apply hasDerivAt_iff_isLittleO.2 + simp + rw [Asymptotics.isLittleO_iff] + intro c hc + + have {z : ℂ} {e : E} : z • e = (∫ (_ : ℝ) in (0)..(z.re), e) + Complex.I • ∫ (_ : ℝ) in (0)..(z.im), e:= by + simp + rw [smul_comm] + rw [← smul_assoc] + simp + have : z.re • e = (z.re : ℂ) • e := by exact rfl + rw [this, ← add_smul] + simp + conv => + left + intro x + left + arg 1 + arg 2 + rw [this] + 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 + apply Continuous.intervalIntegrable + apply Continuous.comp + exact hf + have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl + rw [this] + continuity + have t₁ {r : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by + apply Continuous.intervalIntegrable + apply Continuous.comp + exact hf + fun_prop + have t₂ {a b : ℝ} : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by + apply Continuous.intervalIntegrable + apply Continuous.comp hf + have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by + funext x + apply Complex.ext + rw [Complex.add_re] + simp + simp + rw [this] + apply Continuous.add + continuity + fun_prop + + have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by + apply Continuous.intervalIntegrable + apply Continuous.comp + exact hf + fun_prop + conv => + left + intro x + left + arg 1 + rw [this] + rw [← smul_sub] + rw [← intervalIntegral.integral_sub t₀ t₁] + rw [← intervalIntegral.integral_sub t₂ t₃] + rw [Filter.eventually_iff_exists_mem] + + let s := f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)) + have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball + have h₂s : 0 ∈ s := by + apply Set.mem_preimage.mpr + apply Metric.mem_ball_self + linarith + + obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s + + have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by + intro y hy + apply mem_ball_iff_norm.mp (h₂ε hy) + + use Metric.ball 0 (ε / (4 : ℝ)) + constructor + · apply Metric.ball_mem_nhds 0 + linarith + · intro y hy + have h₁y : |y.re| < ε / 4 := by + calc |y.re| + _ ≤ Complex.abs y := by apply Complex.abs_re_le_abs + _ < ε / 4 := by + let A := mem_ball_iff_norm.1 hy + simp at A + linarith + have h₂y : |y.im| < ε / 4 := by + calc |y.im| + _ ≤ Complex.abs y := by apply Complex.abs_im_le_abs + _ < ε / 4 := by + let A := mem_ball_iff_norm.1 hy + simp at A + linarith + + have intervalComputation {x' y' : ℝ} (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by + let A := h.1 + let B := h.2 + rcases le_total 0 y' with hy | hy + · simp [hy] at A + simp [hy] at B + rw [abs_of_nonneg hy] + rw [abs_of_nonneg (le_of_lt A)] + exact B + · simp [hy] at A + simp [hy] at B + rw [abs_of_nonpos hy] + rw [abs_of_nonpos] + linarith [h.1] + exact B + + have t₁ : ‖(∫ (x : ℝ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : ℝ)) * |y.re - 0| := by + apply intervalIntegral.norm_integral_le_of_norm_le_const + intro x hx + + have h₁x : |x| < ε / 4 := by + calc |x| + _ ≤ |y.re| := intervalComputation hx + _ < ε / 4 := h₁y + apply le_of_lt + apply h₃ε { re := x, im := 0 } + rw [mem_ball_iff_norm] + simp + have : { re := x, im := 0 } = (x : ℂ) := by rfl + rw [this] + rw [Complex.abs_ofReal] + linarith + + have t₂ : ‖∫ (x : ℝ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : ℝ)) * |y.im - 0| := by + apply intervalIntegral.norm_integral_le_of_norm_le_const + intro x hx + + have h₁x : |x| < ε / 4 := by + calc |x| + _ ≤ |y.im| := intervalComputation hx + _ < ε / 4 := h₂y + + apply le_of_lt + apply h₃ε { re := y.re, im := x } + simp + + calc Complex.abs { re := y.re, im := x } + _ ≤ |y.re| + |x| := by + apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x } + _ < ε := by + linarith + + 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 + simp + rw [norm_smul] + simp + _ ≤ (c / (4 : ℝ)) * |y.re - 0| + (c / (4 : ℝ)) * |y.im - 0| := by + apply add_le_add + exact t₁ + exact t₂ + _ ≤ (c / (4 : ℝ)) * (|y.re| + |y.im|) := by + simp + rw [mul_add] + _ ≤ (c / (4 : ℝ)) * (4 * ‖y‖) := by + have : |y.re| + |y.im| ≤ 4 * ‖y‖ := by + calc |y.re| + |y.im| + _ ≤ ‖y‖ + ‖y‖ := by + apply add_le_add + apply Complex.abs_re_le_abs + apply Complex.abs_im_le_abs + _ ≤ 4 * ‖y‖ := by + rw [← two_mul] + apply mul_le_mul + linarith + rfl + exact norm_nonneg y + linarith + + apply mul_le_mul + rfl + exact this + apply add_nonneg + apply abs_nonneg + apply abs_nonneg + linarith + _ ≤ c * ‖y‖ := by + linarith + + +theorem primitive_translation + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + (f : ℂ → E) + (z₀ t : ℂ) : + primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by + funext z + unfold primitive + simp + + let g : ℝ → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} ) + have {x : ℝ} : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by + congr 1 + apply Complex.ext <;> simp + conv => + left + left + arg 1 + intro x + rw [this] + rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)] + simp + + congr 1 + let g : ℝ → E := fun x ↦ f ( {re := z.re - t.re, im := x} ) + have {x : ℝ} : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by + congr 1 + apply Complex.ext <;> simp + conv => + left + arg 1 + intro x + rw [this] + rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)] + simp + + +theorem primitive_hasDerivAtBasepoint + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + {f : ℂ → E} + (hf : Continuous f) + (z₀ : ℂ) : + HasDerivAt (primitive z₀ f) (f z₀) z₀ := by + + let g := f ∘ fun z ↦ z + z₀ + have : Continuous g := by continuity + let A := primitive_fderivAtBasepointZero g this + simp at A + + let B := primitive_translation g z₀ z₀ + simp at B + have : (g ∘ fun z ↦ (z - z₀)) = f := by + funext z + dsimp [g] + simp + rw [this] at B + rw [B] + have : f z₀ = (1 : ℂ) • (f z₀) := by + exact (MulAction.one_smul (f z₀)).symm + conv => + arg 2 + rw [this] + + apply HasDerivAt.scomp + simp + have : g 0 = f z₀ := by simp [g] + rw [← this] + exact A + apply HasDerivAt.sub_const + have : (fun (x : ℂ) ↦ x) = id := by + funext x + simp + rw [this] + exact hasDerivAt_id z₀ + + +lemma integrability₁ + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + (f : ℂ → E) + (hf : Differentiable ℂ f) + (a₁ a₂ b : ℝ) : + IntervalIntegrable (fun x => f { re := x, im := b }) MeasureTheory.volume a₁ a₂ := by + apply Continuous.intervalIntegrable + apply Continuous.comp + exact Differentiable.continuous hf + have : ((fun x => { re := x, im := b }) : ℝ → ℂ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by + funext x + apply Complex.ext + rw [Complex.add_re] + simp + rw [Complex.add_im] + simp + rw [this] + continuity + + +lemma integrability₂ + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + (f : ℂ → E) + (hf : Differentiable ℂ f) + (a₁ a₂ b : ℝ) : + IntervalIntegrable (fun x => f { re := b, im := x }) MeasureTheory.volume a₁ a₂ := by + apply Continuous.intervalIntegrable + apply Continuous.comp + exact Differentiable.continuous hf + have : (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by + funext x + apply Complex.ext + rw [Complex.add_re] + simp + simp + rw [this] + apply Continuous.add + continuity + fun_prop + + +theorem primitive_additivity + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + (f : ℂ → E) + (hf : Differentiable ℂ f) + (z₀ z₁ : ℂ) : + (fun z ↦ (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁)) = 0 := by + funext z + + + + unfold primitive + have : (∫ (x : ℝ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ℝ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ℝ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by + rw [intervalIntegral.integral_add_adjacent_intervals] + apply integrability₁ f hf + apply integrability₁ f hf + rw [this] + have : (∫ (x : ℝ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ℝ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ℝ) in z₁.im..z.im, f { re := z.re, im := x }) := by + rw [intervalIntegral.integral_add_adjacent_intervals] + apply integrability₂ f hf + apply integrability₂ f hf + rw [this] + simp + + have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d - h + (c) := by + abel + rw [this] + simp + + let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ (hf.differentiableOn) + have {x : ℝ} {w : ℂ} : ↑x + w.im * Complex.I = { re := x, im := w.im } := by + apply Complex.ext + · simp + · simp + simp_rw [this] at A + have {x : ℝ} {w : ℂ} : w.re + x * Complex.I = { re := w.re, im := x } := by + apply Complex.ext + · simp + · simp + simp_rw [this] at A + rw [← A] + abel + + +theorem primitive_additivity' + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + (f : ℂ → E) + (hf : Differentiable ℂ f) + (z₀ z₁ : ℂ) : + primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by + + nth_rw 1 [← sub_zero (primitive z₀ f)] + rw [← primitive_additivity f hf z₀ z₁] + + funext z + simp + abel + + +theorem primitive_hasDerivAt + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + {f : ℂ → E} + (hf : Differentiable ℂ f) + (z₀ z : ℂ) : + HasDerivAt (primitive z₀ f) (f z) z := by + rw [primitive_additivity' f hf z₀ z] + rw [← add_zero (f z)] + apply HasDerivAt.add + apply primitive_hasDerivAtBasepoint + exact hf.continuous + apply hasDerivAt_const + + +theorem primitive_differentiable + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + {f : ℂ → E} + (hf : Differentiable ℂ f) + (z₀ : ℂ) : + Differentiable ℂ (primitive z₀ f) := by + intro z + exact (primitive_hasDerivAt hf z₀ z).differentiableAt + + +theorem primitive_hasFderivAt + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + {f : ℂ → E} + (hf : Differentiable ℂ f) + (z₀ : ℂ) : + ∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by + intro z + rw [hasFDerivAt_iff_hasDerivAt] + simp + exact primitive_hasDerivAt hf z₀ z + + +theorem primitive_hasFderivAt' + {f : ℂ → ℂ} + (hf : Differentiable ℂ f) + (z₀ : ℂ) : + ∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by + intro z + rw [hasFDerivAt_iff_hasDerivAt] + simp + exact primitive_hasDerivAt hf z₀ z + + +theorem primitive_fderiv + {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] + {f : ℂ → E} + (hf : Differentiable ℂ f) + (z₀ : ℂ) : + ∀ z, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by + intro z + apply HasFDerivAt.fderiv + exact primitive_hasFderivAt hf z₀ z + + +theorem primitive_fderiv' + {f : ℂ → ℂ} + (hf : Differentiable ℂ f) + (z₀ : ℂ) : + ∀ z, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by + intro z + apply HasFDerivAt.fderiv + exact primitive_hasFderivAt' hf z₀ z