Higher-Order Cancellation Assembly

Assembles the per-term vanishing results into the full higher-order cancellation proof. The abstract theorem higherOrderCancel_assembly_abstract takes two callback hypotheses (holomorphic vanishing and finset vanishing) that are instantiated differently for convex vs null-homologous domains.

Main results

• higherOrderCancel_assembly_abstract: abstract assembly with callback hypotheses

The convex-domain specializations (higherOrderCancel_assembly, conditionsAB_imply_higherOrderCancel) are in FlatnessTransfer.lean.

theorem GeneralizedResidueTheory.higherOrderCancel_assembly_abstract (U : Set ℂ) (hU : IsOpen U) (S0 : Finset ℂ) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f (U \ ↑S0)) (γ : PiecewiseC1Immersion) (hγ_closed : γ.IsClosed) (hγ_in_U : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ U) (hMero : ∀ s ∈ S0, MeromorphicAt f s) (hCondA : SatisfiesConditionA' γ S0 fun (s : ℂ) => poleOrderAt f s) (hCondB : SatisfiesConditionB γ f S0) (_hγ_meas : Measurable γ.toFun) (h_no_endpt : ∀ s ∈ S0, γ.toFun γ.a ≠ s ∧ γ.toFun γ.b ≠ s) (h_unique_cross : ∀ s ∈ S0, ∀ t₁ ∈ Set.Icc γ.a γ.b, ∀ t₂ ∈ Set.Icc γ.a γ.b, γ.toFun t₁ = s → γ.toFun t₂ = s → t₁ = t₂) (hS0_in_U : ∀ s ∈ S0, s ∈ U) (h_holo_vanish : ∀ (g : ℂ → ℂ), DifferentiableOn ℂ g U → ∫ (t : ℝ) in γ.a..γ.b, g (γ.toFun t) * deriv γ.toFun t = 0) (h_finset_vanish : ∀ (T : Finset ℂ) (g : ℂ → ℂ), (∀ s ∈ T, MeromorphicAt g s) → (∀ s ∈ T, residueAt g s = 0) → DifferentiableOn ℂ g (U \ ↑T) → (∀ s ∈ T, s ∈ U) → (∀ s ∈ T, ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ≠ s) → ∫ (t : ℝ) in γ.a..γ.b, g (γ.toFun t) * deriv γ.toFun t = 0) : have h := fun (z : ℂ) => f z - ∑ s ∈ S0, residueAt f s / (z - s); Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 h γ.toFun ε t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)