1.1 Integration and classical domains
This chapter fixes the domains and notation used in the analytic results. It is a reference: the approximation path begins in Chapter 2.1.
1.1.1 Integrable functions and weights
The notation \(\mathcal I(\mu )\) records when an integral exists. A weight on an open interval defines a measure on \(\mathbb {R}\) by assigning no mass outside that interval.
For a measure \(\mu \) on a measurable space \(X\), let \(\mathcal I(\mu )\) be the set of functions \(f:X\to \mathbb {R}\) that are \(\mu \)-integrable.
Lean Formalisation
def MeasureTheory.IntegrableInput.{u_1} {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) : Type u_1Lean definition
/-- Real integrable functions, retaining pointwise representatives (DLMF 18.2). -/
abbrev IntegrableInput {X : Type*} [MeasurableSpace X] (μ : Measure X) :=
{f : X → ℝ // Integrable f μ}For \(a,b\in \mathbb {R}\) and a continuous \(w:(a,b)\to \mathbb {R}_{\ge 0}\), form \(w\, dx\) on the open interval \((a,b)\), then push it forward to \(\mathbb {R}\) by inclusion. Denote this measure by \(\mu _w\).
Lean Formalisation
def MeasureTheory.openIntervalWeightMeasure (a b : ℝ) (w : C(↑(Set.Ioo a b), NNReal)) : MeasureTheory.Measure ℝLean definition
/-- A continuous nonnegative density on an open interval, pushed to the real line.
Reference: DLMF 18.2(i). -/
def openIntervalWeightMeasure (a b : ℝ) (w : C(Ioo a b, ℝ≥0)) : Measure ℝ :=
Measure.map Subtype.val (volume.withDensity fun x : Ioo a b ↦ (w x : ℝ≥0∞))A function \(f:\mathbb {R}\to \mathbb {R}\) is \(\mu _w\)-integrable if and only if \(x\mapsto w(x)f(x)\) is Lebesgue-integrable on the open interval \((a,b)\). For \(f\in \mathcal I(\mu _w)\),
Both integrals exist as finite real integrals.
Lean Formalisation
theorem MeasureTheory.integrable_openIntervalWeightMeasure_iff (a b : ℝ) (w : C(↑(Set.Ioo a b), NNReal)) (f : ℝ → ℝ) :
MeasureTheory.Integrable f (MeasureTheory.openIntervalWeightMeasure a b w) ↔
MeasureTheory.Integrable (fun x => ↑(w x) * f ↑x) MeasureTheory.volumeLean proof
/-- Integrability is exactly integrability of the weighted subtype function. -/
theorem integrable_openIntervalWeightMeasure_iff (a b : ℝ) (w : C(Ioo a b, ℝ≥0))
(f : ℝ → ℝ) :
Integrable f (openIntervalWeightMeasure a b w) ↔
Integrable (fun x : Ioo a b ↦ (w x : ℝ) * f x) volume := by
rw [openIntervalWeightMeasure,
(MeasurableEmbedding.subtype_coe measurableSet_Ioo).integrable_map_iff,
integrable_withDensity_iff_integrable_coe_smul w.continuous.measurable]
rflIntegrability of functions in the domain
Every \(f\in \mathcal I(\mu )\) is \(\mu \)-integrable.
Lean Formalisation
theorem MeasureTheory.IntegrableInput.integrable.{u_1} {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
(f : MeasureTheory.IntegrableInput μ) : MeasureTheory.Integrable (↑f) μLean proof
/-- A bundled input has a genuine finite integral. -/
theorem IntegrableInput.integrable {X : Type*} [MeasurableSpace X] {μ : Measure X}
(f : IntegrableInput μ) : Integrable f.val μ := f.property1.1.2 Derivatives and their domains
Derivatives on open sets are local. For absolutely continuous real functions, the derivative representative need only agree with the derivative almost everywhere.
Let \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). Let \(U\subseteq \mathbb K\) be open, \(f:U\to \mathbb K\), \(x\in U\) and \(d\in \mathbb K\). Say that \(f\) has derivative \(d\) at \(x\) if there exists \(F:\mathbb K\to \mathbb K\) agreeing with \(f\) on \(U\) such that \(F'(x)\) exists and equals \(d\).
Lean Formalisation
def HasDerivAtOnOpen.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜) (f : ↥U → 𝕜) (d : 𝕜)
(x : ↥U) : PropLean definition
/-- Differentiation of a function whose point type is an open scalar domain. -/
def HasDerivAtOnOpen (U : TopologicalSpace.Opens 𝕜) (f : U → 𝕜)
(d : 𝕜) (x : U) : Prop :=
∃ g : 𝕜 → 𝕜, (∀ y : U, g y = f y) ∧ HasDerivAt g d xLet \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). For every extension \(F\) agreeing with \(f\) on \(U\), the open-domain derivative condition is equivalent to \(F'(x)=d\) with the derivative existing. The derivative value is unique. If \(f'(x)=d\) and \(g'(x)=e\), then \((fg)'(x)=d\, g(x)+f(x)e\) and \((cf)'(x)=cd\) for every \(c\in \mathbb K\).
Lean Formalisation
theorem hasDerivAtOnOpen_iff.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜) (f : ↥U → 𝕜)
(d : 𝕜) (x : ↥U) (g : 𝕜 → 𝕜) (hg : ∀ (y : ↥U), g ↑y = f y) : HasDerivAtOnOpen U f d x ↔ HasDerivAt g d ↑xLean proof
/-- A derivative is independent of the chosen extension off the open domain. -/
theorem hasDerivAtOnOpen_iff (U : TopologicalSpace.Opens 𝕜) (f : U → 𝕜)
(d : 𝕜) (x : U) (g : 𝕜 → 𝕜) (hg : ∀ y : U, g y = f y) :
HasDerivAtOnOpen U f d x ↔ HasDerivAt g d x := by
constructor
· rintro ⟨h, hh, hd⟩
apply hd.congr_of_eventuallyEq
filter_upwards [U.isOpen.mem_nhds x.property] with y hy
exact (hg ⟨y, hy⟩).trans (hh ⟨y, hy⟩).symm
· intro hd
exact ⟨g, hg, hd⟩For \(F:\mathbb R\to \mathbb R\) and a measure \(\mu \) on \(\mathbb R\), let \(\mathcal D_\mu (F)\) consist of the integrable functions \(h\in \mathcal I(\mu )\) for which \(F\) has derivative \(h(x)\) at \(\mu \)-almost every \(x\). This is an almost-everywhere derivative representation; no derivative is asserted at the exceptional points.
Lean Formalisation
inductive IntegrableDerivative (f : ℝ → ℝ) (μ : MeasureTheory.Measure ℝ) : TypeLean definition
/-- An integrable representative of a derivative, with existence certified a.e. -/
structure IntegrableDerivative (f : ℝ → ℝ) (μ : Measure ℝ) where
input : IntegrableInput μ
hasDerivAt : ∀ᵐ x ∂μ, HasDerivAt f (input.val x) xEvery member of \(\mathcal D_\mu (F)\) is integrable, and any two members agree \(\mu \)-almost everywhere. If \(F\) is absolutely continuous on the closed interval with endpoints \(a,b\), then \(\mathcal D_\mu (F)\) is nonempty for Lebesgue measure restricted to that interval.
Lean Formalisation
theorem IntegrableDerivative.integrable {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (g : IntegrableDerivative f μ) :
MeasureTheory.Integrable (↑g.input) μLean proof
theorem integrable {f : ℝ → ℝ} {μ : Measure ℝ} (g : IntegrableDerivative f μ) :
Integrable g μ := g.input.propertyLet \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). For open \(U\subseteq \mathbb K\), write \(D_U^n f=g\) when there is a chain \(f_0=f,f_1,\ldots ,f_n=g\) of functions \(U\to \mathbb K\) such that \(f_{k+1}(x)\) is the derivative of \(f_k\) at every \(x\in U\), for every \(k{\lt}n\).
Lean Formalisation
def HasIteratedDerivOnOpen.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜) :
ℕ → (↥U → 𝕜) → (↥U → 𝕜) → PropLean definition
/-- Iterated derivatives through a chain of genuine derivatives on an open domain. -/
def HasIteratedDerivOnOpen (U : TopologicalSpace.Opens 𝕜) :
ℕ → (U → 𝕜) → (U → 𝕜) → Prop
| 0, f, g => f = g
| n + 1, f, g => ∃ h, HasIteratedDerivOnOpen U n f h ∧
∀ x, HasDerivAtOnOpen U h (g x) xLet \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). For an open set \(U\subseteq \mathbb K\) and \(n\ge 0\), let \(\mathcal D^n(U)\) consist of functions \(f:U\to \mathbb K\) possessing a derivative chain of order \(n\). For \(f\in \mathcal D^n(U)\) define \(D_U^n f\) to be the unique final function of that chain. No value is assigned without such a chain.
Lean Formalisation
def IteratedDerivInput.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜) (n : ℕ) : Type u_1Lean definition
/-- Functions possessing a derivative chain of the specified order. -/
abbrev IteratedDerivInput (U : TopologicalSpace.Opens 𝕜) (n : ℕ) :=
{f : U → 𝕜 // ∃ g, HasIteratedDerivOnOpen U n f g}Let \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)), let \(U\subseteq \mathbb K\) be open, and let \(f:U\to \mathbb K\). We call \(f\) analytic on \(U\) if, for every \(x\in U\), there exist a function \(F:\mathbb K\to \mathbb K\), coefficients \(a_n\in \mathbb K\) for \(n\in \mathbb N\), and \(r\in (0,\infty ]\) such that:
\(F(y)=f(y)\) for every \(y\in U\);
\(r\le R\), where the supremum is taken in \([0,\infty ]\) and
\[ R=\sup \left\{ s\ge 0:\ \exists C\in \mathbb R,\quad \| a_n\| s^n\le C\text{ for every }n\in \mathbb N\right\} ; \]for every \(h\in \mathbb K\) with \(\| h\| {\lt}r\), the partial sums
\[ \sum _{n=0}^{N-1}a_nh^n \]converge to \(F(x+h)\) as \(N\to \infty \).
Lean Formalisation
def AnalyticOnOpen.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜) (f : ↥U → 𝕜) : PropLean definition
/-- Analyticity of a function with an open domain in its point type. -/
def AnalyticOnOpen (U : TopologicalSpace.Opens 𝕜) (f : U → 𝕜) : Prop :=
∀ x : U, ∃ g : 𝕜 → 𝕜, (∀ y : U, g y = f y) ∧ AnalyticAt 𝕜 g xLet \(\mathbb K\) be a complete nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)), and let \(U\subseteq \mathbb K\) be open. Every analytic function \(f:U\to \mathbb K\) belongs to \(\mathcal D^n(U)\) for every \(n\ge 0\).
Lean Formalisation
theorem AnalyticOnOpen.exists_iteratedDeriv.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
{U : TopologicalSpace.Opens 𝕜} {f : ↥U → 𝕜} (hf : AnalyticOnOpen U f) (n : ℕ) : ∃ g, HasIteratedDerivOnOpen U n f gLean proof
/-- An analytic function on a typed open domain has derivatives of every order. -/
theorem AnalyticOnOpen.exists_iteratedDeriv {U : TopologicalSpace.Opens 𝕜}
{f : U → 𝕜} (hf : AnalyticOnOpen U f) (n : ℕ) :
∃ g, HasIteratedDerivOnOpen U n f g := by
classical
by_cases hU : Nonempty U
· obtain ⟨x⟩ := hU
obtain ⟨F, hF, _⟩ := hf x
have ha := (analyticOnOpen_iff U f F hF).mp hf
have hd := hasIteratedDerivOnOpen_of_analytic_extension U F ha n
have he : (fun x : U ↦ F x) = f := funext hF
rw [he] at hd
exact ⟨_, hd⟩
· have : IsEmpty U := ⟨fun x ↦ hU ⟨x⟩⟩
refine ⟨f, ?_⟩
induction n with
| zero => rfl
| succ n ih => exact ⟨f, ih, fun x ↦ isEmptyElim x⟩Derivative values, restriction and local jets
Let \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). The relation \(D_U^0f=g\) is equivalent to \(f=g\). The relation \(D_U^{n+1}f=g\) is equivalent to the existence of \(h\) with \(D_U^nf=h\) and \(h'(x)=g(x)\) at every point of \(U\). Whenever such a derivative chain exists, its final function is unique.
Lean Formalisation
theorem hasIteratedDerivOnOpen_zero.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜)
(f g : ↥U → 𝕜) : HasIteratedDerivOnOpen U 0 f g ↔ f = gLean proof
/-- Order zero is equality of functions. -/
theorem hasIteratedDerivOnOpen_zero (U : TopologicalSpace.Opens 𝕜) (f g : U → 𝕜) :
HasIteratedDerivOnOpen U 0 f g ↔ f = g := Iff.rflLet \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). For \(f\in \mathcal D^n(U)\), the function \(D_U^nf\) belongs to an actual order-\(n\) derivative chain starting at \(f\). A function \(g:U\to \mathbb K\) equals \(D_U^nf\) if and only if it is the final function of such a chain. In particular, \(D_U^0f=f\).
Lean Formalisation
theorem iteratedDerivOnOpen_spec.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : TopologicalSpace.Opens 𝕜} {n : ℕ}
(f : IteratedDerivInput U n) : HasIteratedDerivOnOpen U n (↑f) (iteratedDerivOnOpen f)Lean proof
/-- The classical value belongs to an actual derivative chain. -/
theorem iteratedDerivOnOpen_spec {U : TopologicalSpace.Opens 𝕜} {n : ℕ}
(f : IteratedDerivInput U n) :
HasIteratedDerivOnOpen U n f.val (iteratedDerivOnOpen f) := f.property.choose_specLet \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). For every extension \(F\) agreeing with \(f\) on \(U\), analyticity of \(f\) on its open domain is equivalent to analyticity of \(F\) at every point of \(U\). Thus the condition is independent of the extension away from \(U\).
Lean Formalisation
theorem analyticOnOpen_iff.{u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜) (f : ↥U → 𝕜)
(g : 𝕜 → 𝕜) (hg : ∀ (y : ↥U), g ↑y = f y) : AnalyticOnOpen U f ↔ AnalyticOnNhd 𝕜 g ↑ULean proof
/-- Analyticity does not depend on how values are assigned outside the open domain. -/
theorem analyticOnOpen_iff (U : TopologicalSpace.Opens 𝕜) (f : U → 𝕜)
(g : 𝕜 → 𝕜) (hg : ∀ y : U, g y = f y) :
AnalyticOnOpen U f ↔ AnalyticOnNhd 𝕜 g U := by
constructor
· intro h x hx
obtain ⟨F, hF, hA⟩ := h ⟨x, hx⟩
apply hA.congr
filter_upwards [U.isOpen.mem_nhds hx] with y hy
exact (hF ⟨y, hy⟩).trans (hg ⟨y, hy⟩).symm
· intro h x
exact ⟨g, hg, h x x.property⟩Let \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). Derivative chains restrict to smaller open domains. An order-\(n\) chain restricts to an order-\(k\) chain for every \(k\le n\), without changing its initial function.
Lean Formalisation
theorem HasDerivAtOnOpen.restrict.{u_2} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {U V : TopologicalSpace.Opens 𝕜}
(hVU : V ≤ U) {f : ↥U → 𝕜} {d : 𝕜} (x : ↥V) (h : HasDerivAtOnOpen U f d ⟨↑x, ⋯⟩) :
HasDerivAtOnOpen V (fun y => f ⟨↑y, ⋯⟩) d xLean proof
theorem HasDerivAtOnOpen.restrict {U V : TopologicalSpace.Opens 𝕜}
(hVU : V ≤ U) {f : U → 𝕜} {d : 𝕜} (x : V)
(h : HasDerivAtOnOpen U f d ⟨x.val, hVU x.property⟩) :
HasDerivAtOnOpen V (fun y ↦ f ⟨y.val, hVU y.property⟩) d x := by
obtain ⟨F, hF, hd⟩ := h
exact ⟨F, fun y ↦ hF ⟨y.val, hVU y.property⟩, hd⟩Let \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). Let \(f:U\to \mathbb K\), with \(U\) open, and \(x\in U\). Its order-zero derivative at \(x\) is \(f(x)\). For \(n=k+1\), say that its order-\(n\) derivative at \(x\) is \(d\) if some open neighbourhood \(V\subseteq U\) of \(x\) carries an order-\(k\) derivative chain of \(f|_V\), whose final function has derivative \(d\) at \(x\). The highest derivative is required only at \(x\).
Lean Formalisation
def HasIteratedDerivAtOnOpen.{u_2} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜) (n : ℕ)
(f : ↥U → 𝕜) (d : 𝕜) (x : ↥U) : PropLean definition
/-- An order-n derivative exists at the specified point, with lower derivatives
existing on a neighbourhood. The highest derivative need only exist at the point. -/
def HasIteratedDerivAtOnOpen (U : TopologicalSpace.Opens 𝕜)
(n : ℕ) (f : U → 𝕜) (d : 𝕜) (x : U) : Prop :=
match n with
| 0 => d = f x
| k + 1 => ∃ (V : TopologicalSpace.Opens 𝕜) (hx : x.val ∈ V) (hVU : V ≤ U)
(g : V → 𝕜),
HasIteratedDerivOnOpen V k (fun y ↦ f ⟨y.val, hVU y.property⟩) g ∧
HasDerivAtOnOpen V g d ⟨x.val, hx⟩Let \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). The pointwise iterated derivative, when it exists, is unique. An order-\(n\) derivative chain on \(U\) gives that pointwise derivative at every \(x\in U\).
Lean Formalisation
theorem HasIteratedDerivAtOnOpen.unique.{u_2} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {U : TopologicalSpace.Opens 𝕜} {n : ℕ}
{f : ↥U → 𝕜} {d e : 𝕜} {x : ↥U} (hd : HasIteratedDerivAtOnOpen U n f d x) (he : HasIteratedDerivAtOnOpen U n f e x) :
d = eLean proof
theorem HasIteratedDerivAtOnOpen.unique {U : TopologicalSpace.Opens 𝕜}
{n : ℕ} {f : U → 𝕜} {d e : 𝕜} {x : U}
(hd : HasIteratedDerivAtOnOpen U n f d x)
(he : HasIteratedDerivAtOnOpen U n f e x) : d = e := by
cases n with
| zero => exact hd.trans he.symm
| succ n =>
obtain ⟨V, hxV, hVU, g, hg, hd⟩ := hd
obtain ⟨W, hxW, hWU, h, hh, he⟩ := he
let Z := V ⊓ W
have hZV : Z ≤ V := inf_le_left
have hZW : Z ≤ W := inf_le_right
have hgv := hg.restrict hZV
have hhw := hh.restrict hZW
have heq : (fun y : Z ↦ g ⟨y.val, hZV y.property⟩) =
(fun y : Z ↦ h ⟨y.val, hZW y.property⟩) := hgv.unique hhw
let y : Z := ⟨x.val, hxV, hxW⟩
have hd' := hd.restrict hZV y
have he' := he.restrict hZW y
rw [heq] at hd'
exact hd'.unique he'Let \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). For \(f:U\to \mathbb K\) and \(m\ge 0\), a jet point is \(x\in U\) at which every derivative of order \(0,\ldots ,m\) exists in the preceding pointwise sense. At such a point define \(J_kf(x)\) to be its unique order-\(k\) derivative value.
Lean Formalisation
def DerivativeJetPoint.{u_2} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] (U : TopologicalSpace.Opens 𝕜) (m : ℕ)
(f : ↥U → 𝕜) : Type u_2Lean definition
/-- The evaluation point certifies every derivative used by a finite differential expression. -/
abbrev DerivativeJetPoint (U : TopologicalSpace.Opens 𝕜) (m : ℕ) (f : U → 𝕜) :=
{x : U // ∀ k : Fin (m + 1), ∃ d, HasIteratedDerivAtOnOpen U k.val f d x}Let \(\mathbb K\) be a nontrivially normed field (for example \(\mathbb R\) or \(\mathbb C\)). For each jet point and \(0\le k\le m\), \(J_kf(x)=d\) if and only if the order-\(k\) derivative exists at \(x\) with value \(d\). If \(f\) admits an order-\(m\) derivative chain on \(U\), every \(x\in U\) is a jet point of order \(m\), and its truncated chain values agree with these jet values.
Lean Formalisation
theorem derivativeJet_spec.{u_2} {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {U : TopologicalSpace.Opens 𝕜} {m : ℕ} {f : ↥U → 𝕜}
(x : DerivativeJetPoint U m f) (k : Fin (m + 1)) : HasIteratedDerivAtOnOpen U (↑k) f (derivativeJet x k) ↑xLean proof
theorem derivativeJet_spec {U : TopologicalSpace.Opens 𝕜} {m : ℕ} {f : U → 𝕜}
(x : DerivativeJetPoint U m f) (k : Fin (m + 1)) :
HasIteratedDerivAtOnOpen U k.val f (derivativeJet x k) x.val :=
(x.property k).choose_spec1.1.3 Circle integrals
The contour formulas in Chapter 2.5 use the following parametrized circle integral.
For \(c\in \mathbb C\) and \(r\in \mathbb R\), let \(S=\{ z:|z-c|=|r|\} \) and \(\gamma (\theta )=c+r e^{i\theta }\). Let \(\mathcal C_{c,r}\) consist of functions \(f:S\to \mathbb C\) for which \(\theta \mapsto i r e^{i\theta }f(\gamma (\theta ))\) is integrable on \([0,2\pi ]\). For \(f\in \mathcal C_{c,r}\), define
Addition in \(\mathcal C_{c,r}\) is pointwise addition of functions. Reference: [ATAP, proof of Theorem 8.1].
Lean Formalisation
def Complex.CircleIntegralInput (c : ℂ) (r : ℝ) : TypeLean definition
/-- A function on the actual contour, with integrability of its parametrized
line integrand. The radius may be zero (a constant curve) or signed.
Reference: ATAP, proof of Theorem 8.1. -/
abbrev CircleIntegralInput (c : ℂ) (r : ℝ) :=
{f : sphere c |r| → ℂ // IntervalIntegrable
(fun θ : ℝ => (circleMap 0 r θ * I) *
f ⟨circleMap c r θ, circleMap_mem_sphere' c r θ⟩) volume 0 (2 * π)}If \(f\in \mathcal C_{c,r}\) and \(|f(z)|\le M\) for every \(z\in S\), then
Reference: [ATAP, proof of Theorem 8.1].
Lean Formalisation
theorem Complex.norm_circleIntegralOn_le {c : ℂ} {r M : ℝ} (f : c.CircleIntegralInput r)
(hf : ∀ (z : ↑(Metric.sphere c |r|)), ‖↑f z‖ ≤ M) : ‖Complex.circleIntegralOn f‖ ≤ 2 * Real.pi * |r| * MLean proof
/-- The classical length-times-bound estimate (ATAP, proof of Theorem 8.1). -/
theorem norm_circleIntegralOn_le {c : ℂ} {r M : ℝ}
(f : CircleIntegralInput c r) (hf : ∀ z, ‖f.val z‖ ≤ M) :
‖circleIntegralOn f‖ ≤ 2 * π * |r| * M := by
calc
‖circleIntegralOn f‖ ≤ |r| * M * |2 * π - 0| := by
apply intervalIntegral.norm_integral_le_of_norm_le_const
intro θ _
calc
‖(circleMap 0 r θ * I) * f.val ⟨_, circleMap_mem_sphere' c r θ⟩‖ =
|r| * ‖f.val ⟨_, circleMap_mem_sphere' c r θ⟩‖ := by
simp only [norm_mul, norm_I, norm_circleMap_zero, mul_one]
_ ≤ |r| * M := mul_le_mul_of_nonneg_left (hf _) (abs_nonneg _)
_ = 2 * π * |r| * M := by
rw [sub_zero, abs_of_pos Real.two_pi_pos]
ringParametrization and linearity
For \(f\in \mathcal C_{c,r}\), the function \(\theta \mapsto i r e^{i\theta }f(c+r e^{i\theta })\) is integrable on \([0,2\pi ]\), and its integral equals \(\mathcal I_{c,r}(f)\). Every continuous \(f:S\to \mathbb C\) belongs to \(\mathcal C_{c,r}\), with its values on \(S\) unchanged. For \(r=0\) the curve is constant and \(\mathcal I_{c,0}(f)=0\). For \(f,g\in \mathcal C_{c,r}\),
Lean Formalisation
theorem Complex.circleIntegralOn_spec {c : ℂ} {r : ℝ} (f : c.CircleIntegralInput r) :
IntervalIntegrable (fun θ => circleMap 0 r θ * Complex.I * ↑f ⟨circleMap c r θ, ⋯⟩) MeasureTheory.volume 0
(2 * Real.pi) ∧
Complex.circleIntegralOn f = ∫ (θ : ℝ) in 0..2 * Real.pi, circleMap 0 r θ * Complex.I * ↑f ⟨circleMap c r θ, ⋯⟩Lean proof
theorem circleIntegralOn_spec {c : ℂ} {r : ℝ} (f : CircleIntegralInput c r) :
IntervalIntegrable (fun θ : ℝ => (circleMap 0 r θ * I) *
f.val ⟨circleMap c r θ, circleMap_mem_sphere' c r θ⟩) volume 0 (2 * π) ∧
circleIntegralOn f = ∫ θ in 0..2 * π, (circleMap 0 r θ * I) *
f.val ⟨circleMap c r θ, circleMap_mem_sphere' c r θ⟩ :=
⟨f.property, rfl⟩