TransportedRealLocalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Energy transport on retained source subsets and away from a prescribed core set.

theorem OAI.CircleDomainRigidity.transported_real_energy_on_source_set line 16

theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.transported_energy_away_lt line 54

Source documentation

The finite target energy away from a retained source set is charged to original source energy away from that same set, plus the transfer error.

theorem transported_energy_away_lt (l : Fin n)
    {E : Set (ℝ × ℝ)} (hE : MeasurableSet E) (hEc : E ⊆ M.core)
    {W : Set ℂ} (hW : W ⊆ Complex.equivRealProdCLM ⁻¹'
      (sphereRealMap M.forward '' (realChartDomain (openCompletedRegion M.terminals.H) \ E))) :
    IntegrableOn (euclideanGradientEnergy
      ((sphereRealFunction (M.functions l) ∘ M.inverse) ∘ ((↑) : ℂ → Sphere))) W ∧
    (∫ z in W, euclideanGradientEnergy
      ((sphereRealFunction (M.functions l) ∘ M.inverse) ∘ ((↑) : ℂ → Sphere)) z) <
      (∫ x in realChartDomain G \ E,
        gradientEnergy (u l) (fun z => sphericalMetricFactor z • 1) x) + ε := by
…

Mentions: OAI.CircleDomainRigidity.sphereRealMap, OAI.CircleDomainRigidity.FiniteTransfer.realChartDomain, OAI.CircleDomainRigidity.FiniteTransfer.openCompletedRegion, OAI.CircleDomainRigidity.euclideanGradientEnergy, OAI.CircleDomainRigidity.sphereRealFunction, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.gradientEnergy, OAI.CircleDomainRigidity.FiniteTransfer.sphericalMetricFactor