OAI/Analysis/CircleDomains/Sobolev/MetricInterpolation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric line 21
2. def OAI.CircleDomainRigidity.FiniteTransfer.matrixEnergy line 23
3. def OAI.CircleDomainRigidity.FiniteTransfer.blendMetric line 26
4. theorem OAI.CircleDomainRigidity.FiniteTransfer.blendMetric_zero line 29
5. theorem OAI.CircleDomainRigidity.FiniteTransfer.blendMetric_one line 32
6. theorem OAI.CircleDomainRigidity.FiniteTransfer.blendMetric_posDef line 35
7. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousOn_matrixEnergy line 43
8. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_core_preserving_metric line 62

   Source documentation

   Replace a smooth positive definite metric by the identity near a compact core. The change of the actual coordinate energy outside that core is small. The transition can be confined to any prescribed open neighborhood.

   theorem exists_core_preserving_metric
       {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
       {μ : Measure E} [IsFiniteMeasureOnCompacts μ]
       {K S U : Set E} (hK : IsCompact K) (hS : Bornology.IsBounded S)
       (hSm : MeasurableSet S) (hU : IsOpen U) (hKU : K ⊆ U)
       (A g : E → PlanarMetric) (hA : Continuous A) (hg : ContDiff ℝ ∞ g)
       (hPD : ∀ x, (g x).PosDef) {ε : ℝ} (hε : 0 < ε) :
       ∃ (N : Set E) (g' : E → PlanarMetric), IsOpen N ∧ K ⊆ N ∧ N ⊆ U ∧
         ContDiff ℝ ∞ g' ∧ (∀ x, (g' x).PosDef) ∧
         (∀ᶠ x in 𝓝ˢ K, g' x = 1) ∧ (∀ x ∉ N, g' x = g x) ∧
         (∫ x in S \ K, |matrixEnergy (A x) (g' x) - matrixEnergy (A x) (g x)| ∂μ) < ε := by
   …

   Mentions: OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.matrixEnergy

9. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuous_matrixEnergy line 94
10. theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_lt_of_abs_sub_lt line 100
11. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_core_gramMetric line 116

    Source documentation

    The complete local metric step: small pairwise wedges give one smooth positive definite metric with the prescribed total energy bound, equal to the original identity metric on a full neighborhood of the retained core. The constant regularization and the transition region are both constructed.

    theorem exists_smooth_core_gramMetric
        (x y : ℕ → (ℝ × ℝ) → ℝ) (n : ℕ)
        (hx : ∀ i, ContDiff ℝ ∞ (x i)) (hy : ∀ i, ContDiff ℝ ∞ (y i))
        {K S U : Set (ℝ × ℝ)} (hK : IsCompact K) (hS : Bornology.IsBounded S)
        (hSm : MeasurableSet S) (hU : IsOpen U) (hKU : K ⊆ U) {ε : ℝ}
        (hε : (∫ z in S \ K, 2 * covectorWedges (fun i => x i z) (fun i => y i z) n) < ε) :
        ∃ (τ : ℝ) (N : Set (ℝ × ℝ)) (g : (ℝ × ℝ) → PlanarMetric),
          0 < τ ∧ IsOpen N ∧ K ⊆ N ∧ N ⊆ U ∧ ContDiff ℝ ∞ g ∧
          (∀ z, (g z).PosDef) ∧ (∀ᶠ z in 𝓝ˢ K, g z = 1) ∧
          (∀ z ∉ N, g z = gramTensor (fun i => x i z) (fun i => y i z) n + τ • 1) ∧
          (∫ z in S \ K, matrixEnergy (gramTensor (fun i => x i z) (fun i => y i z) n) (g z)) < ε := by
    …

    Mentions: OAI.CircleDomainRigidity.FiniteTransfer.covectorWedges, OAI.CircleDomainRigidity.FiniteTransfer.PlanarMetric, OAI.CircleDomainRigidity.FiniteTransfer.gramTensor, OAI.CircleDomainRigidity.FiniteTransfer.matrixEnergy