De Giorgi's theorem for a coefficient with a jump

This file runs the energy method and De Giorgi's theorem on an explicit equation whose coefficient is discontinuous, so that no regularity theory for continuous coefficients applies to it.

The coefficient field is TauCeti.PDE.jumpCoefficient n, the matrix κ(x) I on ℝⁿ⁺¹ with κ(x) = 1 on the open half-space {x₀ > 0} and κ(x) = 2 on its complement. It is measurable and uniformly elliptic with constants 1 and 2, and it is discontinuous at every point of the hyperplane {x₀ = 0} (TauCeti.PDE.not_continuousAt_jumpCoefficient), in particular inside the unit ball.

On a bounded nonempty open set Ω, consider the Dirichlet problem

-div(κ ∇u) = 0 in Ω, u = x₀ on ∂Ω,

in its weak form: u ∈ H¹(Ω), u - g ∈ H¹₀(Ω) for a function g ∈ H¹(Ω) equal to the coordinate x₀ almost everywhere, and ∫_Ω κ ∇u · ∇v = 0 for every v ∈ H¹₀(Ω). TauCeti.PDE.exists_holderOnWith_preciseRepresentative_jumpCoefficient proves:

• the problem has exactly one weak solution, by Lax–Milgram; a priori it is only known to lie in H¹(Ω);
• the solution is not constant, since a constant minus x₀ is not in H¹₀(Ω) (TauCeti.W1p0.not_exists_value_ae_eq_const_of_inner_gradient_eq_one);
• by De Giorgi's theorem its precise representative is Hölder continuous on every compact subset of Ω, with an exponent α ∈ (0, 1] depending only on the dimension.

References

• E. De Giorgi, Sulla differenziabilità e l'analiticità delle estremali degli integrali multipli regolari, Mem. Accad. Sci. Torino (1957).
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 8.3 and Theorem 8.24.

noncomputable def TauCeti.PDE.jumpCoefficient (n : ℕ) (x : EuclideanSpace ℝ (Fin (n + 1))) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ

The coefficient field κ(x) I on ℝⁿ⁺¹ with κ(x) = 1 where x₀ > 0 and κ(x) = 2 elsewhere: a uniformly elliptic matrix field with a jump across the hyperplane {x₀ = 0}.

theorem TauCeti.PDE.jumpCoefficient_apply {n : ℕ} (x : EuclideanSpace ℝ (Fin (n + 1))) : jumpCoefficient n x = (if 0 < x.ofLp 0 then 1 else 2) • 1

Unfolding TauCeti.PDE.jumpCoefficient.

theorem TauCeti.PDE.uniformlyEllipticOn_jumpCoefficient {n : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))) : UniformlyEllipticOn Ω (jumpCoefficient n) 1 2

The jump coefficient is uniformly elliptic with constants 1 and 2 on every set.

theorem TauCeti.PDE.stronglyMeasurable_jumpCoefficient {n : ℕ} : MeasureTheory.StronglyMeasurable (jumpCoefficient n)

The jump coefficient is strongly measurable.

theorem TauCeti.PDE.not_continuousAt_jumpCoefficient {n : ℕ} {x : EuclideanSpace ℝ (Fin (n + 1))} (hx : x.ofLp 0 = 0) : ¬ContinuousAt (jumpCoefficient n) x

The jump coefficient is discontinuous at every point of the hyperplane {x₀ = 0}.

theorem TauCeti.PDE.exists_holderOnWith_preciseRepresentative_jumpCoefficient (n : ℕ) : ∃ (α : NNReal), 0 < α ∧ α ≤ 1 ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin (n + 1)))}, Bornology.IsBounded ↑Omega → (↑Omega).Nonempty → ∃ (g : ↥(W1p MeasureTheory.volume Omega 2)), (↑↑(W1p.value g) =ᵐ[MeasureTheory.volume.restrict ↑Omega] fun (x : EuclideanSpace ℝ (Fin (n + 1))) => x.ofLp 0) ∧ (∃! u : ↥(W1p MeasureTheory.volume Omega 2), u - g ∈ w1p0Submodule MeasureTheory.volume Omega 2 ∧ ∀ (v : ↥(W1p0 MeasureTheory.volume Omega 2)), energyFormH1 (jumpCoefficient n) 0 0 u ↑v = 0) ∧ ∀ (u : ↥(W1p MeasureTheory.volume Omega 2)), (u - g ∈ w1p0Submodule MeasureTheory.volume Omega 2 ∧ ∀ (v : ↥(W1p0 MeasureTheory.volume Omega 2)), energyFormH1 (jumpCoefficient n) 0 0 u ↑v = 0) → (¬∃ (c : ℝ), ↑↑(W1p.value u) =ᵐ[MeasureTheory.volume.restrict ↑Omega] fun (x : EuclideanSpace ℝ (Fin (n + 1))) => c) ∧ ∀ (K : Set (EuclideanSpace ℝ (Fin (n + 1)))), IsCompact K → K ⊆ ↑Omega → ∃ (C : NNReal), HolderOnWith C α (MeasureTheory.preciseRepresentative MeasureTheory.volume ↑↑(W1p.value u)) K

De Giorgi's theorem on an equation with a discontinuous coefficient. There is α ∈ (0, 1], depending only on the dimension, such that the following holds on every bounded nonempty open set Ω ⊆ ℝⁿ⁺¹. Let g ∈ H¹(Ω) be the coordinate function x₀. The Dirichlet problem -div(κ ∇u) = 0 in Ω, u = x₀ on ∂Ω, for the coefficient κ I = TauCeti.PDE.jumpCoefficient n with a jump across {x₀ = 0}, has exactly one weak solution u ∈ H¹(Ω), that is u - g ∈ H¹₀(Ω) and ∫_Ω κ ∇u · ∇v = 0 for every v ∈ H¹₀(Ω). This solution is not constant, and its precise representative is Hölder continuous with exponent α on every compact subset of Ω.