SphereCircleEnergy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Energy transport through a metric-conformal sphere map

On the finite charts, the actual sphere map and actual intrinsic circle coordinate satisfy the Dirichlet change-of-variables formula. The source set may be any measurable part of a mask or of a localized tail.

theorem OAI.CircleDomainRigidity.integral_circleEnergy_metric_sphere_map line 24

theorem OAI.CircleDomainRigidity.integral_filled_circleEnergy_metric_sphere_map line 51

Source documentation

The same formula for a source coordinate identified locally with the pullback. This is the equality used for the filled coordinates.

theorem integral_filled_circleEnergy_metric_sphere_map
    {s W : Set (ℝ × ℝ)} (hs : MeasurableSet s) (hW : IsOpen W)
    {U : Set Sphere} {f : Sphere → Sphere} (hinj : InjOn f U)
    (hsU : ∀ x ∈ s, ((Complex.equivRealProdCLM.symm x : ℂ) : Sphere) ∈ U)
    {g : (ℝ × ℝ) → PlanarMetric}
    (hf : ∀ p ∈ U, IsMetricConformalAt g f p) (hg : ∀ x ∈ s, (g x).PosDef)
    (hfinite : ∀ x ∈ s, f ((Complex.equivRealProdCLM.symm x : ℂ) : Sphere) ≠ OnePoint.infty)
    (hmap : MapsTo (sphereRealMap f) s W)
    (u F : (ℝ × ℝ) → UnitAddCircle) (hu : SmoothCircleOn u W)
    (hcoordinate : ∀ x ∈ s, (u ∘ sphereRealMap f) =ᶠ[𝓝 x] F) :
    (∫ y in sphereRealMap f '' s, fieldEnergy (circleGradient u) (fun _ => 1) y) =
      ∫ x in s, fieldEnergy (circleGradient F) g x := by
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsMetricConformalAt, OAI.CircleDomainRigidity.sphereRealMap