Perturbations of a function by functions vanishing near its critical points

Let f be a C² function with globally Lipschitz gradient on a finite-dimensional real inner product space E, and h : ι → E → ℝ a finite family of C² functions with compact support, each vanishing on a neighbourhood of the critical set of f. The perturbed function is perturb f h s = f + ∑ᵢ sᵢ hᵢ for a parameter s : EuclideanSpace ℝ ι.

To study the dependence on s of the negative-gradient flow of perturb f h s, the parameter is made a state variable: the flow of a cut-off augmented field on E × EuclideanSpace ℝ ι is C¹ jointly in time, space and parameter, and agrees with the negative-gradient flow of perturb f h s for parameters in the closed unit ball.

Main declarations

• TauCeti.IsAdmissiblePerturbation f h: h is C², compactly supported, and its support avoids the critical points of f; ContDiffBump.isAdmissiblePerturbation_mul: a bump times a C² function is admissible when the bump's support avoids the critical points.
• TauCeti.perturb f h s: the perturbed function, with TauCeti.fderiv_perturb, TauCeti.gradient_perturb and TauCeti.contDiff_perturb; TauCeti.perturb_perturb: perturbing by the same family adds the parameters.
• TauCeti.perturb_eventuallyEq_of_fderiv_eq_zero: near each critical point of f the perturbation agrees with f.
• TauCeti.exists_pos_forall_fderiv_perturb_eq_zero_iff: for small parameters the critical points of perturb f h s are those of f; consequently TauCeti.exists_pos_forall_isAdmissiblePerturbation_perturb: an admissible family for f stays admissible for perturb f h s for small s.
• TauCeti.perturbedFlow f h hf hh hc: the flow of the field (x, s) ↦ (-∇ f x - ∑ᵢ a(s)ᵢ ∇ hᵢ x, 0) on E × EuclideanSpace ℝ ι, where a is the cutoff of the parameter. TauCeti.contDiff_perturbedFlow says it is C¹ jointly in time, space and parameter (TauCeti.contDiff_perturbedFlow_of_contDiff: C^{n+1} for C^{n+2} data), and TauCeti.perturbedFlow_apply_of_norm_le that, for ‖s‖ ≤ 1, it is the negative-gradient flow of perturb f h s, with the parameter carried along (TauCeti.snd_perturbedFlow_apply); TauCeti.perturbedFlow_congr: it does not depend on the Lipschitz witness for ∇ f. TauCeti.exists_lipschitzWith_gradient_perturb supplies the Lipschitz hypothesis needed to speak of that flow.
• TauCeti.hasDerivAt_fst_fderiv_perturbedFlow_apply: at the parameter 0, the derivative of the perturbed flow along a tangent vector (v, e) solves the inhomogeneous variational equation u' = -D(∇f)(φₜ x) u - ∑ᵢ eᵢ ∇hᵢ(φₜ x) along the negative-gradient orbit of x, with TauCeti.perturbedFlow_apply_zero and TauCeti.snd_fderiv_perturbedFlow_apply.
• TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral: Duhamel's formula for the derivative of the perturbed flow in a parameter direction at the parameter 0, and TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral_of_norm_lt at any parameter of norm less than 1, with the flow of the perturbation in place of the flow of f.
• TauCeti.range_fst_fderiv_perturbedFlow_inr_le: at the parameter 0, a family whose members all belong to a second family moves the perturbed flow in no more directions than the second.
• TauCeti.negativeGradientFlow_perturb_apply_eq, TauCeti.mem_stableSet_perturb_iff, TauCeti.mem_unstableSet_perturb_iff: away from the supports of the family, the perturbed flow, and membership in stable and unstable sets, are those of f.
• TauCeti.stableSet_perturb_inter_preimage_Iic, TauCeti.unstableSet_perturb_inter_preimage_Ici: for a family supported where f > c (resp. f < c), the stable sets where f ≤ c (resp. the unstable sets where c ≤ f) are those of f.

References

• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014 (transversality of the unstable and stable manifolds of a Morse function by perturbation).
• S. Smale, On gradient dynamical systems, Ann. of Math. 74 (1961), 199--206.

structure TauCeti.IsAdmissiblePerturbation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f h : E → ℝ) : Prop

A function h is an admissible perturbation of f when it is twice continuously differentiable, has compact support, and its support does not meet the critical points of f.

• contDiff : ContDiff ℝ 2 h

  h is twice continuously differentiable.

• hasCompactSupport : HasCompactSupport h

  h has compact support.

• disjoint : Disjoint (tsupport h) {x : E | fderiv ℝ f x = 0}

  The support of h avoids the critical points of f.

def TauCeti.perturb {E : Type u_1} {ι : Type u_2} [Fintype ι] (f : E → ℝ) (h : ι → E → ℝ) (s : EuclideanSpace ℝ ι) : E → ℝ

The perturbation f + ∑ᵢ sᵢ hᵢ of f by the family h with coefficients s.

@[simp]

theorem TauCeti.perturb_apply {E : Type u_1} {ι : Type u_2} [Fintype ι] (f : E → ℝ) (h : ι → E → ℝ) (s : EuclideanSpace ℝ ι) (x : E) : perturb f h s x = f x + ∑ i : ι, s.ofLp i * h i x

@[simp]

theorem TauCeti.perturb_zero {E : Type u_1} {ι : Type u_2} [Fintype ι] (f : E → ℝ) (h : ι → E → ℝ) : perturb f h 0 = f

@[simp]

theorem TauCeti.perturb_perturb {E : Type u_1} {ι : Type u_2} [Fintype ι] (f : E → ℝ) (h : ι → E → ℝ) (s₀ s : EuclideanSpace ℝ ι) : perturb (perturb f h s₀) h s = perturb f h (s₀ + s)

Perturbing a perturbation by the same family adds the parameters: f_{s₀} perturbed by s is f_{s₀ + s}.

@[simp]

theorem TauCeti.fderiv_perturb {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (hh : ∀ (i : ι), DifferentiableAt ℝ (h i) x) (s : EuclideanSpace ℝ ι) : fderiv ℝ (perturb f h s) x = fderiv ℝ f x + ∑ i : ι, s.ofLp i • fderiv ℝ (h i) x

The differential of a perturbation is the perturbed differential.

theorem TauCeti.contDiff_perturb {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {n : WithTop ℕ∞} (hfs : ContDiff ℝ n f) (hh : ∀ (i : ι), ContDiff ℝ n (h i)) (s : EuclideanSpace ℝ ι) : ContDiff ℝ n (perturb f h s)

The perturbation of a Cⁿ function by Cⁿ functions is Cⁿ.

theorem TauCeti.perturb_eventuallyEq_of_forall_notMem_tsupport {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {x : E} (s : EuclideanSpace ℝ ι) (hx : ∀ (i : ι), x ∉ tsupport (h i)) : perturb f h s =ᶠ[nhds x] f

A perturbation agrees with f near each point outside the supports of the family.

theorem TauCeti.perturb_eventuallyEq_of_fderiv_eq_zero {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} (hh : ∀ (i : ι), IsAdmissiblePerturbation f (h i)) (s : EuclideanSpace ℝ ι) {x : E} (hx : fderiv ℝ f x = 0) : perturb f h s =ᶠ[nhds x] f

Near a critical point of f, a perturbation agrees with f. The functions of an admissible family vanish on a neighbourhood of each critical point.

theorem TauCeti.exists_pos_forall_fderiv_perturb_eq_zero_iff {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} (hfs : ContDiff ℝ 1 f) (hh : ∀ (i : ι), ContDiff ℝ 1 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (hdisj : ∀ (i : ι), Disjoint (tsupport (h i)) {x : E | fderiv ℝ f x = 0}) : ∃ δ > 0, ∀ (s : EuclideanSpace ℝ ι), ‖s‖ < δ → ∀ (x : E), fderiv ℝ (perturb f h s) x = 0 ↔ fderiv ℝ f x = 0

Small perturbations keep the critical points. For a family of compactly supported C¹ functions whose supports avoid the critical points of f (for instance an admissible family), for all sufficiently small parameters the critical points of perturb f h s are those of f.

theorem TauCeti.exists_pos_forall_isAdmissiblePerturbation_perturb {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} (hfs : ContDiff ℝ 1 f) (hadm : ∀ (i : ι), IsAdmissiblePerturbation f (h i)) : ∃ δ > 0, ∀ (s : EuclideanSpace ℝ ι), ‖s‖ < δ → ∀ (i : ι), IsAdmissiblePerturbation (perturb f h s) (h i)

Admissibility persists under small perturbations. A family admissible for f stays admissible for perturb f h s for all sufficiently small s, since the critical points do not change.

theorem ContDiffBump.isAdmissiblePerturbation_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [HasContDiffBump E] {f : E → ℝ} {z : E} (θ : ContDiffBump z) (hθ : ∀ x ∈ Metric.closedBall z θ.rOut, fderiv ℝ f x ≠ 0) {g : E → ℝ} (hg : ContDiff ℝ 2 g) : TauCeti.IsAdmissiblePerturbation f fun (x : E) => ↑θ x * g x

Bumps away from the critical points give admissible perturbations. If the closed support of a smooth bump θ contains no critical point of f, then θ g is an admissible perturbation of f for every C² function g; for instance x ↦ θ x * ⟪v, x - z⟫.

@[simp]

theorem TauCeti.gradient_perturb {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {x : E} (hf : DifferentiableAt ℝ f x) (hh : ∀ (i : ι), DifferentiableAt ℝ (h i) x) (s : EuclideanSpace ℝ ι) : gradient (perturb f h s) x = gradient f x + ∑ i : ι, s.ofLp i • gradient (h i) x

The gradient of a perturbation is the perturbed gradient.

theorem TauCeti.gradient_perturb_of_forall_notMem_tsupport {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} (s : EuclideanSpace ℝ ι) {x : E} (hx : ∀ (i : ι), x ∉ tsupport (h i)) : gradient (perturb f h s) x = gradient f x

Outside the supports of the family, the gradient of a perturbation is the gradient of f.

theorem TauCeti.negativeGradientFlow_perturb_apply_eq {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) {s : EuclideanSpace ℝ ι} {K' : NNReal} (hf' : LipschitzWith K' (gradient (perturb f h s))) {y : E} {t : ℝ} (hy : ∀ τ ∈ Set.uIcc 0 t, ∀ (i : ι), (negativeGradientFlow f hf).toFun τ y ∉ tsupport (h i)) : (negativeGradientFlow (perturb f h s) hf').toFun t y = (negativeGradientFlow f hf).toFun t y

Away from the perturbation, the perturbed flow is the flow of f. If the orbit segment {φ_τ y | τ ∈ [[0, t]]} of the negative-gradient flow of f avoids the supports of the family, then the negative-gradient flow of perturb f h s sends y at time t to φ_t y.

theorem TauCeti.mem_stableSet_perturb_iff {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) {s : EuclideanSpace ℝ ι} {K' : NNReal} (hf' : LipschitzWith K' (gradient (perturb f h s))) {y q : E} (hy : ∀ (τ : ℝ), 0 ≤ τ → ∀ (i : ι), (negativeGradientFlow f hf).toFun τ y ∉ tsupport (h i)) : y ∈ (negativeGradientFlow (perturb f h s) hf').stableSet q ↔ y ∈ (negativeGradientFlow f hf).stableSet q

Stable sets away from the perturbation. If the forward orbit of y under the negative-gradient flow of f avoids the supports of the family, then y lies in the stable set of a point q for the perturbed flow if and only if it does for the flow of f.

theorem TauCeti.mem_unstableSet_perturb_iff {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) {s : EuclideanSpace ℝ ι} {K' : NNReal} (hf' : LipschitzWith K' (gradient (perturb f h s))) {y p : E} (hy : ∀ τ ≤ 0, ∀ (i : ι), (negativeGradientFlow f hf).toFun τ y ∉ tsupport (h i)) : y ∈ (negativeGradientFlow (perturb f h s) hf').unstableSet p ↔ y ∈ (negativeGradientFlow f hf).unstableSet p

Unstable sets away from the perturbation. If the backward orbit of y under the negative-gradient flow of f avoids the supports of the family, then y lies in the unstable set of a point p for the perturbed flow if and only if it does for the flow of f.

theorem TauCeti.stableSet_perturb_inter_preimage_Iic {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) {s : EuclideanSpace ℝ ι} {K' : NNReal} (hf' : LipschitzWith K' (gradient (perturb f h s))) {c : ℝ} (hc : ∀ (i : ι), tsupport (h i) ⊆ f ⁻¹' Set.Ioi c) (q : E) : (negativeGradientFlow (perturb f h s) hf').stableSet q ∩ f ⁻¹' Set.Iic c = (negativeGradientFlow f hf).stableSet q ∩ f ⁻¹' Set.Iic c

Stable sets below a level are unchanged. If the family is supported where f > c, then at points where f ≤ c the stable set of q for the perturbed flow is that for the flow of f: the forward orbits of these points stay below c.

theorem TauCeti.unstableSet_perturb_inter_preimage_Ici {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) {s : EuclideanSpace ℝ ι} {K' : NNReal} (hf' : LipschitzWith K' (gradient (perturb f h s))) {c : ℝ} (hc : ∀ (i : ι), tsupport (h i) ⊆ f ⁻¹' Set.Iio c) (p : E) : (negativeGradientFlow (perturb f h s) hf').unstableSet p ∩ f ⁻¹' Set.Ici c = (negativeGradientFlow f hf).unstableSet p ∩ f ⁻¹' Set.Ici c

Unstable sets above a level are unchanged. If the family is supported where f < c, then at points where c ≤ f the unstable set of p for the perturbed flow is that for the flow of f: the backward orbits of these points stay above c.

theorem TauCeti.exists_lipschitzWith_gradient_perturb {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hf : Differentiable ℝ f) (hK : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (s : EuclideanSpace ℝ ι) : ∃ (K' : NNReal), LipschitzWith K' (gradient (perturb f h s))

The gradient of a perturbation of f by compactly supported C² functions is Lipschitz if the gradient of f is, so its negative-gradient flow is defined.

noncomputable def TauCeti.perturbedFlow {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {K : NNReal} (f : E → ℝ) (h : ι → E → ℝ) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) : Flow ℝ (E × EuclideanSpace ℝ ι)

The flow of the cut-off augmented field on E × EuclideanSpace ℝ ι: the field is (x, s) ↦ (-∇ f x - ∑ᵢ a(s)ᵢ ∇ hᵢ x, 0), with a a smooth cutoff of the parameter equal to the identity on the closed unit ball. The parameter is constant along its orbits, and for ‖s‖ ≤ 1 the first component is the negative-gradient flow of perturb f h s (perturbedFlow_apply_of_norm_le); outside the unit ball it is the flow of the cut-off field, not of perturb f h s.

theorem TauCeti.perturbedFlow_congr {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K K' : NNReal} (hf : LipschitzWith K (gradient f)) (hf' : LipschitzWith K' (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) : perturbedFlow f h hf hh hc = perturbedFlow f h hf' hh hc

Independence of the Lipschitz witness. The perturbed flow does not depend on the Lipschitz bound for ∇ f used to construct it: both are flows of the same augmented field, which do not depend on the Lipschitz constant (flowOfLipschitz_congr).

theorem TauCeti.contDiff_perturbedFlow_of_contDiff {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (n : ℕ) (hfs : ContDiff ℝ (↑n + 2) f) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (hhs : ∀ (i : ι), ContDiff ℝ (↑n + 2) (h i)) : ContDiff ℝ (↑n + 1) (Function.uncurry (perturbedFlow f h hf hh hc).toFun)

Higher regularity of the perturbed flow: if f and the perturbing functions are C^{n+2}, the perturbed flow is C^{n+1} jointly in time, the initial condition and the parameter.

theorem TauCeti.contDiff_perturbedFlow {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) : ContDiff ℝ 1 (Function.uncurry (perturbedFlow f h hf hh hc).toFun)

The perturbed flow is C¹, jointly in time, the initial condition and the parameter.

@[simp]

theorem TauCeti.snd_perturbedFlow_apply {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (t : ℝ) (p : E × EuclideanSpace ℝ ι) : ((perturbedFlow f h hf hh hc).toFun t p).2 = p.2

The parameter is constant along the perturbed flow.

theorem TauCeti.perturbedFlow_apply_of_norm_le {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hd : Differentiable ℝ f) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) {s : EuclideanSpace ℝ ι} (hs : ‖s‖ ≤ 1) {K' : NNReal} (hf' : LipschitzWith K' (gradient (perturb f h s))) (t : ℝ) (x : E) : (perturbedFlow f h hf hh hc).toFun t (x, s) = ((negativeGradientFlow (perturb f h s) hf').toFun t x, s)

The perturbed flow is the negative-gradient flow of the perturbation. For a parameter s of norm at most 1, the perturbed flow sends (x, s) at time t to the pair of the time-t image of x under the negative-gradient flow of perturb f h s, and s.

@[simp]

theorem TauCeti.perturbedFlow_apply_zero {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (t : ℝ) (x : E) : (perturbedFlow f h hf hh hc).toFun t (x, 0) = ((negativeGradientFlow f hf).toFun t x, 0)

At the parameter 0 the perturbed flow is the negative-gradient flow of f.

@[simp]

theorem TauCeti.snd_fderiv_perturbedFlow_apply {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (t : ℝ) (p q : E × EuclideanSpace ℝ ι) : ((fderiv ℝ ((perturbedFlow f h hf hh hc).toFun t) p) q).2 = q.2

The parameter component of a variation is constant: the derivative of the time-t map of the perturbed flow does not change the parameter component of a tangent vector.

theorem TauCeti.hasDerivAt_fst_fderiv_perturbedFlow_apply {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (x : E) (q : E × EuclideanSpace ℝ ι) (t : ℝ) : HasDerivAt (fun (τ : ℝ) => ((fderiv ℝ ((perturbedFlow f h hf hh hc).toFun τ) (x, 0)) q).1) (-(fderiv ℝ (gradient f) ((negativeGradientFlow f hf).toFun t x)) ((fderiv ℝ ((perturbedFlow f h hf hh hc).toFun t) (x, 0)) q).1 - ∑ i : ι, q.2.ofLp i • gradient (h i) ((negativeGradientFlow f hf).toFun t x)) t

The variation of the perturbed flow. At the parameter 0, the derivative u t = (Dφₜ(x, 0) q).1 of the perturbed flow along a tangent vector q = (v, e) solves the inhomogeneous variational equation along the negative-gradient orbit φₜ x of f: u' = -D(∇f)(φₜ x) u - ∑ᵢ eᵢ ∇hᵢ(φₜ x). For q = (0, e) this is the derivative of s ↦ φ^{f + ∑ sᵢ hᵢ}_t x at s = 0 in the direction e; for q = (v, 0) it is the variational equation of the negative-gradient flow of f.

theorem TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (x : E) (e : EuclideanSpace ℝ ι) (T : ℝ) : ((fderiv ℝ ((perturbedFlow f h hf hh hc).toFun T) (x, 0)) (0, e)).1 = -(fderiv ℝ ((negativeGradientFlow f hf).toFun T) x) (∫ (σ : ℝ) in 0..T, (fderiv ℝ ((negativeGradientFlow f hf).toFun (-σ)) ((negativeGradientFlow f hf).toFun σ x)) (∑ i : ι, e.ofLp i • gradient (h i) ((negativeGradientFlow f hf).toFun σ x)))

Duhamel's formula for the parameter variation. At the parameter 0, the derivative of the perturbed flow in a parameter direction e is -Dφ_T(x) ∫₀ᵀ Dφ_{-σ}(φ_σ x) (∑ᵢ eᵢ ∇hᵢ(φ_σ x)) dσ, where φ is the negative-gradient flow of f: the perturbation ∑ᵢ eᵢ ∇hᵢ met along the orbit is transported back to time 0, integrated, and carried forward to time T.

theorem TauCeti.range_fst_fderiv_perturbedFlow_inr_le {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} {κ : Type u_3} [Fintype κ] {h' : κ → E → ℝ} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) (hh' : ∀ (k : κ), ContDiff ℝ 2 (h' k)) (hc' : ∀ (k : κ), HasCompactSupport (h' k)) (e : κ → ι) (he : ∀ (k : κ), h' k = h (e k)) (x : E) (T : ℝ) : (↑(ContinuousLinearMap.fst ℝ E (EuclideanSpace ℝ κ) ∘SL fderiv ℝ ((perturbedFlow f h' hf hh' hc').toFun T) (x, 0) ∘SL ContinuousLinearMap.inr ℝ E (EuclideanSpace ℝ κ))).range ≤ (↑(ContinuousLinearMap.fst ℝ E (EuclideanSpace ℝ ι) ∘SL fderiv ℝ ((perturbedFlow f h hf hh hc).toFun T) (x, 0) ∘SL ContinuousLinearMap.inr ℝ E (EuclideanSpace ℝ ι))).range

The parameter derivative only sees the functions of the family. If h' k = h (e k) for every k, then at the parameter 0 the range of the parameter derivative of the perturbed flow for h' is contained in that for h.

theorem TauCeti.fst_fderiv_perturbedFlow_apply_eq_neg_integral_of_norm_lt {E : Type u_1} {ι : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] {f : E → ℝ} {h : ι → E → ℝ} {K : NNReal} (hfs : ContDiff ℝ 2 f) (hf : LipschitzWith K (gradient f)) (hh : ∀ (i : ι), ContDiff ℝ 2 (h i)) (hc : ∀ (i : ι), HasCompactSupport (h i)) {s₀ : EuclideanSpace ℝ ι} (hs₀ : ‖s₀‖ < 1) {K' : NNReal} (hf' : LipschitzWith K' (gradient (perturb f h s₀))) (x : E) (e : EuclideanSpace ℝ ι) (T : ℝ) : ((fderiv ℝ ((perturbedFlow f h hf hh hc).toFun T) (x, s₀)) (0, e)).1 = -(fderiv ℝ ((negativeGradientFlow (perturb f h s₀) hf').toFun T) x) (∫ (σ : ℝ) in 0..T, (fderiv ℝ ((negativeGradientFlow (perturb f h s₀) hf').toFun (-σ)) ((negativeGradientFlow (perturb f h s₀) hf').toFun σ x)) (∑ i : ι, e.ofLp i • gradient (h i) ((negativeGradientFlow (perturb f h s₀) hf').toFun σ x)))

Duhamel's formula at a small parameter. For a parameter s₀ of norm less than 1, the derivative of the perturbed flow of f at (x, s₀) in a parameter direction e is -Dφ_T(x) ∫₀ᵀ Dφ_{-σ}(φ_σ x) (∑ᵢ eᵢ ∇hᵢ(φ_σ x)) dσ, where φ is now the negative-gradient flow of the perturbation f_{s₀}.