ReleaseAnalyticContourSup.lean

1 import KomorebiVerification.PaperII.ReleaseAnalyticContour
2 import Mathlib.Topology.Order.Compact
3 
4 set_option autoImplicit false
5 noncomputable section
6 namespace Komorebi.PaperII.ReleaseAnalyticContour
7 open scoped BigOperators Topology
8 open MeasureTheory Set TypedLinearDefects
9 universe u v
10 namespace IntegralCycle
11 
12 /-- A finite cycle has compact trace, including the empty cycle. -/
13 theorem isCompact_trace (Γ : IntegralCycle) : IsCompact Γ.trace := by
14   have htrace : Γ.trace = ⋃ i : Fin Γ.count, Γ.curve i '' uIcc (0:ℝ) 1 := by
15     ext z
16     simp only [trace, mem_ofPred_eq, mem_iUnion, mem_image]
17   rw [htrace]
18   exact isCompact_iUnion fun i => isCompact_uIcc.image_of_continuousOn (Γ.continuousOn_curve i)
19 
20 /-- Supremum norm on the trace, with explicit zero for an empty cycle. -/
21 def supNorm {E : Type u} [NormedAddCommGroup E] (Γ : IntegralCycle) (f : ℂ → E) : ℝ :=
22   sSup (insert 0 ((fun z => ‖f z‖) '' Γ.trace))
23 
24 theorem bddAbove_norms {E : Type u} [NormedAddCommGroup E]
25     (Γ : IntegralCycle) {f : ℂ → E} (hf : ContinuousOn f Γ.trace) :
26     BddAbove (insert 0 ((fun z => ‖f z‖) '' Γ.trace)) := by
27   exact (Γ.isCompact_trace.bddAbove_image hf.norm).insert 0
28 
29 theorem supNorm_nonneg {E : Type u} [NormedAddCommGroup E]
30     (Γ : IntegralCycle) {f : ℂ → E} (hf : ContinuousOn f Γ.trace) :
31     0 ≤ Γ.supNorm f := by
32   exact le_csSup (Γ.bddAbove_norms hf) (mem_insert _ _)
33 
34 theorem norm_le_supNorm {E : Type u} [NormedAddCommGroup E]
35     (Γ : IntegralCycle) {f : ℂ → E} (hf : ContinuousOn f Γ.trace)
36     {z : ℂ} (hz : z ∈ Γ.trace) : ‖f z‖ ≤ Γ.supNorm f := by
37   exact le_csSup (Γ.bddAbove_norms hf) (mem_insert_of_mem _ (mem_image_of_mem _ hz))
38 
39 /-- On a nonempty trace this is exactly the usual supremum of norms. -/
40 theorem supNorm_eq_sSup {E : Type u} [NormedAddCommGroup E]
41     (Γ : IntegralCycle) {f : ℂ → E} (hf : ContinuousOn f Γ.trace)
42     (hne : Γ.trace.Nonempty) :
43     Γ.supNorm f = sSup ((fun z => ‖f z‖) '' Γ.trace) := by
44   apply le_antisymm
45   · apply csSup_le (by simp)
46     intro b hb
47     rcases hb with rfl | hb
48     · obtain ⟨z,hz⟩ := hne
49       exact (norm_nonneg (f z)).trans
50         (le_csSup (Γ.isCompact_trace.bddAbove_image hf.norm) (mem_image_of_mem _ hz))
51     · exact le_csSup (Γ.isCompact_trace.bddAbove_image hf.norm) hb
52   · exact csSup_le_csSup (Γ.bddAbove_norms hf) (hne.image _) (subset_insert _ _)
53 end IntegralCycle
54 
55 /-- Exact supremum-norm version of the actual cycle integral defect estimate.
56 For an empty cycle, the explicitly defined suprema and integral are zero. -/
57 theorem dunfordIntegral_norm_defect_le_sup
58     {Ef : Type u} {Ec : Type v}
59     [NormedAddCommGroup Ef] [NormedAddCommGroup Ec]
60     [NormedSpace ℂ Ef] [NormedSpace ℂ Ec]
61     [NormedSpace ℝ Ef] [NormedSpace ℝ Ec]
62     [IsScalarTower ℝ ℂ Ef] [IsScalarTower ℝ ℂ Ec]
63     [CompleteSpace Ef] [CompleteSpace Ec]
64     (Γ : IntegralCycle) (h : ℂ → ℂ) (hh : ContinuousOn h Γ.trace)
65     (C : Ef →L[ℂ] Ec) (Tf : Ef →L[ℂ] Ef) (Tc : Ec →L[ℂ] Ec)
66     (hf : Γ.trace ⊆ resolventSet ℂ Tf) (hc : Γ.trace ⊆ resolventSet ℂ Tc) :
67     ‖C.comp (dunfordIntegral Γ h Tf) - (dunfordIntegral Γ h Tc).comp C‖ ≤
68       Γ.length / (2 * Real.pi) * Γ.supNorm h * ‖continuousDefect C Tf Tc‖ *
69         Γ.supNorm (resolvent Tc) * Γ.supNorm (resolvent Tf) := by
70   have hfc := continuousOn_resolvent_trace Γ Tf hf
71   have hcc := continuousOn_resolvent_trace Γ Tc hc
72   exact dunfordIntegral_norm_defect_le Γ h hh C Tf Tc hf hc _ _ _
73     (Γ.supNorm_nonneg hh) (Γ.supNorm_nonneg hcc) (Γ.supNorm_nonneg hfc)
74     (fun _ hz => Γ.norm_le_supNorm hh hz)
75     (fun _ hz => Γ.norm_le_supNorm hcc hz)
76     (fun _ hz => Γ.norm_le_supNorm hfc hz)
77 end Komorebi.PaperII.ReleaseAnalyticContour

Back to source controls