ThinCollar.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Interpolation in a thin exterior neighborhood

For a compact retained core, integrals over shrinking exterior neighborhoods tend to zero. A continuous family of energy densities can consequently be interpolated smoothly to its original value near the core with arbitrarily small added energy. No measure-zero assumption on the core boundary is used.

theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGridStep_antitone line 24
theorem OAI.CircleDomainRigidity.FiniteTransfer.iInter_outer_thickenings_eq_empty line 30
theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_integral_outer_thickenings line 45

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_interpolation_small_change line 63

Source documentation

Smoothly select the original member H (x,0) near the retained core, and the new member H (x,1) away from a small neighborhood. The absolute change of its integral outside the core is arbitrarily small.

theorem exists_smooth_interpolation_small_change
    {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)
    (H : E × ℝ → ℝ) (hH : ContinuousOn H (univ ×ˢ Icc 0 1))
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (N : Set E) (χ : E → ℝ), IsOpen N ∧ K ⊆ N ∧ N ⊆ U ∧
      ContDiff ℝ ∞ χ ∧ (∀ x, χ x ∈ Icc 0 1) ∧
      (∀ᶠ x in 𝓝ˢ K, χ x = 0) ∧ (∀ x ∉ N, χ x = 1) ∧
      (∫ x in S \ K, |H (x, χ x) - H (x, 1)| ∂μ) < ε := by
…