ReleaseCycleParameter.lean

1 import KomorebiVerification.PaperII.ReleaseAnalyticContour
2 import Mathlib.Analysis.Calculus.ParametricIntervalIntegral
3 import Mathlib.Analysis.Calculus.MeanValue
4 
5 set_option autoImplicit false
6 noncomputable section
7 
8 namespace Komorebi.PaperII.ReleaseCycleParameter
9 open MeasureTheory Set Filter
10 open scoped Topology BigOperators
11 open Komorebi.PaperII.ReleaseAnalyticContour
12 
13 theorem isCompact_trace (Γ : IntegralCycle) : IsCompact Γ.trace := by
14   have heq : Γ.trace = ⋃ i : Fin Γ.count, Γ.curve i '' uIcc (0 : ℝ) 1 := by
15     ext z
16     simp only [IntegralCycle.trace, mem_ofPred_eq, mem_iUnion, mem_image]
17   rw [heq]
18   exact isCompact_iUnion fun i => isCompact_uIcc.image_of_continuousOn (Γ.continuousOn_curve i)
19 
20 theorem exists_ball_away_trace (Γ : IntegralCycle) {w : ℂ} (hw : w ∉ Γ.trace) :
21     ∃ ε > 0, ∀ z ∈ Γ.trace, ∀ w' ∈ Metric.ball w ε,
22       ε ≤ ‖z - w'‖ := by
23   obtain ⟨r, hr, hball⟩ := Metric.isOpen_iff.mp (isCompact_trace Γ).isClosed.isOpen_compl w hw
24   refine ⟨r / 2, half_pos hr, ?_⟩
25   intro z hz w' hw'
26   have hzout : r ≤ ‖z - w‖ := by
27     by_contra! hlt
28     exact hball (by simpa only [Metric.mem_ball, dist_eq_norm] using hlt) hz
29   have hw'lt : ‖w' - w‖ < r / 2 := by simpa only [Metric.mem_ball, dist_eq_norm] using hw'
30   have htri : ‖z - w‖ ≤ ‖z - w'‖ + ‖w' - w‖ := by
31     convert norm_add_le (z - w') (w' - w) using 1; ring_nf
32   linarith
33 
34 section Parameter
35 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
36 variable [NormedSpace ℝ E] [IsScalarTower ℝ ℂ E] [CompleteSpace E]
37 
38 omit [IsScalarTower ℝ ℂ E] [CompleteSpace E] in
39 /-- Differentiation of the actual finite Banach-valued cycle integral.
40 The domination is a constant times the integrable velocity, so no pointwise
41 bound on the velocity or piecewise smoothness is required. -/
42 theorem hasDerivAt_lineIntegral (Γ : IntegralCycle) {f f' : ℂ → ℂ → E}
43     {w : ℂ} {s : Set ℂ} (hs : s ∈ 𝓝 w)
44     (hf : ∀ w' ∈ s, ContinuousOn (f w') Γ.trace)
45     (hf' : ContinuousOn (f' w) Γ.trace)
46     (hderiv : ∀ w' ∈ s, ∀ z ∈ Γ.trace,
47       HasDerivAt (fun a => f a z) (f' w' z) w')
48     (M : ℝ) (hbound : ∀ w' ∈ s, ∀ z ∈ Γ.trace, ‖f' w' z‖ ≤ M) :
49     HasDerivAt (fun a => Γ.lineIntegral (f a)) (Γ.lineIntegral (f' w)) w := by
50   unfold IntegralCycle.lineIntegral
51   apply HasDerivAt.fun_sum
52   intro i hi
53   apply (intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le
54     (bound := fun t => ‖Γ.velocity i t‖ * M) hs ?_ ?_ ?_ ?_ ?_ ?_).2
55   · filter_upwards [hs] with a ha
56     simpa only [uIoc_of_le (by norm_num : (0 : ℝ) ≤ 1)] using
57       (Γ.integrable_lineIntegrand (hf a ha) i).1.aestronglyMeasurable
58   · exact Γ.integrable_lineIntegrand (hf w (mem_of_mem_nhds hs)) i
59   · simpa only [uIoc_of_le (by norm_num : (0 : ℝ) ≤ 1)] using
60       (Γ.integrable_lineIntegrand hf' i).1.aestronglyMeasurable
61   · filter_upwards with t ht a ha
62     have htrace : Γ.curve i t ∈ Γ.trace :=
63       ⟨i, t, by simpa using Ioc_subset_Icc_self ht, rfl⟩
64     rw [norm_smul]
65     exact mul_le_mul_of_nonneg_left (hbound a ha _ htrace) (norm_nonneg _)
66   · exact (Γ.velocity_integrable i).norm.mul_const M
67   · filter_upwards with t ht a ha
68     exact (hderiv a ha (Γ.curve i t)
69       ⟨i, t, by simpa using Ioc_subset_Icc_self ht, rfl⟩).const_smul (Γ.velocity i t)
70 
71 end Parameter
72 
73 end Komorebi.PaperII.ReleaseCycleParameter

Back to source controls