OAI/Analysis/CircleDomains/Sobolev/CovectorMetric.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Metric selection for local covectors

Periodic coordinates need not have a global scalar potential. The Gram argument applies to their smooth covector fields, retaining the spherical metric near a closed core and near infinity, and realizing masked fields by smooth extensions.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.fieldEnergy line 22
  2. def OAI.CircleDomainRigidity.FiniteTransfer.fieldGram line 25
  3. def OAI.CircleDomainRigidity.FiniteTransfer.fieldWedges line 28
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousOn_fieldEnergy line 31
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_fieldGram_eq_sum line 52
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_spherical_metric_for_covectors line 64

    Source documentation

    The spherical Gram metric construction does not require exactness of the covectors and therefore applies to periodic differentials.

    theorem exists_spherical_metric_for_covectors
    (v : ℕ → (ℝ × ℝ) → ℝ × ℝ) (n : ℕ) (hv : ∀ i, ContDiff ℝ ∞ (v i))
    {Q K : Set (ℝ × ℝ)} (hQ : IsCompact Q) (hK : IsClosed K) {ε : ℝ}
    (hε : (∫ z in Q \ K, 2 * fieldWedges v n z) < ε) :
    ∃ (R : ℝ) (g : (ℝ × ℝ) → PlanarMetric), 0 < R ∧ ContDiff ℝ ∞ g ∧
      (∀ z, (g z).PosDef) ∧
      (∀ᶠ z in 𝓝ˢ K, g z = sphericalMetricFactor z • 1) ∧
      (∀ z ∉ closedBall 0 R, g z = sphericalMetricFactor z • 1) ∧
      (∫ z in Q \ K, matrixEnergy (fieldGram v n z) (g z)) < ε := by
…

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.fieldWedges, OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.sphericalMetricFactor, OAI.CircleDomainRigidity.FiniteTransfer.matrixEnergy, OAI.CircleDomainRigidity.FiniteTransfer.fieldGram

  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_masked_covector line 131

    Source documentation

    Extend a local covector field across the inactive side of a mask. No global scalar primitive is introduced.

    theorem exists_smooth_masked_covector
    {Ω Q K M : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hM : IsClosed M) (hboundary : frontier M ⊆ interior K)
    {v : (ℝ × ℝ) → ℝ × ℝ} (hv : ContDiffOn ℝ ∞ v (Ω ∩ interior M)) :
    ∃ V : (ℝ × ℝ) → ℝ × ℝ, ContDiff ℝ ∞ V ∧
      ∀ z ∈ Q \ K, V z = M.indicator v z := by
…