ReleaseCycleDSlope.lean

1 import KomorebiVerification.PaperII.ReleaseCycleParameter
2 /-
3 Copyright (c) 2026. All rights reserved.
4 Released under Apache 2.0 license as described in the file LICENSE.
5 Authors: Chris Birkbeck
6 -/
7 
8 /-
9 Modified for Operation Komorebi Paper II on 2026-10-19.
10 The upstream scalar divided-difference estimates are generalized here to
11 arbitrary complete complex normed spaces. New cycle-integral holomorphy,
12 symmetry and repeated-divided-difference results are added. The upstream
13 source and exact revision are recorded in PROVENANCE.md.
14 -/
15 
16 import Mathlib.Analysis.Calculus.DSlope
17 import Mathlib.Analysis.Calculus.Deriv.Shift
18 import Mathlib.Analysis.Complex.Convex
19 import Mathlib.Analysis.Complex.Liouville
20 import Mathlib.Analysis.Complex.RemovableSingularity
21 import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
22 import Mathlib.Analysis.SpecificLimits.RCLike
23 import Mathlib.MeasureTheory.Integral.DominatedConvergence
24 
25 /-!
26 # `dslope` as a parameter integral
27 
28 For `f : ℂ → ℂ` differentiable on an open convex set `U` and `c, w ∈ U`, we have
29 the integral representation:
30 
31   `dslope f c w = ∫₀¹ deriv f (c + t • (w - c)) ∂t`
32 
33 This is the fundamental theorem of calculus applied to `f` on the segment `[c, w] ⊆ U`.
34 The representation unifies the two cases in `dslope` (`c = w` giving `deriv f c`, and
35 `c ≠ w` giving the usual slope formula).
36 
37 From this integral representation we deduce:
38 
39 * Joint continuity of `(c, w) ↦ dslope f c w` on convex open sets
40 
41 ## Main results
42 
43 * `dslope_eq_integral_deriv` — `dslope f c w = ∫₀¹ deriv f (c + t•(w-c))` on convex `U`
44 -/
45 
46 
47 
48 open Set MeasureTheory Filter Topology intervalIntegral
49 
50 noncomputable section
51 
52 namespace Komorebi.PaperII.ReleaseCycleDSlope
53 
54 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
55   [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
56 variable {f : ℂ → E}
57 
58 set_option backward.isDefEq.respectTransparency false in
59 /-- The `dslope` integral representation on a convex open set: when `f` is
60 differentiable on `U` and both `c, w ∈ U` (so the segment `[c, w] ⊆ U`), then
61 `dslope f c w` equals the integral of the derivative of `f` along the segment. -/
62 theorem dslope_eq_integral_deriv {U : Set ℂ} (hU : Convex ℝ U) (hU_open : IsOpen U)
63     (hf : DifferentiableOn ℂ f U) {c w : ℂ} (hc : c ∈ U) (hw : w ∈ U) :
64     dslope f c w = ∫ t in (0 : ℝ)..1, deriv f (c + t • (w - c)) := by
65   have h_seg : ∀ t ∈ Icc (0 : ℝ) 1, c + t • (w - c) ∈ U := fun t ht ↦ by
66     rw [show c + t • (w - c) = (1 - t) • c + t • w by module]
67     exact hU hc hw (by linarith [ht.2]) ht.1 (by linarith)
68   have h_deriv : ∀ t ∈ Icc (0 : ℝ) 1,
69       HasDerivAt f (deriv f (c + t • (w - c))) (c + t • (w - c)) := fun t ht ↦
70     ((hf (c + t • (w - c)) (h_seg t ht)).differentiableAt
71       (hU_open.mem_nhds (h_seg t ht))).hasDerivAt
72   have h_deriv_contU : ContinuousOn (deriv f) U :=
73     (hf.analyticOnNhd hU_open).deriv.continuousOn
74   have h_cont : ContinuousOn (fun t : ℝ ↦ deriv f (c + t • (w - c))) (Icc (0 : ℝ) 1) :=
75     h_deriv_contU.comp (by continuity : Continuous _).continuousOn h_seg
76   have h_int := integral_unitInterval_deriv_eq_sub h_cont h_deriv
77   rw [show c + (w - c) = w by ring] at h_int
78   by_cases hwc : w = c
79   · subst hwc; simp
80   · have hne : w - c ≠ 0 := sub_ne_zero.mpr hwc
81     rw [dslope_of_ne f hwc, slope_def_module, ← h_int, inv_smul_smul₀ hne]
82 
83 set_option backward.isDefEq.respectTransparency false in
84 private lemma exists_compact_tube_prod {U : Set ℂ} (hU : Convex ℝ U) (hU_open : IsOpen U)
85     {c₀ w₀ : ℂ} (hc₀ : c₀ ∈ U) (hw₀ : w₀ ∈ U) :
86     ∃ ε > 0, ∃ K ⊆ U, IsCompact K ∧
87       ∀ c ∈ Metric.ball c₀ ε, ∀ w ∈ Metric.ball w₀ ε,
88         ∀ t ∈ Icc (0 : ℝ) 1, c + t • (w - c) ∈ K := by
89   obtain ⟨ρ_c, hρ_c_pos, hρ_c_sub⟩ := Metric.isOpen_iff.mp hU_open c₀ hc₀
90   obtain ⟨ρ_w, hρ_w_pos, hρ_w_sub⟩ := Metric.isOpen_iff.mp hU_open w₀ hw₀
91   set ρ := min ρ_c ρ_w / 2
92   have hρ_pos : 0 < ρ := by positivity
93   refine ⟨ρ, hρ_pos,
94     (fun p : ℂ × ℂ × ℝ ↦ (1 - p.2.2) • p.1 + p.2.2 • p.2.1) ''
95       (Metric.closedBall c₀ ρ ×ˢ Metric.closedBall w₀ ρ ×ˢ Icc (0 : ℝ) 1),
96     ?_, ?_, ?_⟩
97   · rintro z ⟨⟨c, w, t⟩, ⟨hc, hw, ht⟩, rfl⟩
98     rw [Metric.mem_closedBall] at hc hw
99     simp only [ρ] at hc hw
100     exact hU
101       (hρ_c_sub (Metric.mem_ball.mpr (by linarith [min_le_left ρ_c ρ_w])))
102       (hρ_w_sub (Metric.mem_ball.mpr (by linarith [min_le_right ρ_c ρ_w])))
103       (by linarith [ht.2]) ht.1 (by linarith)
104   · exact IsCompact.image_of_continuousOn ((isCompact_closedBall _ _).prod
105       ((isCompact_closedBall _ _).prod isCompact_Icc))
106       (((continuous_const.sub continuous_snd.snd).smul continuous_fst).add
107         (continuous_snd.snd.smul continuous_snd.fst)).continuousOn
108   · intro c hc w hw t ht
109     rw [Metric.mem_ball] at hc hw
110     refine ⟨(c, w, t), ⟨?_, ?_, ht⟩, ?_⟩
111     · rw [Metric.mem_closedBall]; linarith
112     · rw [Metric.mem_closedBall]; linarith
113     · change (1 - t) • c + t • w = c + t • (w - c)
114       module
115 /-- Joint continuity of `(c, w) ↦ dslope f c w` on `U × U` for `f` differentiable
116 on open convex `U`. -/
117 theorem continuousOn_dslope_prod {U : Set ℂ} (hU : Convex ℝ U) (hU_open : IsOpen U)
118     (hf : DifferentiableOn ℂ f U) :
119     ContinuousOn (fun p : ℂ × ℂ ↦ dslope f p.1 p.2) (U ×ˢ U) := by
120   rintro ⟨c₀, w₀⟩ ⟨hc₀, hw₀⟩
121   obtain ⟨ε, hε_pos, K, hK_sub, hK_compact, hK_tube⟩ :=
122     exists_compact_tube_prod hU hU_open hc₀ hw₀
123   have h_deriv_contU : ContinuousOn (deriv f) U :=
124     (hf.analyticOnNhd hU_open).deriv.continuousOn
125   obtain ⟨M, hM⟩ := hK_compact.bddAbove_image (h_deriv_contU.norm.mono hK_sub)
126   have h_eq_nbhd : (fun p : ℂ × ℂ ↦ dslope f p.1 p.2) =ᶠ[nhds (c₀, w₀)]
127       fun p ↦ ∫ t in (0 : ℝ)..1, deriv f (p.1 + t • (p.2 - p.1)) := by
128     filter_upwards [(hU_open.prod hU_open).mem_nhds
129       (⟨hc₀, hw₀⟩ : (c₀, w₀) ∈ U ×ˢ U)] with p hp
130     exact dslope_eq_integral_deriv hU hU_open hf hp.1 hp.2
131   have hp_proj : ∀ p : ℂ × ℂ, p ∈ Metric.ball (c₀, w₀) ε →
132       p.1 ∈ Metric.ball c₀ ε ∧ p.2 ∈ Metric.ball w₀ ε := fun p hp ↦ by
133     rw [Metric.mem_ball, Prod.dist_eq] at hp
134     exact ⟨Metric.mem_ball.mpr (lt_of_le_of_lt (le_max_left _ _) hp),
135       Metric.mem_ball.mpr (lt_of_le_of_lt (le_max_right _ _) hp)⟩
136   refine (ContinuousAt.congr ?_ h_eq_nbhd.symm).continuousWithinAt
137   refine continuousAt_of_dominated_interval
138     (bound := fun _ ↦ max M 0) ?_ ?_ intervalIntegrable_const ?_
139   · filter_upwards [Metric.ball_mem_nhds (c₀, w₀) hε_pos] with p hp
140     rw [uIoc_of_le (zero_le_one' ℝ)]
141     obtain ⟨hp_c, hp_w⟩ := hp_proj p hp
142     have h_cont : ContinuousOn (fun t : ℝ ↦ deriv f (p.1 + t • (p.2 - p.1)))
143         (Icc (0 : ℝ) 1) :=
144       h_deriv_contU.comp (by continuity : Continuous _).continuousOn
145         fun t ht ↦ hK_sub (hK_tube p.1 hp_c p.2 hp_w t ht)
146     exact (h_cont.mono Ioc_subset_Icc_self).aestronglyMeasurable measurableSet_Ioc
147   · filter_upwards [Metric.ball_mem_nhds (c₀, w₀) hε_pos] with p hp
148     filter_upwards with t ht
149     rw [uIoc_of_le zero_le_one] at ht
150     obtain ⟨hp_c, hp_w⟩ := hp_proj p hp
151     exact le_max_of_le_left (hM ⟨p.1 + t • (p.2 - p.1),
152       hK_tube p.1 hp_c p.2 hp_w t (Ioc_subset_Icc_self ht), rfl⟩)
153   · filter_upwards with t ht
154     rw [uIoc_of_le zero_le_one] at ht
155     have hmem : c₀ + t • (w₀ - c₀) ∈ U :=
156       hK_sub (hK_tube c₀ (Metric.mem_ball_self hε_pos) w₀
157         (Metric.mem_ball_self hε_pos) t (Ioc_subset_Icc_self ht))
158     exact (h_deriv_contU.continuousAt (hU_open.mem_nhds hmem)).comp_of_eq
159       (by continuity : Continuous _).continuousAt rfl
160 
161 /-- **Joint continuity of `dslope` on any open set** (without convexity).
162 
163 The convex `continuousOn_dslope_prod` proof uses `dslope_eq_integral_deriv` which
164 requires the segment `[c, w]` to lie in `U`. For non-convex `U`, the segment may
165 exit `U`, so this proof splits cases:
166 
167 * Off-diagonal `c₀ ≠ w₀`: `dslope f c w = (f w − f c)/(w − c)` for `w ≠ c`, and
168   this equality holds eventually near `(c₀, w₀)` (since `w₀ − c₀ ≠ 0`).
169   Continuity of `f` on `U` then gives joint continuity of the quotient.
170 * Diagonal `c₀ = w₀`: any open ball around `c₀` inside `U` is convex, so the
171   convex theorem `continuousOn_dslope_prod` applies on the ball, giving
172   `ContinuousAt` at `(c₀, c₀)`. -/
173 theorem continuousOn_dslope_prod_open {U : Set ℂ} (hU_open : IsOpen U)
174     (hf : DifferentiableOn ℂ f U) :
175     ContinuousOn (fun p : ℂ × ℂ ↦ dslope f p.1 p.2) (U ×ˢ U) := by
176   rintro ⟨c₀, w₀⟩ ⟨hc₀, hw₀⟩
177   by_cases h_eq : c₀ = w₀
178   · subst h_eq
179     obtain ⟨ρ, hρ_pos, hρ_sub⟩ := Metric.isOpen_iff.mp hU_open c₀ hc₀
180     exact ((continuousOn_dslope_prod (convex_ball c₀ ρ) Metric.isOpen_ball
181       (hf.mono hρ_sub)).continuousAt ((Metric.isOpen_ball.prod
182         Metric.isOpen_ball).mem_nhds ⟨Metric.mem_ball_self hρ_pos,
183           Metric.mem_ball_self hρ_pos⟩)).continuousWithinAt
184   · have hf_diff_at : ∀ z ∈ U, DifferentiableAt ℂ f z := fun z hz ↦
185       (hf z hz).differentiableAt (hU_open.mem_nhds hz)
186     have h_sub_ne : (fun p : ℂ × ℂ ↦ p.2 - p.1) (c₀, w₀) ≠ 0 :=
187       sub_ne_zero.mpr (Ne.symm h_eq)
188     have h_eventually_ne : ∀ᶠ p : ℂ × ℂ in nhds (c₀, w₀), p.2 ≠ p.1 := by
189       filter_upwards [(by continuity : Continuous fun p : ℂ × ℂ ↦
190         p.2 - p.1).continuousAt.tendsto.eventually_ne h_sub_ne] with p hp using
191         sub_ne_zero.mp hp
192     have h_eq_nbhd : (fun p : ℂ × ℂ ↦ dslope f p.1 p.2) =ᶠ[nhds (c₀, w₀)]
193         fun p ↦ (p.2 - p.1)⁻¹ • (f p.2 - f p.1) := by
194       filter_upwards [h_eventually_ne] with p hp
195       rw [dslope_of_ne f hp, slope_def_module]
196     have h_quot_cont : ContinuousAt
197         (fun p : ℂ × ℂ ↦ (p.2 - p.1)⁻¹ • (f p.2 - f p.1)) (c₀, w₀) :=
198       ((continuousAt_snd.sub continuousAt_fst).inv₀ h_sub_ne).smul
199         (((hf_diff_at w₀ hw₀).continuousAt.comp continuousAt_snd).sub
200           ((hf_diff_at c₀ hc₀).continuousAt.comp continuousAt_fst))
201     exact (h_quot_cont.congr h_eq_nbhd.symm).continuousWithinAt
202 
203 /-- **Continuity of `c ↦ dslope f c w₀` on any open set `U`** (no convexity).
204 Follows from `continuousOn_dslope_prod_open` by partial application. -/
205 theorem continuousOn_dslope_first_arg_open {U : Set ℂ} (hU_open : IsOpen U)
206     (hf : DifferentiableOn ℂ f U) {w₀ : ℂ} (hw₀ : w₀ ∈ U) :
207     ContinuousOn (fun c ↦ dslope f c w₀) U := by
208   rw [show (fun c : ℂ ↦ dslope f c w₀) =
209     (fun p : ℂ × ℂ ↦ dslope f p.1 p.2) ∘ (fun c : ℂ ↦ (c, w₀)) from rfl]
210   exact (continuousOn_dslope_prod_open hU_open hf).comp
211     (continuous_id.prodMk continuous_const).continuousOn fun c hc ↦ ⟨hc, hw₀⟩
212 
213 /-- **Uniform bound on `deriv (dslope f c) w`** for `c` in a compact subset of an
214 open set `U` and `w` in a ball around `w₀ ∈ U`. Cauchy's estimate applied to
215 `dslope f c` (analytic on `U` by `Complex.differentiableOn_dslope`). The bound is
216 `2M/ρ` where `M = sup_{(c, z) ∈ K_c × closedBall w₀ (3ρ/2)} ‖dslope f c z‖`
217 (finite by joint continuity on a compact set). -/
218 theorem deriv_dslope_bounded_on_compact_open {U : Set ℂ} (hU_open : IsOpen U)
219     (hf : DifferentiableOn ℂ f U) {K_c : Set ℂ} (hK_compact : IsCompact K_c)
220     (hK_sub : K_c ⊆ U) {w₀ : ℂ} (hw₀ : w₀ ∈ U) :
221     ∃ C > 0, ∃ δ > 0, ∀ c ∈ K_c, ∀ w ∈ Metric.ball w₀ δ,
222       ‖deriv (dslope f c) w‖ ≤ C := by
223   obtain ⟨ρ_w, hρ_w_pos, hρ_w_sub⟩ := Metric.isOpen_iff.mp hU_open w₀ hw₀
224   set ρ := ρ_w / 4
225   have hρ_pos : 0 < ρ := by positivity
226   have h_cB_w_sub : Metric.closedBall w₀ (3 * ρ / 2) ⊆ U := fun z hz ↦
227     hρ_w_sub <| Metric.mem_ball.mpr <| by
228       rw [Metric.mem_closedBall] at hz; simp only [ρ] at hz ⊢; linarith
229   have hK_sub_prod : K_c ×ˢ Metric.closedBall w₀ (3 * ρ / 2) ⊆ U ×ˢ U :=
230     fun ⟨c, z⟩ ⟨hc, hz⟩ ↦ ⟨hK_sub hc, h_cB_w_sub hz⟩
231   have hKprod_compact : IsCompact (K_c ×ˢ Metric.closedBall w₀ (3 * ρ / 2)) :=
232     hK_compact.prod (isCompact_closedBall _ _)
233   obtain ⟨M, hM⟩ :=
234     hKprod_compact.bddAbove_image ((continuousOn_dslope_prod_open hU_open hf).mono hK_sub_prod).norm
235   refine ⟨max M 0 / (ρ / 2) + 1, by positivity, ρ / 2, by positivity, ?_⟩
236   intro c hc w hw
237   rw [Metric.mem_ball] at hw
238   have h_ds_diff_U : DifferentiableOn ℂ (dslope f c) U :=
239     (Complex.differentiableOn_dslope (hU_open.mem_nhds (hK_sub hc))).mpr hf
240   have h_cB_w_w0 :
241       Metric.closedBall w (ρ / 2) ⊆ Metric.closedBall w₀ (3 * ρ / 2) := fun z hz ↦ by
242     rw [Metric.mem_closedBall] at hz ⊢
243     linarith [dist_triangle z w w₀]
244   have h_DC : DiffContOnCl ℂ (dslope f c) (Metric.ball w (ρ / 2)) :=
245     ⟨h_ds_diff_U.mono fun z hz ↦
246       h_cB_w_sub (h_cB_w_w0 (Metric.ball_subset_closedBall hz)),
247      (h_ds_diff_U.mono fun z hz ↦
248        h_cB_w_sub (h_cB_w_w0 (Metric.closure_ball_subset_closedBall hz))).continuousOn⟩
249   have h_sphere_bound : ∀ z ∈ Metric.sphere w (ρ / 2),
250       ‖dslope f c z‖ ≤ max M 0 := fun z hz ↦
251     le_max_of_le_left
252       (hM ⟨(c, z), ⟨hc, h_cB_w_w0 (Metric.sphere_subset_closedBall hz)⟩, rfl⟩)
253   linarith [Complex.norm_deriv_le_of_forall_mem_sphere_norm_le (by positivity : (0:ℝ) < ρ / 2)
254     h_DC h_sphere_bound]
255 
256 omit [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
257 /-- Divided differences are symmetric, including the diagonal. -/
258 theorem dslope_comm (g : ℂ → E) (a b : ℂ) : dslope g a b = dslope g b a := by
259   by_cases h : b = a
260   · subst b; rfl
261   · rw [dslope_of_ne g h, dslope_of_ne g (Ne.symm h), slope_comm]
262 
263 omit [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
264 /-- The derivative in one node equals the repeated divided difference at that node.
265 This identity supplies continuous dependence of the derivative on the other node. -/
266 theorem deriv_dslope_eq_repeated {g : ℂ → E} {c w : ℂ}
267     (hg : DifferentiableAt ℂ g w) (hd : DifferentiableAt ℂ (dslope g c) w) :
268     deriv (dslope g c) w = dslope (dslope g w) w c := by
269   by_cases hcw : c = w
270   · subst c; simp
271   have hdiff := (((hasDerivAt_id w).sub_const c).smul hd.hasDerivAt)
272   have hdiff' : HasDerivAt (fun z => g z - g c)
273       ((1 : ℂ) • dslope g c w + (w - c) • deriv (dslope g c) w) w :=
274     (hdiff.congr_of_eventuallyEq (Eventually.of_forall fun z => (sub_smul_dslope g c z).symm)).congr_deriv (by simp only [id_eq, add_comm])
275   have hrel := hdiff'.unique (hg.hasDerivAt.sub_const (g c))
276   simp only [one_smul] at hrel
277   have hrep := sub_smul_dslope (dslope g w) w c
278   rw [dslope_same, dslope_comm g w c] at hrep
279   apply (smul_right_injective E (sub_ne_zero.mpr (Ne.symm hcw)))
280   have hneg : (w - c) • dslope (dslope g w) w c =
281       deriv g w - dslope g c w := by
282     calc
283       (w - c) • dslope (dslope g w) w c =
284           -((c - w) • dslope (dslope g w) w c) := by rw [← neg_smul]; congr 1; ring
285       _ = deriv g w - dslope g c w := by rw [hrep]; abel
286   dsimp only
287   rw [hneg]
288   exact eq_sub_of_add_eq' hrel
289 
290 open Komorebi.PaperII.ReleaseAnalyticContour
291 open Komorebi.PaperII.ReleaseCycleParameter
292 
293 /-- Holomorphy of the actual Banach-valued divided-difference cycle integral.
294 Only the defining integrable velocities of `IntegralCycle` are used. -/
295 theorem differentiableOn_lineIntegral_dslope (Γ : IntegralCycle)
296     {U : Set ℂ} (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
297     (htrace : Γ.trace ⊆ U) :
298     DifferentiableOn ℂ (fun w => Γ.lineIntegral (dslope f w)) U := by
299   intro w hw
300   obtain ⟨M, hM, δ, hδ, hbound⟩ :=
301     deriv_dslope_bounded_on_compact_open hU hf (isCompact_trace Γ) htrace hw
302   have hwU := hU.mem_nhds hw
303   have hs : Metric.ball w δ ∩ U ∈ 𝓝 w := inter_mem (Metric.ball_mem_nhds w hδ) hwU
304   have hds : ∀ a ∈ U, DifferentiableOn ℂ (dslope f a) U := fun a ha =>
305     (Complex.differentiableOn_dslope (hU.mem_nhds ha)).mpr hf
306   have hderiv : ∀ a ∈ U, ∀ z ∈ U,
307       HasDerivAt (fun b => dslope f b z) (dslope (dslope f a) a z) a := by
308     intro a ha z hz
309     have hd : DifferentiableAt ℂ (dslope f z) a :=
310       (hds z hz a ha).differentiableAt (hU.mem_nhds ha)
311     rw [← deriv_dslope_eq_repeated ((hf a ha).differentiableAt (hU.mem_nhds ha)) hd]
312     exact hd.hasDerivAt.congr_of_eventuallyEq
313       (Eventually.of_forall fun b => dslope_comm f b z)
314   apply DifferentiableAt.differentiableWithinAt
315   exact (hasDerivAt_lineIntegral Γ (f' := fun a z => dslope (dslope f a) a z) hs
316     (fun a ha => (hds a ha.2).continuousOn.mono htrace)
317     (((Complex.differentiableOn_dslope hwU).mpr (hds w hw)).continuousOn.mono htrace)
318     (fun a ha z hz => hderiv a ha.2 z (htrace hz)) M
319     (fun a ha z hz => by
320       rw [← deriv_dslope_eq_repeated
321         ((hf a ha.2).differentiableAt (hU.mem_nhds ha.2))
322         ((hds z (htrace hz) a ha.2).differentiableAt (hU.mem_nhds ha.2))]
323       exact hbound z hz a ha.1)).differentiableAt
324 
325 end Komorebi.PaperII.ReleaseCycleDSlope
326 

Back to source controls