PlanarEnergyChange.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The integral energy formula in the real chart

Mathlib's change-of-variables theorem combines with the proved covector pullback identity. This works on arbitrary measurable subsets, including each mask and each localized tail of a finite completion.

def OAI.CircleDomainRigidity.FiniteTransfer.planeDerivativeMatrix line 20
theorem OAI.CircleDomainRigidity.FiniteTransfer.det_planeDerivativeMatrix line 23

theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_covectorEnergy_change_variables line 29

Source documentation

Dirichlet energy of a target covector field equals energy of its actual pullback in any conformally rescaled pullback metric.

theorem integral_covectorEnergy_change_variables
    {s : Set (ℝ × ℝ)} (hs : MeasurableSet s)
    (f : (ℝ × ℝ) → (ℝ × ℝ)) (A : (ℝ × ℝ) → ((ℝ × ℝ) →L[ℝ] (ℝ × ℝ)))
    (hf : ∀ x ∈ s, HasFDerivWithinAt f (A x) s x) (hinj : InjOn f s)
    (hdet : ∀ x ∈ s, (A x).det ≠ 0)
    (v : (ℝ × ℝ) → Fin 2 → ℝ) (g : (ℝ × ℝ) → PlanarMetric)
    (hPD : ∀ x ∈ s, (g (f x)).PosDef)
    (c : (ℝ × ℝ) → ℝ) (hc : ∀ x ∈ s, 0 < c x) :
    (∫ y in f '' s, covectorEnergy (v y) (g y)) =
      ∫ x in s, covectorEnergy ((planeDerivativeMatrix (A x))ᵀ *ᵥ v (f x))
        (c x • ((planeDerivativeMatrix (A x))ᵀ * g (f x) * planeDerivativeMatrix (A x))) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.covectorEnergy, OAI.CircleDomainRigidity.FiniteTransfer.planeDerivativeMatrix