The L² Leibniz estimate to No Poincaré inequality holds on…

TheoremThe L² Leibniz estimate#

At exponent two, the gradient ψ ∇u + u ∇ψ of ψ u satisfies

‖∇(ψ u)‖₂² ≤ 2 ∫_Ω ψ² ‖∇u‖² + 2 ∫_Ω ‖∇ψ‖² u².

Unlike TauCeti.W1p.norm_contDiffSMul_le, the two terms keep their weights ψ² and ‖∇ψ‖², which is the form in which energy estimates such as Caccioppoli's inequality are applied to a localized function.

TauCeti.W1p.norm_gradient_contDiffSMul_sq_le.{u_1} {E : Type u_1} [MeasurableSpace E]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E}
  {psi : E → ℝ} {M : ℝ} (hpsi : ContDiff ℝ (↑⊤) psi) (hM : 0 ≤ M) (hpsiM : ∀ x ∈ Omega, |psi x| ≤ M)
  (hgradM : ∀ x ∈ Omega, ‖gradient psi x‖ ≤ M) (u : ↥(TauCeti.W1p mu Omega 2)) :
  ‖TauCeti.W1p.gradient (TauCeti.W1p.contDiffSMul psi hpsi hM hpsiM hgradM u)‖ ^ 2 ≤
    2 * ∫ (x : E) in ↑Omega, psi x ^ 2 * ‖↑↑(TauCeti.W1p.gradient u) x‖ ^ 2 ∂mu +
      2 * ∫ (x : E) in ↑Omega, ‖gradient psi x‖ ^ 2 * ↑↑(TauCeti.W1p.value u) x ^ 2 ∂mu
Lean

Formalized in Tau Ceti as TauCeti.W1p.norm_gradient_contDiffSMul_sq_le.

Sources
LeanTauCeti.W1p.norm_gradient_contDiffSMul_sq_le
Used by 5
Used byDe Giorgi's interior oscillation estimate · De Giorgi's theorem: Hölder continuity of weak solutions · Moser's Harnack inequality · Moser's reverse Hölder inequality for powers of a positive supersolution · Moser's lower bound from small negative powers

TheoremThe analytic content of the extension theorem#

The zero-extension of u ∈ W^{1,p}_0(Ω) is weakly differentiable on the larger open set Ω', with weak gradient the zero-extension of the weak gradient of u. This is the statement that can fail for a general u ∈ W^{1,p}(Ω): with no condition forcing u to vanish towards ∂Ω, its zero-extension need not be weakly differentiable on Ω' at all.

TauCeti.W1p0.hasWeakFDerivOn_indicator.{u_1} {E : Type u_1} [MeasurableSpace E]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega Omega' : TopologicalSpace.Opens E}
  {p : ENNReal} [Fact (1 ≤ p)] (hsub : Omega ≤ Omega') (u : ↥(TauCeti.W1p0 mu Omega p)) :
  TauCeti.HasWeakFDerivOn mu Omega' ((↑Omega).indicator ↑↑(TauCeti.W1p.value ↑u)) fun x =>
    (innerSL ℝ) ((↑Omega).indicator (↑↑(TauCeti.W1p.gradient ↑u)) x)
Lean

Formalized in Tau Ceti as TauCeti.W1p0.hasWeakFDerivOn_indicator.

Sources
LeanTauCeti.W1p0.hasWeakFDerivOn_indicator
Used by 1
Used byDe Giorgi's theorem: Hölder continuity of weak solutions

TheoremThe borderline Sobolev inequality on W^{1,n}_0(Ω)#

Let n be the dimension and ω = μ(B(0, 1)). If Ω has finite measure, then every u ∈ W^{1,n}_0(Ω) lies in L^q(Ω) for every finite q ≥ n, with

‖u‖_{L^q} ≤ n⁻¹ ω ^ (-1/n) (q (1 - 1/n) + 1) ^ (1 - 1/n + 1/q) μ(Ω) ^ (1/q) ‖∇u‖_{Lⁿ}.

No regularity of Ω is assumed.

TauCeti.W1p.eLpNorm_value_le_mul_measure_rpow_mul_enorm_gradient.{u_1} {E : Type u_1}
  [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p = ↑(Module.finrank ℝ E))
  (hOmega : mu ↑Omega ≠ ⊤) {q : NNReal} (hq : ↑(Module.finrank ℝ E) ≤ q)
  {u : ↥(TauCeti.W1p mu Omega p)} (hu : u ∈ TauCeti.w1p0Submodule mu Omega p) :
  MeasureTheory.eLpNorm (↑↑(TauCeti.W1p.value u)) (↑q) (mu.restrict ↑Omega) ≤
    ENNReal.ofReal
          ((↑(Module.finrank ℝ E))⁻¹ * mu.real (Metric.ball 0 1) ^ (-(↑(Module.finrank ℝ E))⁻¹) *
            (↑q * (1 - (↑(Module.finrank ℝ E))⁻¹) + 1) ^ (1 - (↑(Module.finrank ℝ E))⁻¹ + (↑q)⁻¹)) *
        mu ↑Omega ^ (↑q)⁻¹ *
      ‖TauCeti.W1p.gradient u‖ₑ
Lean

Formalized in Tau Ceti as TauCeti.W1p.eLpNorm_value_le_mul_measure_rpow_mul_enorm_gradient.

Other forms

The borderline Sobolev inequality for compactly supported functions. Formalized in Tau Ceti as TauCeti.eLpNorm_le_mul_measure_rpow_mul_eLpNorm_fderiv.

TauCeti.eLpNorm_le_mul_measure_rpow_mul_eLpNorm_fderiv.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E]
  [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F]
  {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → F} {Ω : Set E} (hu : ContDiff ℝ 1 u)
  (h2u : HasCompactSupport u) (hsupp : tsupport u ⊆ Ω) {q : NNReal}
  (hq : ↑(Module.finrank ℝ E) ≤ q) :
  MeasureTheory.eLpNorm u (↑q) μ ≤
    ENNReal.ofReal
          ((↑(Module.finrank ℝ E))⁻¹ * μ.real (Metric.ball 0 1) ^ (-(↑(Module.finrank ℝ E))⁻¹) *
            (↑q * (1 - (↑(Module.finrank ℝ E))⁻¹) + 1) ^ (1 - (↑(Module.finrank ℝ E))⁻¹ + (↑q)⁻¹)) *
        μ Ω ^ (↑q)⁻¹ *
      MeasureTheory.eLpNorm (fderiv ℝ u) (↑(Module.finrank ℝ E)) μ
Sources
LeanTauCeti.W1p.eLpNorm_value_le_mul_measure_rpow_mul_enorm_gradient · TauCeti.eLpNorm_le_mul_measure_rpow_mul_eLpNorm_fderiv
Uses 1 · Used by 1
Proof usesThe Sobolev inequality on W^{1,p}_0 of a ball
Used byTrudinger's inequality on W^{1,n}_0(Ω)

TheoremDe Giorgi's isoperimetric inequality#

Let Ω be a bounded convex open set in a finite-dimensional real inner product space of dimension n, let u ∈ W^{1,p}(Ω) with 1 ≤ p ≤ ∞, and let k < l. Then, all sets being taken inside Ω,

(l - k) · |{u ≥ l}| · |{u ≤ k}| ≤ μ(B(0, 1)) · (diam Ω) ^ (n + 1) · ∫_{k < u < l} |∇u|.

A function that is both ≤ k and ≥ l on sets of positive measure must have a weak gradient of definite L¹ mass on the strip {k < u < l}.

TauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_convex.{u_1} {E : Type u_1}
  [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hconv : Convex ℝ ↑Omega)
  (hb : Bornology.IsBounded ↑Omega) (u : ↥(TauCeti.W1p mu Omega p)) {k l : ℝ} (hkl : k < l) :
  (l - k) * (mu.restrict ↑Omega).real {x | l ≤ ↑↑(TauCeti.W1p.value u) x} *
      (mu.restrict ↑Omega).real {x | ↑↑(TauCeti.W1p.value u) x ≤ k} ≤
    mu.real (Metric.ball 0 1) * Metric.diam ↑Omega ^ (Module.finrank ℝ E + 1) *
      ∫ (x : E) in {x | k < ↑↑(TauCeti.W1p.value u) x ∧ ↑↑(TauCeti.W1p.value u) x < l},
        ‖↑↑(TauCeti.W1p.gradient u) x‖ ∂mu.restrict ↑Omega
Lean

Formalized in Tau Ceti as TauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_convex.

Other forms

De Giorgi's isoperimetric inequality on a ball. Formalized in Tau Ceti as TauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_eq_ball.

TauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_eq_ball.{u_1} {E : Type u_1}
  [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {c : E} {R : ℝ} (hR : 0 ≤ R)
  (hOmega : ↑Omega = Metric.ball c R) (u : ↥(TauCeti.W1p mu Omega p)) {k l : ℝ} (hkl : k < l) :
  (l - k) * (mu.restrict ↑Omega).real {x | l ≤ ↑↑(TauCeti.W1p.value u) x} *
      (mu.restrict ↑Omega).real {x | ↑↑(TauCeti.W1p.value u) x ≤ k} ≤
    mu.real (Metric.ball 0 1) * (2 * R) ^ (Module.finrank ℝ E + 1) *
      ∫ (x : E) in {x | k < ↑↑(TauCeti.W1p.value u) x ∧ ↑↑(TauCeti.W1p.value u) x < l},
        ‖↑↑(TauCeti.W1p.gradient u) x‖ ∂mu.restrict ↑Omega

De Giorgi's isoperimetric inequality on a ball contained in the Sobolev domain. Formalized in Tau Ceti as TauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_ball_subset.

TauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_ball_subset.{u_1} {E : Type u_1}
  [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {c : E} {R : ℝ} (hR : 0 ≤ R)
  (hball : Metric.ball c R ⊆ ↑Omega) (u : ↥(TauCeti.W1p mu Omega p)) {k l : ℝ} (hkl : k < l) :
  (l - k) * (mu.restrict (Metric.ball c R)).real {x | l ≤ ↑↑(TauCeti.W1p.value u) x} *
      (mu.restrict (Metric.ball c R)).real {x | ↑↑(TauCeti.W1p.value u) x ≤ k} ≤
    mu.real (Metric.ball 0 1) * (2 * R) ^ (Module.finrank ℝ E + 1) *
      ∫ (x : E) in {x | k < ↑↑(TauCeti.W1p.value u) x ∧ ↑↑(TauCeti.W1p.value u) x < l},
        ‖↑↑(TauCeti.W1p.gradient u) x‖ ∂mu.restrict (Metric.ball c R)

De Giorgi's isoperimetric inequality, squared form. Formalized in Tau Ceti as TauCeti.W1p.sq_sub_mul_measureReal_mul_measureReal_le_of_ball_subset.

TauCeti.W1p.sq_sub_mul_measureReal_mul_measureReal_le_of_ball_subset.{u_1} {E : Type u_1}
  [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens E} {c : E} {R : ℝ} (hR : 0 ≤ R) (hball : Metric.ball c R ⊆ ↑Omega)
  (u : ↥(TauCeti.W1p mu Omega 2)) {k l : ℝ} (hkl : k < l)
  (hwLp :
    MeasureTheory.MemLp (fun x => max (↑↑(TauCeti.W1p.value u) x - k) 0) 2 (mu.restrict ↑Omega)) :
  ((l - k) * (mu.restrict (Metric.ball c R)).real {x | l ≤ ↑↑(TauCeti.W1p.value u) x} *
        (mu.restrict (Metric.ball c R)).real {x | ↑↑(TauCeti.W1p.value u) x ≤ k}) ^
      2 ≤
    (mu.real (Metric.ball 0 1) * (2 * R) ^ (Module.finrank ℝ E + 1)) ^ 2 *
        (mu.restrict (Metric.ball c R)).real
          {x | k < ↑↑(TauCeti.W1p.value u) x ∧ ↑↑(TauCeti.W1p.value u) x < l} *
      ∫ (x : E) in Metric.ball c R,
        ‖↑↑(TauCeti.W1p.gradient
                    (TauCeti.W1p.posPartAboveOfMemLp
                      TauCeti.W1p.sq_sub_mul_measureReal_mul_measureReal_le_of_ball_subset._proof_1
                      k u hwLp))
              x‖ ^
          2 ∂mu
Sources
LeanTauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_convex · TauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_eq_ball · TauCeti.W1p.sub_mul_measureReal_mul_measureReal_le_of_ball_subset · TauCeti.W1p.sq_sub_mul_measureReal_mul_measureReal_le_of_ball_subset
Uses 2 · Used by 1
Proof usesThe Poincaré–Wirtinger inequality on a ball · TauCeti.Wkp
Used byDe Giorgi's interior oscillation estimate

TheoremThe divergence theorem on a half-space (TauCeti.setIntegral_normalHalfSpace_fderiv_apply)#

For a compactly supported C¹ function g on ℝ × E and a direction v, the integral of the directional derivative ∂_v g over the half-space {x | a < x.fst} is the boundary integral of g over {a} × E, weighted by ⟪v, -e₁⟫ = -v.fst, the normal component of v along the outward unit normal.

TauCeti.setIntegral_normalHalfSpace_fderiv_apply.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {g : WithLp 2 (ℝ × E) → ℝ} (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (a : ℝ)
  (v : WithLp 2 (ℝ × E)) :
  ∫ (x : WithLp 2 (ℝ × E)) in ↑(TauCeti.normalHalfSpace a), (fderiv ℝ g x) v =
    -(v.fst * ∫ (y : E), g (WithLp.toLp 2 (a, y)))
Lean

Formalized in Tau Ceti as TauCeti.setIntegral_normalHalfSpace_fderiv_apply.

Sources
LeanTauCeti.setIntegral_normalHalfSpace_fderiv_apply
Used by 1
Used byThe divergence theorem on a half-space (TauCeti.setIntegral_setOf_inner_lt_trace_fderiv)

TheoremThe du Bois-Reymond lemma for weak derivatives#

A function whose weak derivative on Ioo a b is 0 is almost everywhere equal to a constant on Ioo a b.

TauCeti.HasWeakLineDerivOn.exists_ae_eq_const.{u_1} {F : Type u_1} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {a b : ℝ} {u : ℝ → F}
  (h :
    TauCeti.HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u 0
      1) :
  ∃ c, u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] fun x => c
Lean

Formalized in Tau Ceti as TauCeti.HasWeakLineDerivOn.exists_ae_eq_const.

Sources
LeanTauCeti.HasWeakLineDerivOn.exists_ae_eq_const
Uses 1 · Used by 1
Proof usesThe du Bois-Reymond lemma
Used byThe fundamental theorem of calculus for weak derivatives

TheoremExtension theorem for bounded Lipschitz domains#

There is a bounded linear extension from W^{1,p}(Ω) to the whole space, and restriction to Ω recovers the original function. Both endpoint exponents p = 1 and p = ∞ are included.

TauCeti.W1p.exists_extensionL_of_isLipschitzDomainWith.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {Ω : TopologicalSpace.Opens (WithLp 2 (ℝ × E))} {L : NNReal} {p : ENNReal} [Fact (1 ≤ p)]
  (hΩ : (↑Ω).IsLipschitzDomainWith L) (hb : Bornology.IsBounded ↑Ω) :
  ∃ T,
    TauCeti.W1p.restrictL ⋯ ∘SL T = ContinuousLinearMap.id ℝ ↥(TauCeti.W1p MeasureTheory.volume Ω p)
Lean

Formalized in Tau Ceti as TauCeti.W1p.exists_extensionL_of_isLipschitzDomainWith.

Sources
LeanTauCeti.W1p.exists_extensionL_of_isLipschitzDomainWith
Uses 1 · Used by 2
Proof usesRademacher's theorem for locally Lipschitz functions
Used byRellich–Kondrachov on bounded Lipschitz domains · The Sobolev inequality on W^{1,p}_0 of a ball

TheoremThe fundamental theorem of calculus for a continuous representative#

Let u' be the weak derivative of u on Ioo a b, integrable on Ioo a b, and let v be continuous on Icc a b and equal to u almost everywhere on Ioo a b. Then ∫ r in s..t, u' r = v t - v s for all s, t ∈ Icc a b.

TauCeti.HasWeakLineDerivOn.integral_eq_sub.{u_1} {F : Type u_1} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {a b : ℝ} {u u' v : ℝ → F}
  (h :
    TauCeti.HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u'
      1)
  (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume)
  (hv : ContinuousOn v (Set.Icc a b)) (hae : u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] v)
  {s t : ℝ} (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : ∫ (r : ℝ) in s..t, u' r = v t - v s
Lean

Formalized in Tau Ceti as TauCeti.HasWeakLineDerivOn.integral_eq_sub.

Sources
LeanTauCeti.HasWeakLineDerivOn.integral_eq_sub
Uses 1 · Used by 2
Proof usesThe fundamental theorem of calculus for weak derivatives
Used byExistence of weak solutions for linear parabolic equations · The Benamou–Brenier lower bound

TheoremThe fundamental theorem of calculus for weak derivatives#

If u' is the weak derivative of u on Ioo a b and t₀ ∈ Ioo a b, then u is almost everywhere on Ioo a b equal to a constant plus the primitive t ↦ ∫ s in t₀..t, u' s.

TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] {a b t₀ : ℝ} {u u' : ℝ → F}
  (h :
    TauCeti.HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u'
      1)
  (ht₀ : t₀ ∈ Set.Ioo a b) :
  ∃ c, u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] fun t => c + ∫ (s : ℝ) in t₀..t, u' s
Lean

Formalized in Tau Ceti as TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral.

Other forms

The fundamental theorem of calculus for weak derivatives, from the left endpoint. Formalized in Tau Ceti as TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_left.

TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_left.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] {a b : ℝ} {u u' : ℝ → F}
  (h :
    TauCeti.HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ } u u'
      1)
  (hu' : MeasureTheory.IntegrableOn u' (Set.Ioo a b) MeasureTheory.volume) :
  ∃ c, u =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] fun t => c + ∫ (s : ℝ) in a..t, u' s
Sources
LeanTauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral · TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_left
Uses 1 · Used by 3
Proof usesThe du Bois-Reymond lemma for weak derivatives
Used byExistence of weak solutions for linear parabolic equations · The fundamental theorem of calculus for a continuous representative · The fundamental theorem of calculus for weak derivatives on the line

TheoremThe fundamental theorem of calculus for weak derivatives on the line#

If u' is the weak derivative of u on all of ℝ, then u is almost everywhere equal to a constant plus the primitive t ↦ ∫ s in t₀..t, u' s, for any base point t₀.

TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_top.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] {u u' : ℝ → F}
  (h : TauCeti.HasWeakLineDerivOn MeasureTheory.volume ⊤ u u' 1) (t₀ : ℝ) :
  ∃ c, u =ᵐ[MeasureTheory.volume] fun t => c + ∫ (s : ℝ) in t₀..t, u' s
Lean

Formalized in Tau Ceti as TauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_top.

Sources
LeanTauCeti.HasWeakLineDerivOn.exists_ae_eq_add_intervalIntegral_top
Uses 1 · Used by 1
Proof usesThe fundamental theorem of calculus for weak derivatives
Used byThe index of the trajectory operator is a difference of Morse indices

TheoremThe Gagliardo--Nirenberg--Sobolev inequality on W^{1,p}(E)#

The image of u under the whole-space Sobolev embedding is bounded in L^{p⋆} by the Lᵖ norm of the gradient of u alone, with Mathlib's constant MeasureTheory.SNormLESNormFDerivOfEqConst.

TauCeti.W1p.norm_sobolevEmbeddingTopL_le.{u_1} {E : Type u_1} [MeasurableSpace E]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p pstar : ENNReal} [Fact (1 ≤ p)]
  (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Module.finrank ℝ E))⁻¹ = p⁻¹)
  (u : ↥(TauCeti.W1p mu ⊤ p)) :
  ‖(TauCeti.W1p.sobolevEmbeddingTopL hpstar hexp) u‖ ≤
    ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ mu p.toReal) * ‖TauCeti.W1p.gradient u‖
Lean

Formalized in Tau Ceti as TauCeti.W1p.norm_sobolevEmbeddingTopL_le.

Other forms

The Gagliardo--Nirenberg--Sobolev inequality between test-function classes. Formalized in Tau Ceti as TauCeti.norm_testFunctionLp_le_mul_norm_gradientTestFunctionLp.

TauCeti.norm_testFunctionLp_le_mul_norm_gradientTestFunctionLp.{u_1} {E : Type u_1}
  [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {pstar : ENNReal}
  (hpstar : pstar ≠ ⊤) (hexp : pstar⁻¹ + (↑(Module.finrank ℝ E))⁻¹ = p⁻¹)
  (phi : TestFunction Omega ℝ ⊤) :
  ‖TauCeti.testFunctionLp pstar phi‖ ≤
    ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ mu p.toReal) *
      ‖TauCeti.gradientTestFunctionLp p phi‖

The Gagliardo--Nirenberg--Sobolev inequality on D^{1,p}_0(Ω). Formalized in Tau Ceti as TauCeti.D1p0.norm_sobolevEmbeddingL_le.

TauCeti.D1p0.norm_sobolevEmbeddingL_le.{u_1} {E : Type u_1} [MeasurableSpace E]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  {mu : MeasureTheory.Measure E} {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)]
  [mu.IsAddHaarMeasure] {pstar : ENNReal} (hpstar : pstar ≠ ⊤)
  (hexp : pstar⁻¹ + (↑(Module.finrank ℝ E))⁻¹ = p⁻¹) (u : ↥(TauCeti.D1p0 mu Omega p)) :
  ‖(TauCeti.D1p0.sobolevEmbeddingL hexp) u‖ ≤
    ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ mu p.toReal) * ‖u‖

The Gagliardo--Nirenberg--Sobolev inequality on W^{1,p}_0(Ω). Formalized in Tau Ceti as TauCeti.W1p.eLpNorm_value_le_mul_enorm_gradient.

TauCeti.W1p.eLpNorm_value_le_mul_enorm_gradient.{u_1} {E : Type u_1} [MeasurableSpace E]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E}
  {p : ENNReal} [Fact (1 ≤ p)] {pstar : ENNReal} (hpstar : pstar ≠ ⊤)
  (hexp : pstar⁻¹ + (↑(Module.finrank ℝ E))⁻¹ = p⁻¹) {u : ↥(TauCeti.W1p mu Omega p)}
  (hu : u ∈ TauCeti.w1p0Submodule mu Omega p) :
  MeasureTheory.eLpNorm (↑↑(TauCeti.W1p.value u)) pstar (mu.restrict ↑Omega) ≤
    ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ mu p.toReal) * ‖TauCeti.W1p.gradient u‖ₑ
Sources
LeanTauCeti.W1p.norm_sobolevEmbeddingTopL_le · TauCeti.norm_testFunctionLp_le_mul_norm_gradientTestFunctionLp · TauCeti.D1p0.norm_sobolevEmbeddingL_le · TauCeti.W1p.eLpNorm_value_le_mul_enorm_gradient
Used by 2
Used byThe interior Sobolev inequality · The Sobolev inequality on W^{1,p}_0 of a ball

TheoremGreen's second identity against a test function#

For u of class C² on the open set Ω and a test function φ on Ω, ∫ Δφ • u ∂μ = ∫ φ • Δu ∂μ: the classical Laplacian of a C² function is its distributional Laplacian.

ContDiffOn.integral_laplacian_smul_eq_integral_smul_laplacian.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
  {Ω : TopologicalSpace.Opens E} {u : E → F} [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure]
  (hu : ContDiffOn ℝ 2 u ↑Ω) (φ : TestFunction Ω ℝ ⊤) :
  ∫ (x : E), Laplacian.laplacian (⇑φ) x • u x ∂μ = ∫ (x : E), φ x • Laplacian.laplacian u x ∂μ
Lean

Formalized in Tau Ceti as ContDiffOn.integral_laplacian_smul_eq_integral_smul_laplacian.

Sources
LeanContDiffOn.integral_laplacian_smul_eq_integral_smul_laplacian
Used by 7
Used byThe Lipschitz bound for bounded harmonic functions · Weyl's lemma for continuous functions · Green's first identity against H¹₀(Ω) · The interior Schauder estimate on small balls · The limit in Harnack's convergence theorem is harmonic · The local Harnack inequality · Perron's theorem

TheoremThe interior Sobolev inequality#

If V has compact closure contained in the open set Ω, 1 ≤ p and 1/p⋆ + 1/n = 1/p with p⋆ < ∞, then for every q ≤ p⋆ there is a constant C with ‖u‖_{L^q(V)} ≤ C ‖u‖_{W^{1,p}(Ω)} for all u ∈ W^{1,p}(Ω). The full Sobolev norm is needed on the right: on a bounded Ω, a nonzero constant has vanishing gradient.

TauCeti.W1p.exists_eLpNorm_value_le_of_isCompact_closure.{u_1} {E : Type u_1} [MeasurableSpace E]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E}
  {p pstar : ENNReal} [Fact (1 ≤ p)] (hpstar : pstar ≠ ⊤)
  (hexp : pstar⁻¹ + (↑(Module.finrank ℝ E))⁻¹ = p⁻¹) {V : Set E} (hVc : IsCompact (closure V))
  (hVO : closure V ⊆ ↑Omega) {q : ENNReal} (hq : q ≤ pstar) :
  ∃ C,
    ∀ (u : ↥(TauCeti.W1p mu Omega p)),
      MeasureTheory.eLpNorm (↑↑(TauCeti.W1p.value u)) q (mu.restrict V) ≤ ↑C * ‖u‖ₑ
Lean

Formalized in Tau Ceti as TauCeti.W1p.exists_eLpNorm_value_le_of_isCompact_closure.

Sources
LeanTauCeti.W1p.exists_eLpNorm_value_le_of_isCompact_closure
Uses 1
Proof usesThe Gagliardo--Nirenberg--Sobolev inequality on W^{1,p}(E)

TheoremJensen's bound for the gradient of a mollification#

If U is a weak derivative field of u on the whole space and rho is a smooth compactly supported probability kernel, then ∫ Φ(‖D(u ⋆ rho)‖) ≤ ∫ Φ(‖U‖) for every Φ convex and monotone on [0, ∞), in extended nonnegative form.

TauCeti.HasWeakFDerivOn.lintegral_ofReal_map_norm_fderiv_convolution_le.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [BorelSpace E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {mu : MeasureTheory.Measure E} [mu.IsAddLeftInvariant]
  [MeasureTheory.SFinite mu] [SecondCountableTopology E] [mu.IsNegInvariant] {u : E → F}
  {U : E → E →L[ℝ] F} (h : TauCeti.HasWeakFDerivOn mu ⊤ u U)
  (hu : MeasureTheory.LocallyIntegrable u mu) (hU : MeasureTheory.LocallyIntegrable U mu)
  {Φ : ℝ → ℝ} (hΦ : ConvexOn ℝ (Set.Ici 0) Φ) (hΦm : MonotoneOn Φ (Set.Ici 0)) {rho : E → ℝ}
  (hrho : ContDiff ℝ (↑⊤) rho) (hrho_cpt : HasCompactSupport rho) (hrho0 : 0 ≤ᵐ[mu] rho)
  (hrho1 : ∫ (x : E), rho x ∂mu = 1) :
  ∫⁻ (x : E),
      ENNReal.ofReal
        (Φ
          ‖fderiv ℝ (MeasureTheory.convolution u rho (ContinuousLinearMap.lsmul ℝ ℝ).flip mu)
              x‖) ∂mu ≤
    ∫⁻ (x : E), ENNReal.ofReal (Φ ‖U x‖) ∂mu
Lean

Formalized in Tau Ceti as TauCeti.HasWeakFDerivOn.lintegral_ofReal_map_norm_fderiv_convolution_le.

Sources
LeanTauCeti.HasWeakFDerivOn.lintegral_ofReal_map_norm_fderiv_convolution_le
Uses 1
Proof usesJensen's inequality for convolution

TheoremThe local Morrey inequality#

Let n < p ≤ ∞, where n is the dimension, and let α = 1 - n / p. There is a constant C > 0, depending only on n, p and the Haar measure μ, such that the following holds. Let u ∈ W^{1,p}(Ω) and let x, y be points with closedBall x (2 |x - y|) ⊆ Ω. Then the precise representative u* of u satisfies

|u*(x) - u*(y)| ≤ C ‖∇u‖_{Lᵖ(B(x, 2 |x - y|))} |x - y|^α.

TauCeti.W1p.exists_dist_preciseRepresentative_le.{u_1} {E : Type u_1} [MeasurableSpace E]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)]
  (hp : ↑(Module.finrank ℝ E) < p) :
  ∃ C,
    0 < C ∧
      ∀ {Omega : TopologicalSpace.Opens E} (u : ↥(TauCeti.W1p mu Omega p)) {x y : E},
        Metric.closedBall x (2 * dist x y) ⊆ ↑Omega →
          dist (TauCeti.MeasureTheory.preciseRepresentative mu (↑↑(TauCeti.W1p.value u)) x)
              (TauCeti.MeasureTheory.preciseRepresentative mu (↑↑(TauCeti.W1p.value u)) y) ≤
            C *
                (MeasureTheory.eLpNorm (↑↑(TauCeti.W1p.gradient u)) p
                    (mu.restrict (Metric.ball x (2 * dist x y)))).toReal *
              dist x y ^ ↑(1 - ↑(Module.finrank ℝ E) / p).toNNReal
Lean

Formalized in Tau Ceti as TauCeti.W1p.exists_dist_preciseRepresentative_le.

Sources
LeanTauCeti.W1p.exists_dist_preciseRepresentative_le
Uses 1
Proof usesThe pointwise Morrey estimate

TheoremMeyers–Serrin: H = W in W^{k,p}(Ω)#

For 1 ≤ p < ∞, every order k and an arbitrary open set Ω, the elements of W^{k,p}(Ω) represented by functions smooth on Ω are dense in W^{k,p}(Ω), in the full Sobolev norm.

TauCeti.Wkp.dense_contDiffOn_representatives.{u_1} {E : Type u_1} [MeasurableSpace E]
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E}
  {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (k : ℕ) :
  Dense {u | ∃ f, ContDiffOn ℝ (↑⊤) f ↑Omega ∧ ↑↑(TauCeti.Wkp.value k u) =ᵐ[mu.restrict ↑Omega] f}
Lean

Formalized in Tau Ceti as TauCeti.Wkp.dense_contDiffOn_representatives.

Sources
LeanTauCeti.Wkp.dense_contDiffOn_representatives
Uses 1 · Used by 2
Statement usesTauCeti.Wkp
Used byThe Calderón–Zygmund estimate ‖D²u‖_p ≤ C ‖Δu‖_p · The interior Schauder estimate on small balls

TheoremThe Morrey potential estimate for the mean#

If u is C¹ on an open set Ω which is star-convex about x and contained in closedBall x D, and p exceeds the dimension n of the space, then for every S ⊆ Ω of positive measure the deviation of u x from the mean of u over S is at most D ^ n / (n μ(S)) * K ^ (1 - 1 / p) * D ^ (1 - n / p) times the Lᵖ(Ω) norm of the derivative of u, where K = n μ(B(0, 1)) (p - 1) / (p - n).

TauCeti.enorm_sub_setAverage_le_of_starConvex_of_finrank_lt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E}
  [μ.IsAddHaarMeasure] {u : E → F} {Ω S : Set E} {x : E} {D : ℝ} {p : NNReal} [CompleteSpace F]
  (hΩ : IsOpen Ω) (hu : ContDiffOn ℝ 1 u Ω) (hx : StarConvex ℝ x Ω) (hD : Ω ⊆ Metric.closedBall x D)
  (hS : S ⊆ Ω) (hS₀ : μ S ≠ 0) (hp : ↑(Module.finrank ℝ E) < p) :
  ‖u x - ⨍ (y : E) in S, u y ∂μ‖ₑ ≤
    ENNReal.ofReal (D ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E)) / μ S *
        ENNReal.ofReal
          ((↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1) * (↑p - 1) /
                (↑p - ↑(Module.finrank ℝ E))) ^
              (1 - 1 / ↑p) *
            D ^ (1 - ↑(Module.finrank ℝ E) / ↑p)) *
      MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) (μ.restrict Ω)
Lean

Formalized in Tau Ceti as TauCeti.enorm_sub_setAverage_le_of_starConvex_of_finrank_lt.

Other forms

The Morrey potential estimate on a convex domain. Formalized in Tau Ceti as TauCeti.enorm_sub_setAverage_le_of_convex_of_finrank_lt.

TauCeti.enorm_sub_setAverage_le_of_convex_of_finrank_lt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E}
  [μ.IsAddHaarMeasure] {u : E → F} {Ω S : Set E} {x : E} {p : NNReal} [CompleteSpace F]
  (hΩ : IsOpen Ω) (hΩc : Convex ℝ Ω) (hb : Bornology.IsBounded Ω) (hu : ContDiffOn ℝ 1 u Ω)
  (hx : x ∈ Ω) (hS : S ⊆ Ω) (hS₀ : μ S ≠ 0) (hp : ↑(Module.finrank ℝ E) < p) :
  ‖u x - ⨍ (y : E) in S, u y ∂μ‖ₑ ≤
    ENNReal.ofReal (Metric.diam Ω ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E)) / μ S *
        ENNReal.ofReal
          ((↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1) * (↑p - 1) /
                (↑p - ↑(Module.finrank ℝ E))) ^
              (1 - 1 / ↑p) *
            Metric.diam Ω ^ (1 - ↑(Module.finrank ℝ E) / ↑p)) *
      MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) (μ.restrict Ω)
Sources
LeanTauCeti.enorm_sub_setAverage_le_of_starConvex_of_finrank_lt · TauCeti.enorm_sub_setAverage_le_of_convex_of_finrank_lt
Used by 1
Used byMorrey's inequality

TheoremMorrey's Dirichlet growth theorem#

Let u ∈ W^{1,p}(Ω) and α > 0, and let K be a set of diameter at most R whose closed 2R-thickening lies in Ω. If the gradient of u satisfies the growth condition

∫_{B(x, r)} ‖∇u‖ ≤ M r^(n - 1 + α) for every x ∈ K and 0 < r ≤ 2R,

then the precise representative of u is α-Hölder continuous on K, with Hölder constant 2 · 2^α · 2ⁿ / (1 - 2^(-α)) · 2^(n + 1) / ω · M, where ω is the measure of the unit ball.

TauCeti.W1p.holderOnWith_preciseRepresentative_of_setIntegral_norm_gradient_le.{u_1} {E : Type u_1}
  [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {α : NNReal} (hα : 0 < α)
  {M R : ℝ} (u : ↥(TauCeti.W1p mu Omega p)) {K : Set E} (hKR : ∀ x ∈ K, ∀ y ∈ K, dist x y ≤ R)
  (hK : Metric.cthickening (2 * R) K ⊆ ↑Omega)
  (hgrowth :
    ∀ x ∈ K,
      ∀ (r : ℝ),
        0 < r →
          r ≤ 2 * R →
            ∫ (z : E) in Metric.ball x r, ‖↑↑(TauCeti.W1p.gradient u) z‖ ∂mu ≤
              M * r ^ (↑(Module.finrank ℝ E) - 1 + ↑α)) :
  HolderOnWith
    (2 * 2 ^ ↑α * (2 ^ Module.finrank ℝ E / (1 - 2 ^ (-↑α))) *
        (2 ^ (Module.finrank ℝ E + 1) / mu.real (Metric.ball 0 1) * M)).toNNReal
    α (TauCeti.MeasureTheory.preciseRepresentative mu ↑↑(TauCeti.W1p.value u)) K
Lean

Formalized in Tau Ceti as TauCeti.W1p.holderOnWith_preciseRepresentative_of_setIntegral_norm_gradient_le.

Other forms

Morrey's Dirichlet growth theorem on the whole space. Formalized in Tau Ceti as TauCeti.W1p.holderWith_preciseRepresentative_of_setIntegral_norm_gradient_le.

TauCeti.W1p.holderWith_preciseRepresentative_of_setIntegral_norm_gradient_le.{u_1} {E : Type u_1}
  [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)]
  {α : NNReal} (hα : 0 < α) {M : ℝ} (u : ↥(TauCeti.W1p mu ⊤ p))
  (hgrowth :
    ∀ (x : E) (r : ℝ),
      0 < r →
        ∫ (z : E) in Metric.ball x r, ‖↑↑(TauCeti.W1p.gradient u) z‖ ∂mu ≤
          M * r ^ (↑(Module.finrank ℝ E) - 1 + ↑α)) :
  HolderWith
    (2 * 2 ^ ↑α * (2 ^ Module.finrank ℝ E / (1 - 2 ^ (-↑α))) *
        (2 ^ (Module.finrank ℝ E + 1) / mu.real (Metric.ball 0 1) * M)).toNNReal
    α (TauCeti.MeasureTheory.preciseRepresentative mu ↑↑(TauCeti.W1p.value u))
Sources
LeanTauCeti.W1p.holderOnWith_preciseRepresentative_of_setIntegral_norm_gradient_le · TauCeti.W1p.holderWith_preciseRepresentative_of_setIntegral_norm_gradient_le
Uses 1
Proof usesThe pointwise Morrey estimate

TheoremMorrey's inequality#

If u is C¹ on the whole space and p exceeds the dimension n of the space, then ‖u x - u y‖ is at most 2 ^ (n + 1) / (n ω) * K ^ (1 - 1 / p) * (2 ‖x - y‖) ^ (1 - n / p) times the Lᵖ norm of the derivative of u, where ω = μ(B(0, 1)) and K = n ω (p - 1) / (p - n).

TauCeti.enorm_sub_le_of_contDiff_of_finrank_lt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E}
  [μ.IsAddHaarMeasure] {u : E → F} {p : NNReal} [CompleteSpace F] (hu : ContDiff ℝ 1 u) (x y : E)
  (hp : ↑(Module.finrank ℝ E) < p) :
  ‖u x - u y‖ₑ ≤
    ENNReal.ofReal
        (2 ^ (Module.finrank ℝ E + 1) / (↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1)) *
            (↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1) * (↑p - 1) /
                (↑p - ↑(Module.finrank ℝ E))) ^
              (1 - 1 / ↑p) *
          (2 * ‖x - y‖) ^ (1 - ↑(Module.finrank ℝ E) / ↑p)) *
      MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
Lean

Formalized in Tau Ceti as TauCeti.enorm_sub_le_of_contDiff_of_finrank_lt.

Other forms

Morrey's inequality on a ball. Formalized in Tau Ceti as TauCeti.enorm_sub_le_of_mem_ball_of_finrank_lt.

TauCeti.enorm_sub_le_of_mem_ball_of_finrank_lt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E}
  [μ.IsAddHaarMeasure] {u : E → F} {p : NNReal} [CompleteSpace F] {z : E} {r : ℝ}
  (hu : ContDiffOn ℝ 1 u (Metric.ball z r)) {x y : E} (hx : x ∈ Metric.ball z r)
  (hy : y ∈ Metric.ball z r) (hp : ↑(Module.finrank ℝ E) < p) :
  ‖u x - u y‖ₑ ≤
    ENNReal.ofReal
        (2 ^ (Module.finrank ℝ E + 1) / (↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1)) *
            (↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1) * (↑p - 1) /
                (↑p - ↑(Module.finrank ℝ E))) ^
              (1 - 1 / ↑p) *
          (2 * r) ^ (1 - ↑(Module.finrank ℝ E) / ↑p)) *
      MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) (μ.restrict (Metric.ball z r))

Morrey's inequality, Hölder form. Formalized in Tau Ceti as TauCeti.holderWith_of_contDiff_of_finrank_lt.

TauCeti.holderWith_of_contDiff_of_finrank_lt.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E}
  [μ.IsAddHaarMeasure] {u : E → F} {p : NNReal} [CompleteSpace F] (hu : ContDiff ℝ 1 u)
  (hp : ↑(Module.finrank ℝ E) < p) (hDu : MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ ≠ ⊤) :
  HolderWith
    ((2 ^ (Module.finrank ℝ E + 1) / (↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1)) *
            (↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1) * (↑p - 1) /
                (↑p - ↑(Module.finrank ℝ E))) ^
              (1 - 1 / ↑p) *
          2 ^ (1 - ↑(Module.finrank ℝ E) / ↑p)).toNNReal *
      (MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ).toNNReal)
    (1 - ↑(Module.finrank ℝ E) / p) u
Sources
LeanTauCeti.enorm_sub_le_of_contDiff_of_finrank_lt · TauCeti.enorm_sub_le_of_mem_ball_of_finrank_lt · TauCeti.holderWith_of_contDiff_of_finrank_lt
Uses 1 · Used by 1
Proof usesThe Morrey potential estimate for the mean
Used byThe supercritical Sobolev multiplication estimate

TheoremNo Poincaré inequality holds on the whole space#

There is no constant C with ‖u‖_p ≤ C ‖Du‖_p for every compactly supported Cᵏ function u, for any order k ≤ ∞ and any p ≠ 0, including p = ∞. In particular, the inequality fails even when restricted to smooth test functions.

Compare MeasureTheory.eLpNorm_le_eLpNorm_fderiv, which supplies such a constant once every u is supported in one fixed bounded set; the proof here shows that hypothesis cannot be dropped.

TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {p : ENNReal} {k : ℕ∞} (hp₀ : p ≠ 0) :
  ¬∃ C,
      ∀ (u : E → ℝ),
        ContDiff ℝ (↑k) u →
          HasCompactSupport u →
            MeasureTheory.eLpNorm u p μ ≤ ↑C * MeasureTheory.eLpNorm (fderiv ℝ u) p μ
Lean

Formalized in Tau Ceti as TauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv.

Sources
LeanTauCeti.not_exists_eLpNorm_le_const_mul_eLpNorm_fderiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.