feat: derivative of the inversion (#5937)

Prove that inversion is smooth away from the center and its derivative is a scaled reflection.



Co-authored-by: Oliver Nash <github@olivernash.org>

Mathlib.lean

@@ -1893,6 +1893,7 @@ import Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
 import Mathlib.Geometry.Euclidean.Basic
 import Mathlib.Geometry.Euclidean.Circumcenter
 import Mathlib.Geometry.Euclidean.Inversion.Basic
+import Mathlib.Geometry.Euclidean.Inversion.Calculus
 import Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
 import Mathlib.Geometry.Euclidean.MongePoint
 import Mathlib.Geometry.Euclidean.PerpBisector

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -824,6 +824,17 @@ theorem Filter.EventuallyEq.hasStrictFDerivAt_iff (h : f₀ =ᶠ[𝓝 x] f₁) (
   simp only [*]
 #align filter.eventually_eq.has_strict_fderiv_at_iff Filter.EventuallyEq.hasStrictFDerivAt_iff
 
+theorem HasStrictFDerivAt.congr_fderiv (h : HasStrictFDerivAt f f' x) (h' : f' = g') :
+    HasStrictFDerivAt f g' x :=
+  h' ▸ h
+
+theorem HasFDerivAt.congr_fderiv (h : HasFDerivAt f f' x) (h' : f' = g') : HasFDerivAt f g' x :=
+  h' ▸ h
+
+theorem HasFDerivWithinAt.congr_fderiv (h : HasFDerivWithinAt f f' s x) (h' : f' = g') :
+    HasFDerivWithinAt f g' s x :=
+  h' ▸ h
+
 theorem HasStrictFDerivAt.congr_of_eventuallyEq (h : HasStrictFDerivAt f f' x)
     (h₁ : f =ᶠ[𝓝 x] f₁) : HasStrictFDerivAt f₁ f' x :=
   (h₁.hasStrictFDerivAt_iff fun _ => rfl).1 h

Mathlib/Analysis/InnerProductSpace/Calculus.lean

@@ -226,6 +226,14 @@ theorem hasStrictFDerivAt_norm_sq (x : F) :
   simp [two_smul, real_inner_comm]
 #align has_strict_fderiv_at_norm_sq hasStrictFDerivAt_norm_sqₓ
 
+theorem HasFDerivAt.norm_sq {f : G → F} {f' : G →L[ℝ] F} (hf : HasFDerivAt f f' x) :
+    HasFDerivAt (‖f ·‖ ^ 2) (2 • (innerSL ℝ (f x)).comp f') x :=
+  (hasStrictFDerivAt_norm_sq _).hasFDerivAt.comp x hf
+
+theorem HasFDerivWithinAt.norm_sq {f : G → F} {f' : G →L[ℝ] F} (hf : HasFDerivWithinAt f f' s x) :
+    HasFDerivWithinAt (‖f ·‖ ^ 2) (2 • (innerSL ℝ (f x)).comp f') s x :=
+  (hasStrictFDerivAt_norm_sq _).hasFDerivAt.comp_hasFDerivWithinAt x hf
+
 theorem DifferentiableAt.norm_sq (hf : DifferentiableAt ℝ f x) :
     DifferentiableAt ℝ (fun y => ‖f y‖ ^ 2) x :=
   ((contDiffAt_id.norm_sq 𝕜).differentiableAt le_rfl).comp x hf

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -744,6 +744,10 @@ theorem reflection_orthogonal : reflection Kᗮ = .trans (reflection K) (.neg _)
 
 variable {K}
 
+theorem reflection_singleton_apply (u v : E) :
+    reflection (𝕜 ∙ u) v = 2 • (⟪u, v⟫ / ((‖u‖ : 𝕜) ^ 2)) • u - v := by
+  rw [reflection_apply, orthogonalProjection_singleton, ofReal_pow]
+
 /-- A point is its own reflection if and only if it is in the subspace. -/
 theorem reflection_eq_self_iff (x : E) : reflection K x = x ↔ x ∈ K := by
   rw [← orthogonalProjection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,

Mathlib/Geometry/Euclidean/Inversion/Calculus.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2023 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Geometry.Euclidean.Inversion.Basic
+import Mathlib.Analysis.InnerProductSpace.Calculus
+import Mathlib.Analysis.Calculus.Deriv.Inv
+
+/-!
+# Derivative of the inversion
+
+In this file we prove a formula for the derivative of `EuclideanGeometry.inversion c R`.
+
+## Implementation notes
+
+Since `fderiv` and related definiitons do not work for affine spaces, we deal with an inner product
+space in this file.
+
+## Keywords
+
+inversion, derivative
+-/
+
+local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See Lean 4 issue #2220
+
+open Metric Function AffineMap Set AffineSubspace
+open scoped Topology RealInnerProductSpace
+
+variable {E F : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [InnerProductSpace ℝ F]
+
+open EuclideanGeometry
+
+section DotNotation
+
+variable {c x : E → F} {R : E → ℝ} {s : Set E} {a : E} {n : ℕ∞}
+
+protected theorem ContDiffWithinAt.inversion (hc : ContDiffWithinAt ℝ n c s a)
+    (hR : ContDiffWithinAt ℝ n R s a) (hx : ContDiffWithinAt ℝ n x s a) (hne : x a ≠ c a) :
+    ContDiffWithinAt ℝ n (fun a ↦ inversion (c a) (R a) (x a)) s a :=
+  (((hR.div (hx.dist ℝ hc hne) (dist_ne_zero.2 hne)).pow _).smul (hx.sub hc)).add hc
+
+protected theorem ContDiffOn.inversion (hc : ContDiffOn ℝ n c s) (hR : ContDiffOn ℝ n R s)
+    (hx : ContDiffOn ℝ n x s) (hne : ∀ a ∈ s, x a ≠ c a) :
+    ContDiffOn ℝ n (fun a ↦ inversion (c a) (R a) (x a)) s := fun a ha ↦
+  (hc a ha).inversion (hR a ha) (hx a ha) (hne a ha)
+
+protected nonrec theorem ContDiffAt.inversion (hc : ContDiffAt ℝ n c a) (hR : ContDiffAt ℝ n R a)
+    (hx : ContDiffAt ℝ n x a) (hne : x a ≠ c a) :
+    ContDiffAt ℝ n (fun a ↦ inversion (c a) (R a) (x a)) a :=
+  hc.inversion hR hx hne
+
+protected nonrec theorem ContDiff.inversion (hc : ContDiff ℝ n c) (hR : ContDiff ℝ n R)
+    (hx : ContDiff ℝ n x) (hne : ∀ a, x a ≠ c a) :
+    ContDiff ℝ n (fun a ↦ inversion (c a) (R a) (x a)) :=
+  contDiff_iff_contDiffAt.2 fun a ↦ hc.contDiffAt.inversion hR.contDiffAt hx.contDiffAt (hne a)
+
+protected theorem DifferentiableWithinAt.inversion (hc : DifferentiableWithinAt ℝ c s a)
+    (hR : DifferentiableWithinAt ℝ R s a) (hx : DifferentiableWithinAt ℝ x s a) (hne : x a ≠ c a) :
+    DifferentiableWithinAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) s a :=
+  -- TODO: Use `.div` #5870 
+  (((hR.mul <| (hx.dist ℝ hc hne).inv (dist_ne_zero.2 hne)).pow _).smul (hx.sub hc)).add hc
+
+protected theorem DifferentiableOn.inversion (hc : DifferentiableOn ℝ c s)
+    (hR : DifferentiableOn ℝ R s) (hx : DifferentiableOn ℝ x s) (hne : ∀ a ∈ s, x a ≠ c a) :
+    DifferentiableOn ℝ (fun a ↦ inversion (c a) (R a) (x a)) s := fun a ha ↦
+  (hc a ha).inversion (hR a ha) (hx a ha) (hne a ha)
+
+protected theorem DifferentiableAt.inversion (hc : DifferentiableAt ℝ c a)
+    (hR : DifferentiableAt ℝ R a) (hx : DifferentiableAt ℝ x a) (hne : x a ≠ c a) :
+    DifferentiableAt ℝ (fun a ↦ inversion (c a) (R a) (x a)) a := by
+  rw [← differentiableWithinAt_univ] at *
+  exact hc.inversion hR hx hne
+
+protected theorem Differentiable.inversion (hc : Differentiable ℝ c)
+    (hR : Differentiable ℝ R) (hx : Differentiable ℝ x) (hne : ∀ a, x a ≠ c a) :
+    Differentiable ℝ (fun a ↦ inversion (c a) (R a) (x a)) := fun a ↦
+  (hc a).inversion (hR a) (hx a) (hne a)
+
+end DotNotation
+
+namespace EuclideanGeometry
+
+variable {a b c d x y z : F} {r R : ℝ}
+
+/-- Formula for the Fréchet derivative of `EuclideanGeometry.inversion c R`. -/
+theorem hasFDerivAt_inversion (hx : x ≠ c) :
+    HasFDerivAt (inversion c R)
+      ((R / dist x c) ^ 2 • (reflection (ℝ ∙ (x - c))ᗮ : F →L[ℝ] F)) x := by
+  rcases add_left_surjective c x with ⟨x, rfl⟩
+  have : HasFDerivAt (inversion c R) (_ : F →L[ℝ] F) (c + x)
+  · simp_rw [inversion, dist_eq_norm, div_pow, div_eq_mul_inv]
+    have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c
+    have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul
+      (R ^ 2)
+    exact (B.smul A).add_const c
+  refine this.congr_fderiv (LinearMap.ext_on_codisjoint
+    (Submodule.isCompl_orthogonal_of_completeSpace (K := ℝ ∙ x)).codisjoint
+    (LinearMap.eqOn_span' ?_) fun y hy ↦ ?_)
+  · have : ((‖x‖ ^ 2) ^ 2)⁻¹ * (‖x‖ ^ 2) = (‖x‖ ^ 2)⁻¹
+    · rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']
+    simp [reflection_orthogonalComplement_singleton_eq_neg, real_inner_self_eq_norm_sq,
+      two_mul, this, div_eq_mul_inv, mul_add, add_smul, mul_pow]
+  · simp [Submodule.mem_orthogonal_singleton_iff_inner_right.1 hy,
+      reflection_mem_subspace_eq_self hy, div_eq_mul_inv, mul_pow]
+
+end EuclideanGeometry