From 6001e67b09de06871f22206fa0dfd280b211cb7d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 12 May 2026 02:46:47 -0500 Subject: [PATCH 1/3] Snapshot --- .../Integral/ContourIntegral/Basic.lean | 309 ++++++++++++++++++ .../Integral/IntervalIntegral/Basic.lean | 17 + 2 files changed, 326 insertions(+) create mode 100644 Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean diff --git a/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean new file mode 100644 index 00000000000000..13090f807abe7e --- /dev/null +++ b/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean @@ -0,0 +1,309 @@ +module + +public import Mathlib.MeasureTheory.Integral.CurveIntegral.Basic + +@[expose] public noncomputable section + +open AffineMap MeasureTheory +open scoped unitInterval Convex + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b : ℂ} + +def ContourIntegrable (f : ℂ → E) (γ : Path a b) := + CurveIntegrable (.toSpanSingleton ℂ ∘ f) γ + +/-- TODO -/ +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] 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] +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 + +-- TODO: add `ContinuousLinearMap.toSpanSingleton_neg` +@[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] + +@[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₂ + + +section RestrictScalars + +variable {𝕝 : Type*} [RCLike 𝕝] [NormedSpace 𝕝 F] [NormedSpace 𝕝 E] + [LinearMap.CompatibleSMul E F 𝕝 𝕜] + +@[simp] +theorem contourIntegralFun_restrictScalars : + contourIntegralFun (fun t ↦ (f t).restrictScalars 𝕝) γ = contourIntegralFun f γ := by + ext + letI : NormedSpace ℝ E := .restrictScalars ℝ 𝕜 E + simp [contourIntegralFun_def] + +@[simp] +theorem contourIntegrable_restrictScalars_iff : + ContourIntegrable (fun t ↦ (f t).restrictScalars 𝕝) γ ↔ ContourIntegrable f γ := by + simp [ContourIntegrable] + +@[simp] +theorem contourIntegral_restrictScalars : + ∫ꟲ x in γ, (f x).restrictScalars 𝕝 = ∫ꟲ x in γ, f x := by + letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F + simp [contourIntegral_def] + +end RestrictScalars + +variable {𝕝 : Type*} [RCLike 𝕝] [NormedSpace 𝕝 F] [SMulCommClass 𝕜 𝕝 F] {c : 𝕝} + +@[simp] +theorem contourIntegralFun_smul : contourIntegralFun (c • f) γ = c • contourIntegralFun f γ := by + ext + simp [contourIntegralFun] + +theorem ContourIntegrable.smul (h : ContourIntegrable f γ) : + ContourIntegrable (c • f) γ := by + simpa [ContourIntegrable] using IntervalIntegrable.smul h c + +@[simp] +theorem contourIntegrable_smul_iff : ContourIntegrable (c • f) γ ↔ c = 0 ∨ ContourIntegrable f γ := by + rcases eq_or_ne c 0 with rfl | hc + · simp [ContourIntegrable.zero] + · simp only [hc, false_or] + refine ⟨fun h ↦ ?_, .smul⟩ + simpa [hc] using h.smul (c := c⁻¹) + +@[simp] +theorem contourIntegral_smul : contourIntegral (c • f) γ = c • contourIntegral f γ := by + letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F + simp [contourIntegral_def, intervalIntegral.integral_smul] + +@[simp] +theorem contourIntegral_fun_smul : ∫ꟲ x in γ, c • f x = c • ∫ꟲ x in γ, f x := contourIntegral_smul + +end Algebra + +section FDeriv + +variable {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] + [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] + {a b : E} {s : Set E} {f : ℂ → E} + +/-! +### Derivative of the curve integral w.r.t. the right endpoint + +In this section we prove that the integral of `f` along `[a -[ℝ] b]`, as a function of `b`, +has derivative `f a` at `b = a`. +We provide several versions of this theorem, for `HasFDerivWithinAt` and `HasFDerivAt`, +as well as for continuity near a point and for continuity on the whole set or space. + +Note that we take the derivative at the left endpoint of the segment. +Similar facts about the derivative at a different point are true +provided that `f` is a closed 1-form (formalization WIP, see #24019). +-/ + +/-- The integral of `f` along `[a -[ℝ] b]`, as a function of `b`, has derivative `f a` at `b = a`. +This is a `HasFDerivWithinAt` version assuming that `f` is continuous within a convex set `s` +in a neighborhood of `a` within `s`. -/ +theorem HasFDerivWithinAt.contourIntegral_segment_source' (hs : Convex ℝ s) + (hf : ∀ᶠ x in 𝓝[s] a, ContinuousWithinAt f s x) (ha : a ∈ s) : + HasFDerivWithinAt (∫ꟲ x in .segment a ·, f x) (f a) s a := by + /- Given `ε > 0`, take a number `δ > 0` such that `f` is continuous on `ball a δ ∩ s` + and `‖f z - f a‖ ≤ ε` on this set. + Then for `b ∈ ball a δ ∩ s`, we have + `‖(∫ꟲ x in .segment a b, f x) - f a (b - a)‖ + = ‖(∫ꟲ x in .segment a b, f x) - ∫ꟲ x in .segment a b, f a‖ + ≤ ∫ x in 0..1, ‖f x - f a‖ * ‖b - a‖ + ≤ ε * ‖b - a‖` + -/ + simp only [hasFDerivWithinAt_iff_isLittleO, Path.segment_same, contourIntegral_refl, sub_zero, + Asymptotics.isLittleO_iff] + intro ε hε + obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0, + ball a δ ∩ s ⊆ {z | ContinuousWithinAt f s z ∧ dist (f z) (f a) ≤ ε} := by + rw [← Metric.mem_nhdsWithin_iff, setOf_and, inter_mem_iff] + exact ⟨hf, (hf.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ hε⟩ + rw [eventually_nhdsWithin_iff] + filter_upwards [Metric.ball_mem_nhds _ hδ₀] with b hb hbs + have hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s := + ((convex_ball _ _).inter hs).segment_subset (by simp [*]) (by simp [*]) + rw [← contourIntegral_segment_const, ← contourIntegral_fun_sub] + · refine norm_contourIntegral_segment_le fun z hz ↦ ?_ + simpa [dist_eq_norm] using (hδ (hsub hz)).2 + · rw [contourIntegrable_segment] + refine ContinuousOn.intervalIntegrable_of_Icc zero_le_one fun t ht ↦ ?_ + refine ((hδ ?_).1.eval_const _).comp AffineMap.lineMap_continuous.continuousWithinAt ?_ + · exact hsub <| lineMap_mem_segment ℝ a b ht + · rw [mapsTo_iff_image_subset, ← segment_eq_image_lineMap] + exact hs.segment_subset ha hbs + · rw [contourIntegrable_segment] + exact intervalIntegrable_const + +/-- The integral of `f` along `[a -[ℝ] b]`, as a function of `b`, has derivative `f a` at `b = a`. +This is a `HasFDerivWithinAt` version assuming that `f` is continuous on `s`. -/ +theorem HasFDerivWithinAt.contourIntegral_segment_source (hs : Convex ℝ s) (hf : ContinuousOn f s) + (ha : a ∈ s) : HasFDerivWithinAt (∫ꟲ x in .segment a ·, f x) (f a) s a := + .contourIntegral_segment_source' hs (mem_of_superset self_mem_nhdsWithin hf) ha + +/-- The integral of `f` along `[a -[ℝ] b]`, as a function of `b`, has derivative `f a` at `b = a`. +This is a `HasFDerivAt` version assuming that `f` is continuous in a neighborhood of `a`. -/ +theorem HasFDerivAt.contourIntegral_segment_source' (hf : ∀ᶠ z in 𝓝 a, ContinuousAt f z) : + HasFDerivAt (∫ꟲ x in .segment a ·, f x) (f a) a := + HasFDerivWithinAt.contourIntegral_segment_source' convex_univ + (by simpa only [nhdsWithin_univ, continuousWithinAt_univ]) (mem_univ _) |>.hasFDerivAt_of_univ + +/-- The integral of `f` along `[a -[ℝ] b]`, as a function of `b`, has derivative `f a` at `b = a`. +This is a `HasFDerivAt` version assuming that `f` is continuous on the whole space. -/ +theorem HasFDerivAt.contourIntegral_segment_source (hf : Continuous f) : + HasFDerivAt (∫ꟲ x in .segment a ·, f x) (f a) a := + .contourIntegral_segment_source' <| .of_forall fun _ ↦ hf.continuousAt + +end FDeriv 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 := From 983132ec61ae99365a0e3e9002e59102a36e0657 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 12 May 2026 10:09:09 -0500 Subject: [PATCH 2/3] Fix, add docs --- .../Integral/ContourIntegral/Basic.lean | 167 ++++-------------- .../Integral/CurveIntegral/Basic.lean | 13 +- .../Topology/Algebra/Module/LinearMap.lean | 8 + 3 files changed, 56 insertions(+), 132 deletions(-) diff --git a/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean index 13090f807abe7e..506641cd5d74ff 100644 --- a/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/ContourIntegral/Basic.lean @@ -1,7 +1,21 @@ +/- +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 @@ -9,10 +23,17 @@ 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) γ -/-- TODO -/ +/-- 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) @@ -31,7 +52,6 @@ theorem contourIntegral_eq_intervalIntegral_deriv_smul (f : ℂ → E) (γ : Pat ∫ꟲ x in γ, f x = ∫ t in 0..1, deriv γ.extend t • f (γ.extend t) := by simp [contourIntegral, curveIntegral_eq_intervalIntegral_deriv] - /-! ### Operations on paths -/ @@ -121,9 +141,11 @@ section Algebra variable {f f₁ f₂ : ℂ → E} {γ : Path a b} {t : ℝ} @[to_fun] -protected theorem ContourIntegrable.add (h₁ : ContourIntegrable f₁ γ) (h₂ : ContourIntegrable f₂ γ) : +protected theorem ContourIntegrable.add (h₁ : ContourIntegrable f₁ γ) + (h₂ : ContourIntegrable f₂ γ) : ContourIntegrable (f₁ + f₂) γ := by - simpa [ContourIntegrable] using CurveIntegrable.add h₁ h₂ + 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 @@ -133,7 +155,7 @@ theorem contourIntegral_fun_add (h₁ : ContourIntegrable f₁ γ) (h₂ : Conto ∫ꟲ x in γ, (f₁ x + f₂ x) = ∫ꟲ x in γ, f₁ x + ∫ꟲ x in γ, f₂ x := contourIntegral_add h₁ h₂ -@[to_fun] +@[to_fun (attr := simp)] theorem ContourIntegrable.zero : ContourIntegrable (0 : ℂ → E) γ := by simp [ContourIntegrable] @@ -143,7 +165,6 @@ theorem contourIntegral_zero : contourIntegral (0 : ℂ → E) γ = 0 := by simp @[simp] theorem contourIntegral_fun_zero : ∫ꟲ _ in γ, (0 : E) = 0 := contourIntegral_zero --- TODO: add `ContinuousLinearMap.toSpanSingleton_neg` @[to_fun] theorem ContourIntegrable.neg (h : ContourIntegrable f γ) : ContourIntegrable (-f) γ := by simpa [ContourIntegrable, Function.comp_def, ContinuousLinearMap.toSpanSingleton_neg] @@ -159,12 +180,13 @@ theorem contourIntegrable_fun_neg_iff : ContourIntegrable (-f ·) γ ↔ Contour @[simp] theorem contourIntegral_neg : contourIntegral (-f) γ = -∫ꟲ x in γ, f x := by - simp [contourIntegral] + 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₂ γ) : +protected theorem ContourIntegrable.sub (h₁ : ContourIntegrable f₁ γ) + (h₂ : ContourIntegrable f₂ γ) : ContourIntegrable (f₁ - f₂) γ := sub_eq_add_neg f₁ f₂ ▸ h₁.add h₂.neg @@ -176,134 +198,23 @@ theorem contourIntegral_fun_sub (h₁ : ContourIntegrable f₁ γ) (h₂ : Conto ∫ꟲ x in γ, (f₁ x - f₂ x) = ∫ꟲ x in γ, f₁ x - ∫ꟲ x in γ, f₂ x := contourIntegral_sub h₁ h₂ - -section RestrictScalars - -variable {𝕝 : Type*} [RCLike 𝕝] [NormedSpace 𝕝 F] [NormedSpace 𝕝 E] - [LinearMap.CompatibleSMul E F 𝕝 𝕜] - -@[simp] -theorem contourIntegralFun_restrictScalars : - contourIntegralFun (fun t ↦ (f t).restrictScalars 𝕝) γ = contourIntegralFun f γ := by - ext - letI : NormedSpace ℝ E := .restrictScalars ℝ 𝕜 E - simp [contourIntegralFun_def] +variable {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E] {c : 𝕜} @[simp] -theorem contourIntegrable_restrictScalars_iff : - ContourIntegrable (fun t ↦ (f t).restrictScalars 𝕝) γ ↔ ContourIntegrable f γ := by - simp [ContourIntegrable] +theorem contourIntegrable_smul_iff : + ContourIntegrable (c • f) γ ↔ c = 0 ∨ ContourIntegrable f γ := by + simp [ContourIntegrable, Function.comp_def, ContinuousLinearMap.toSpanSingleton_smul, + curveIntegrable_fun_smul_iff] -@[simp] -theorem contourIntegral_restrictScalars : - ∫ꟲ x in γ, (f x).restrictScalars 𝕝 = ∫ꟲ x in γ, f x := by - letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F - simp [contourIntegral_def] - -end RestrictScalars - -variable {𝕝 : Type*} [RCLike 𝕝] [NormedSpace 𝕝 F] [SMulCommClass 𝕜 𝕝 F] {c : 𝕝} - -@[simp] -theorem contourIntegralFun_smul : contourIntegralFun (c • f) γ = c • contourIntegralFun f γ := by - ext - simp [contourIntegralFun] - -theorem ContourIntegrable.smul (h : ContourIntegrable f γ) : +theorem ContourIntegrable.smul (h : ContourIntegrable f γ) (c : 𝕜) : ContourIntegrable (c • f) γ := by - simpa [ContourIntegrable] using IntervalIntegrable.smul h c - -@[simp] -theorem contourIntegrable_smul_iff : ContourIntegrable (c • f) γ ↔ c = 0 ∨ ContourIntegrable f γ := by - rcases eq_or_ne c 0 with rfl | hc - · simp [ContourIntegrable.zero] - · simp only [hc, false_or] - refine ⟨fun h ↦ ?_, .smul⟩ - simpa [hc] using h.smul (c := c⁻¹) + simp [h] @[simp] theorem contourIntegral_smul : contourIntegral (c • f) γ = c • contourIntegral f γ := by - letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F - simp [contourIntegral_def, intervalIntegral.integral_smul] + simp [contourIntegral, ContinuousLinearMap.toSpanSingleton_smul] @[simp] theorem contourIntegral_fun_smul : ∫ꟲ x in γ, c • f x = c • ∫ꟲ x in γ, f x := contourIntegral_smul end Algebra - -section FDeriv - -variable {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] - [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] - {a b : E} {s : Set E} {f : ℂ → E} - -/-! -### Derivative of the curve integral w.r.t. the right endpoint - -In this section we prove that the integral of `f` along `[a -[ℝ] b]`, as a function of `b`, -has derivative `f a` at `b = a`. -We provide several versions of this theorem, for `HasFDerivWithinAt` and `HasFDerivAt`, -as well as for continuity near a point and for continuity on the whole set or space. - -Note that we take the derivative at the left endpoint of the segment. -Similar facts about the derivative at a different point are true -provided that `f` is a closed 1-form (formalization WIP, see #24019). --/ - -/-- The integral of `f` along `[a -[ℝ] b]`, as a function of `b`, has derivative `f a` at `b = a`. -This is a `HasFDerivWithinAt` version assuming that `f` is continuous within a convex set `s` -in a neighborhood of `a` within `s`. -/ -theorem HasFDerivWithinAt.contourIntegral_segment_source' (hs : Convex ℝ s) - (hf : ∀ᶠ x in 𝓝[s] a, ContinuousWithinAt f s x) (ha : a ∈ s) : - HasFDerivWithinAt (∫ꟲ x in .segment a ·, f x) (f a) s a := by - /- Given `ε > 0`, take a number `δ > 0` such that `f` is continuous on `ball a δ ∩ s` - and `‖f z - f a‖ ≤ ε` on this set. - Then for `b ∈ ball a δ ∩ s`, we have - `‖(∫ꟲ x in .segment a b, f x) - f a (b - a)‖ - = ‖(∫ꟲ x in .segment a b, f x) - ∫ꟲ x in .segment a b, f a‖ - ≤ ∫ x in 0..1, ‖f x - f a‖ * ‖b - a‖ - ≤ ε * ‖b - a‖` - -/ - simp only [hasFDerivWithinAt_iff_isLittleO, Path.segment_same, contourIntegral_refl, sub_zero, - Asymptotics.isLittleO_iff] - intro ε hε - obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0, - ball a δ ∩ s ⊆ {z | ContinuousWithinAt f s z ∧ dist (f z) (f a) ≤ ε} := by - rw [← Metric.mem_nhdsWithin_iff, setOf_and, inter_mem_iff] - exact ⟨hf, (hf.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ hε⟩ - rw [eventually_nhdsWithin_iff] - filter_upwards [Metric.ball_mem_nhds _ hδ₀] with b hb hbs - have hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s := - ((convex_ball _ _).inter hs).segment_subset (by simp [*]) (by simp [*]) - rw [← contourIntegral_segment_const, ← contourIntegral_fun_sub] - · refine norm_contourIntegral_segment_le fun z hz ↦ ?_ - simpa [dist_eq_norm] using (hδ (hsub hz)).2 - · rw [contourIntegrable_segment] - refine ContinuousOn.intervalIntegrable_of_Icc zero_le_one fun t ht ↦ ?_ - refine ((hδ ?_).1.eval_const _).comp AffineMap.lineMap_continuous.continuousWithinAt ?_ - · exact hsub <| lineMap_mem_segment ℝ a b ht - · rw [mapsTo_iff_image_subset, ← segment_eq_image_lineMap] - exact hs.segment_subset ha hbs - · rw [contourIntegrable_segment] - exact intervalIntegrable_const - -/-- The integral of `f` along `[a -[ℝ] b]`, as a function of `b`, has derivative `f a` at `b = a`. -This is a `HasFDerivWithinAt` version assuming that `f` is continuous on `s`. -/ -theorem HasFDerivWithinAt.contourIntegral_segment_source (hs : Convex ℝ s) (hf : ContinuousOn f s) - (ha : a ∈ s) : HasFDerivWithinAt (∫ꟲ x in .segment a ·, f x) (f a) s a := - .contourIntegral_segment_source' hs (mem_of_superset self_mem_nhdsWithin hf) ha - -/-- The integral of `f` along `[a -[ℝ] b]`, as a function of `b`, has derivative `f a` at `b = a`. -This is a `HasFDerivAt` version assuming that `f` is continuous in a neighborhood of `a`. -/ -theorem HasFDerivAt.contourIntegral_segment_source' (hf : ∀ᶠ z in 𝓝 a, ContinuousAt f z) : - HasFDerivAt (∫ꟲ x in .segment a ·, f x) (f a) a := - HasFDerivWithinAt.contourIntegral_segment_source' convex_univ - (by simpa only [nhdsWithin_univ, continuousWithinAt_univ]) (mem_univ _) |>.hasFDerivAt_of_univ - -/-- The integral of `f` along `[a -[ℝ] b]`, as a function of `b`, has derivative `f a` at `b = a`. -This is a `HasFDerivAt` version assuming that `f` is continuous on the whole space. -/ -theorem HasFDerivAt.contourIntegral_segment_source (hf : Continuous f) : - HasFDerivAt (∫ꟲ x in .segment a ·, f x) (f a) a := - .contourIntegral_segment_source' <| .of_forall fun _ ↦ hf.continuousAt - -end FDeriv 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/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 From 5a0c4346883bd2940aaad1c26f2789f26e5db86d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 12 May 2026 10:43:09 -0500 Subject: [PATCH 3/3] mk_all --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) 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