diff --git a/Mathlib.lean b/Mathlib.lean index 7385f049d57331..619200eface6ed 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5377,6 +5377,7 @@ public import Mathlib.MeasureTheory.Integral.CircleAverage public import Mathlib.MeasureTheory.Integral.CircleIntegral public import Mathlib.MeasureTheory.Integral.CircleTransform public import Mathlib.MeasureTheory.Integral.CompactlySupported +public import Mathlib.MeasureTheory.Integral.ContourIntegral.Basic public import Mathlib.MeasureTheory.Integral.CurveIntegral.Basic public import Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare public import Mathlib.MeasureTheory.Integral.DivergenceTheorem diff --git a/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean new file mode 100644 index 00000000000000..506641cd5d74ff --- /dev/null +++ b/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean @@ -0,0 +1,220 @@ +/- +Copyright (c) 2026 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov +-/ +module +public import Mathlib.MeasureTheory.Integral.CurveIntegral.Basic + +/-! +# Contour integrals + +In this file we specialize the definition of `curveIntegral` to paths in `ℂ`. +In this case, we integrate functions instead of 1-forms, +interpreting a function `f` as the 1-form `f(z)dz`, +written as `ContinuousLinearMap.toSpanSingleton ℂ ∘ f`. +-/ + + +@[expose] public noncomputable section + +open AffineMap MeasureTheory +open scoped unitInterval Convex + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℂ} + +/-- A function `f : ℂ → E` is *contour integrable* along a path `γ`, +if the 1-form $f(z)\,dz$ is curve integrable along `γ`. + +Equivalently, this means that `φ(t)=γ'(t)•f(γ(t))` is interval integrable on `[0, 1]`. -/ +def ContourIntegrable (f : ℂ → E) (γ : Path a b) := + CurveIntegrable (.toSpanSingleton ℂ ∘ f) γ + +/-- The *contour integral* of a function `f : ℂ → E` along a path `γ`, +defined as the curve integral of $f(z)\,dz$ along `γ`. + +Equivalently, this is given by the integral of `γ'(t)•f(t)` along `[0, 1]`. -/ +def contourIntegral (f : ℂ → E) (γ : Path a b) : E := + ∫ᶜ x in γ, .toSpanSingleton ℂ (f x) + +@[inherit_doc contourIntegral] +notation3 "∫ꟲ "(...)" in " γ ", "r:67:(scoped f => contourIntegral f γ) => r + +theorem contourIntegral_of_not_completeSpace (h : ¬CompleteSpace E) + (f : ℂ → E) (γ : Path a b) : ∫ꟲ x in γ, f x = 0 := by + rw [contourIntegral, curveIntegral_of_not_completeSpace h] + +theorem contourIntegral_eq_intervalIntegral_derivWithin_smul (f : ℂ → E) (γ : Path a b) : + ∫ꟲ x in γ, f x = ∫ t in 0..1, derivWithin γ.extend I t • f (γ.extend t) := by + simp [contourIntegral, curveIntegral_def, curveIntegralFun_def] + +theorem contourIntegral_eq_intervalIntegral_deriv_smul (f : ℂ → E) (γ : Path a b) : + ∫ꟲ x in γ, f x = ∫ t in 0..1, deriv γ.extend t • f (γ.extend t) := by + simp [contourIntegral, curveIntegral_eq_intervalIntegral_deriv] + +/-! +### Operations on paths +-/ + +section PathOperations + +variable {c d : ℂ} {f : ℂ → E} {γ γab : Path a b} {γbc : Path b c} {t : ℝ} + +@[simp] +theorem contourIntegral_refl (f : ℂ → E) (a : ℂ) : ∫ꟲ x in .refl a, f x = 0 := by + simp [contourIntegral] + +@[simp] +theorem ContourIntegrable.refl (f : ℂ → E) (a : ℂ) : ContourIntegrable f (.refl a) := + CurveIntegrable.refl .. + +@[simp] +theorem contourIntegral_cast (f : ℂ → E) (γ : Path a b) (hc : c = a) (hd : d = b) : + ∫ꟲ x in γ.cast hc hd, f x = ∫ꟲ x in γ, f x := by + simp [contourIntegral] + +@[simp] +theorem contourIntegrable_cast_iff (hc : c = a) (hd : d = b) : + ContourIntegrable f (γ.cast hc hd) ↔ ContourIntegrable f γ := by + simp [ContourIntegrable] + +protected alias ⟨_, ContourIntegrable.cast⟩ := curveIntegrable_cast_iff + +protected theorem ContourIntegrable.symm (h : ContourIntegrable f γ) : + ContourIntegrable f γ.symm := + CurveIntegrable.symm h + +@[simp] +theorem contourIntegrable_symm : ContourIntegrable f γ.symm ↔ ContourIntegrable f γ := + ⟨fun h ↦ by simpa using h.symm, .symm⟩ + +@[simp] +theorem contourIntegral_symm (f : ℂ → E) (γ : Path a b) : + ∫ꟲ x in γ.symm, f x = -∫ꟲ x in γ, f x := by + simp [contourIntegral] + +protected theorem ContourIntegrable.trans (h₁ : ContourIntegrable f γab) + (h₂ : ContourIntegrable f γbc) : + ContourIntegrable f (γab.trans γbc) := + CurveIntegrable.trans h₁ h₂ + +theorem contourIntegral_trans (h₁ : ContourIntegrable f γab) (h₂ : ContourIntegrable f γbc) : + ∫ꟲ x in γab.trans γbc, f x = (∫ꟲ x in γab, f x) + ∫ꟲ x in γbc, f x := + curveIntegral_trans h₁ h₂ + +theorem contourIntegrable_segment : + ContourIntegrable f (.segment a b) ↔ + a = b ∨ IntervalIntegrable (fun t ↦ f (lineMap a b t)) volume 0 1 := by + simp [ContourIntegrable, curveIntegrable_segment, sub_eq_zero, @eq_comm _ a] + +theorem contourIntegral_segment (f : ℂ → E) (a b : ℂ) : + ∫ꟲ x in .segment a b, f x = (b - a) • ∫ t in 0..1, f (lineMap a b t) := by + simp [contourIntegral, curveIntegral_segment] + +@[simp] +theorem contourIntegral_segment_const [CompleteSpace E] (a b : ℂ) (y : E) : + ∫ꟲ _ in .segment a b, y = (b - a) • y := by + simp [contourIntegral_segment] + +/-- If `‖f z‖ ≤ C` at all points of the segment `[a -[ℝ] b]`, +then the contour integral `∫ꟲ x in .segment a b, f x` has norm at most `C * ‖b - a‖`. -/ +theorem norm_contourIntegral_segment_le {C : ℝ} (h : ∀ z ∈ [a -[ℝ] b], ‖f z‖ ≤ C) : + ‖∫ꟲ x in .segment a b, f x‖ ≤ C * ‖b - a‖ := + norm_curveIntegral_segment_le <| by simpa + +/-- If a function `f` is continuous on a set `s`, +then it is contour integrable along any $C^1$ path in this set. -/ +theorem ContinuousOn.contourIntegrable_of_contDiffOn {s : Set ℂ} + (hf : ContinuousOn f s) (hγ : ContDiffOn ℝ 1 γ.extend I) (hγs : ∀ t, γ t ∈ s) : + ContourIntegrable f γ := by + refine ContinuousOn.curveIntegrable_of_contDiffOn ?_ hγ hγs + exact ContinuousLinearMap.toSpanSingletonCLE.continuous.comp_continuousOn hf + +end PathOperations + +/-! +### Algebraic operations on the function +-/ + +section Algebra + +variable {f f₁ f₂ : ℂ → E} {γ : Path a b} {t : ℝ} + +@[to_fun] +protected theorem ContourIntegrable.add (h₁ : ContourIntegrable f₁ γ) + (h₂ : ContourIntegrable f₂ γ) : + ContourIntegrable (f₁ + f₂) γ := by + simpa [ContourIntegrable, Function.comp_def, ContinuousLinearMap.toSpanSingleton_add] + using CurveIntegrable.add h₁ h₂ + +theorem contourIntegral_add (h₁ : ContourIntegrable f₁ γ) (h₂ : ContourIntegrable f₂ γ) : + contourIntegral (f₁ + f₂) γ = ∫ꟲ x in γ, f₁ x + ∫ꟲ x in γ, f₂ x := by + simpa [contourIntegral, ContinuousLinearMap.toSpanSingleton_add] using curveIntegral_add h₁ h₂ + +theorem contourIntegral_fun_add (h₁ : ContourIntegrable f₁ γ) (h₂ : ContourIntegrable f₂ γ) : + ∫ꟲ x in γ, (f₁ x + f₂ x) = ∫ꟲ x in γ, f₁ x + ∫ꟲ x in γ, f₂ x := + contourIntegral_add h₁ h₂ + +@[to_fun (attr := simp)] +theorem ContourIntegrable.zero : ContourIntegrable (0 : ℂ → E) γ := by + simp [ContourIntegrable] + +@[simp] +theorem contourIntegral_zero : contourIntegral (0 : ℂ → E) γ = 0 := by simp [contourIntegral] + +@[simp] +theorem contourIntegral_fun_zero : ∫ꟲ _ in γ, (0 : E) = 0 := contourIntegral_zero + +@[to_fun] +theorem ContourIntegrable.neg (h : ContourIntegrable f γ) : ContourIntegrable (-f) γ := by + simpa [ContourIntegrable, Function.comp_def, ContinuousLinearMap.toSpanSingleton_neg] + using CurveIntegrable.neg h + +@[simp] +theorem contourIntegrable_neg_iff : ContourIntegrable (-f) γ ↔ ContourIntegrable f γ := + ⟨fun h ↦ by simpa using h.neg, .neg⟩ + +@[simp] +theorem contourIntegrable_fun_neg_iff : ContourIntegrable (-f ·) γ ↔ ContourIntegrable f γ := + contourIntegrable_neg_iff + +@[simp] +theorem contourIntegral_neg : contourIntegral (-f) γ = -∫ꟲ x in γ, f x := by + simp [contourIntegral, ContinuousLinearMap.toSpanSingleton_neg] + +@[simp] +theorem contourIntegral_fun_neg : ∫ꟲ x in γ, -f x = -∫ꟲ x in γ, f x := contourIntegral_neg + +protected theorem ContourIntegrable.sub (h₁ : ContourIntegrable f₁ γ) + (h₂ : ContourIntegrable f₂ γ) : + ContourIntegrable (f₁ - f₂) γ := + sub_eq_add_neg f₁ f₂ ▸ h₁.add h₂.neg + +theorem contourIntegral_sub (h₁ : ContourIntegrable f₁ γ) (h₂ : ContourIntegrable f₂ γ) : + contourIntegral (f₁ - f₂) γ = ∫ꟲ x in γ, f₁ x - ∫ꟲ x in γ, f₂ x := by + rw [sub_eq_add_neg, sub_eq_add_neg, contourIntegral_add h₁ h₂.neg, contourIntegral_neg] + +theorem contourIntegral_fun_sub (h₁ : ContourIntegrable f₁ γ) (h₂ : ContourIntegrable f₂ γ) : + ∫ꟲ x in γ, (f₁ x - f₂ x) = ∫ꟲ x in γ, f₁ x - ∫ꟲ x in γ, f₂ x := + contourIntegral_sub h₁ h₂ + +variable {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {c : 𝕜} + +@[simp] +theorem contourIntegrable_smul_iff : + ContourIntegrable (c • f) γ ↔ c = 0 ∨ ContourIntegrable f γ := by + simp [ContourIntegrable, Function.comp_def, ContinuousLinearMap.toSpanSingleton_smul, + curveIntegrable_fun_smul_iff] + +theorem ContourIntegrable.smul (h : ContourIntegrable f γ) (c : 𝕜) : + ContourIntegrable (c • f) γ := by + simp [h] + +@[simp] +theorem contourIntegral_smul : contourIntegral (c • f) γ = c • contourIntegral f γ := by + simp [contourIntegral, ContinuousLinearMap.toSpanSingleton_smul] + +@[simp] +theorem contourIntegral_fun_smul : ∫ꟲ x in γ, c • f x = c • ∫ꟲ x in γ, f x := contourIntegral_smul + +end Algebra diff --git a/Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean index 0500efc9c74d45..795377f3357e58 100644 --- a/Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean @@ -377,7 +377,7 @@ theorem curveIntegralFun_zero : curveIntegralFun (0 : E → E →L[𝕜] F) γ = theorem curveIntegralFun_fun_zero : curveIntegralFun (fun _ ↦ 0 : E → E →L[𝕜] F) γ = 0 := curveIntegralFun_zero -@[to_fun] +@[to_fun (attr := simp)] theorem CurveIntegrable.zero : CurveIntegrable (0 : E → E →L[𝕜] F) γ := by simp [CurveIntegrable, IntervalIntegrable.zero] @@ -460,7 +460,7 @@ theorem curveIntegralFun_smul : curveIntegralFun (c • ω) γ = c • curveInte ext simp [curveIntegralFun] -theorem CurveIntegrable.smul (h : CurveIntegrable ω γ) : +theorem CurveIntegrable.smul (h : CurveIntegrable ω γ) (c : 𝕝) : CurveIntegrable (c • ω) γ := by simpa [CurveIntegrable] using IntervalIntegrable.smul h c @@ -469,8 +469,13 @@ theorem curveIntegrable_smul_iff : CurveIntegrable (c • ω) γ ↔ c = 0 ∨ C rcases eq_or_ne c 0 with rfl | hc · simp [CurveIntegrable.zero] · simp only [hc, false_or] - refine ⟨fun h ↦ ?_, .smul⟩ - simpa [hc] using h.smul (c := c⁻¹) + refine ⟨fun h ↦ ?_, (.smul · c)⟩ + simpa [hc] using h.smul c⁻¹ + +@[simp] +theorem curveIntegrable_fun_smul_iff : + CurveIntegrable (c • ω ·) γ ↔ c = 0 ∨ CurveIntegrable ω γ := + curveIntegrable_smul_iff @[simp] theorem curveIntegral_smul : curveIntegral (c • ω) γ = c • curveIntegral ω γ := by diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean index 0ad3a9f100f3c7..3b1dfc7a7bc1e1 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean @@ -304,11 +304,28 @@ end variable [NormedRing A] {f g : ℝ → ε} {a b : ℝ} {μ : Measure ℝ} +@[to_fun] theorem smul {R : Type*} [NormedAddCommGroup R] [SMulZeroClass R E] [IsBoundedSMul R E] {f : ℝ → E} (h : IntervalIntegrable f μ a b) (r : R) : IntervalIntegrable (r • f) μ a b := ⟨h.1.smul r, h.2.smul r⟩ +@[simp] +theorem _root_.intervalIntegrable_smul_iff {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 E] + {f : ℝ → E} {c : 𝕜} : + IntervalIntegrable (c • f) μ a b ↔ c = 0 ∨ IntervalIntegrable f μ a b := by + rcases eq_or_ne c 0 with rfl | hc + · simp [IntervalIntegrable.zero] + · simp only [hc, false_or] + refine ⟨fun h ↦ ?_, (.smul · c)⟩ + simpa [hc] using h.smul c⁻¹ + +@[simp] +theorem _root_.intervalIntegrable_fun_smul_iff {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 E] + {f : ℝ → E} {c : 𝕜} : + IntervalIntegrable (c • f ·) μ a b ↔ c = 0 ∨ IntervalIntegrable f μ a b := + intervalIntegrable_smul_iff + @[simp] theorem add [ContinuousAdd ε] (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) : IntervalIntegrable (fun x => f x + g x) μ a b := diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean index 9e10ba35a06a14..0feaffb4b169fe 100644 --- a/Mathlib/Topology/Algebra/Module/LinearMap.lean +++ b/Mathlib/Topology/Algebra/Module/LinearMap.lean @@ -928,6 +928,14 @@ instance ring [IsTopologicalAddGroup M] : Ring (M →L[R] M) where theorem intCast_apply [IsTopologicalAddGroup M] (z : ℤ) (m : M) : (↑z : M →L[R] M) m = z • m := rfl +theorem toSpanSingleton_neg [TopologicalSpace R] [ContinuousSMul R M] [IsTopologicalAddGroup M] + (a : M) : toSpanSingleton R (-a) = -toSpanSingleton R a := by + ext; simp + +theorem toSpanSingleton_sub [TopologicalSpace R] [ContinuousSMul R M] [IsTopologicalAddGroup M] + (a b : M) : toSpanSingleton R (a - b) = toSpanSingleton R a - toSpanSingleton R b := by + simp [sub_eq_add_neg, toSpanSingleton_add, toSpanSingleton_neg] + theorem toSpanSingleton_pow [TopologicalSpace R] [IsTopologicalRing R] (c : R) (n : ℕ) : toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n) := by induction n with