The Caccioppoli inequality to The local Harnack inequality

TheoremThe Caccioppoli inequality#

Let a be measurable and uniformly elliptic on Ω with constants 0 < λ ≤ Λ, and let u ∈ H¹(Ω) be a weak solution of -∂ᵢ(aⁱʲ ∂ⱼu) = f in Ω, in the sense that a(u, v) = ∫_Ω f v for every v ∈ H¹₀(Ω), with no boundary condition on u. Then for every smooth ψ compactly supported in Ω,

∫_Ω ψ² ‖∇u‖² ≤ (2Λ/λ)² ∫_Ω ‖∇ψ‖² u² + (2/λ) ∫_Ω ψ² f u.

For f = 0 the last term vanishes, and the gradient of u where ψ = 1 is bounded by u itself on the support of ψ.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_le.{u_1} {ι : Type u_1}
  [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {lam Lam : ℝ} [DecidableEq ι] (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  {f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))} {u : ↥(TauCeti.W1p mu Omega 2)}
  (hu :
    ∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
      TauCeti.PDE.energyFormH1 a 0 0 u ↑v =
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ↑↑f x * ↑↑(TauCeti.W1p.value ↑v) x ∂mu)
  {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcpt : HasCompactSupport ψ)
  (hts : tsupport ψ ⊆ ↑Omega) :
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ‖↑↑(TauCeti.W1p.gradient u) x‖ ^ 2 ∂mu ≤
    (2 * Lam / lam) ^ 2 *
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
          ‖gradient ψ x‖ ^ 2 * ↑↑(TauCeti.W1p.value u) x ^ 2 ∂mu +
      2 / lam *
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ↑↑f x * ↑↑(TauCeti.W1p.value u) x ∂mu
Lean

Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_le.

Other forms

The Caccioppoli inequality for a nonnegative-level truncation of a weak subsolution. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
  {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {lam Lam : ℝ}
  (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  {f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))} {u : ↥(TauCeti.W1p mu Omega 2)}
  (hu :
    ∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
      (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value ↑v) x) →
        TauCeti.PDE.energyFormH1 a 0 0 u ↑v ≤
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ↑↑f x * ↑↑(TauCeti.W1p.value ↑v) x ∂mu)
  {k : ℝ} (hk : 0 ≤ k) {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ)
  (hcpt : HasCompactSupport ψ) (hts : tsupport ψ ⊆ ↑Omega) :
  have w :=
    TauCeti.W1p.posPartAbove
      TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_memLp._proof_1
      hk u;
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ‖↑↑(TauCeti.W1p.gradient w) x‖ ^ 2 ∂mu ≤
    (2 * Lam / lam) ^ 2 *
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
          ‖gradient ψ x‖ ^ 2 * ↑↑(TauCeti.W1p.value w) x ^ 2 ∂mu +
      2 / lam *
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ↑↑f x * ↑↑(TauCeti.W1p.value w) x ∂mu

The Caccioppoli inequality for a nonnegative-level truncation of a weak subsolution with lower-order terms. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
  {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
  {c : EuclideanSpace ℝ ι → ℝ} {lam Lam beta gamma : ℝ}
  (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  (hb : MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega))
  (hc : MeasureTheory.AEStronglyMeasurable c (mu.restrict ↑Omega))
  (hb_bound : ∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) (hc_bound : ∀ x ∈ ↑Omega, ‖c x‖ ≤ gamma)
  {f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))} {u : ↥(TauCeti.W1p mu Omega 2)}
  (hu :
    ∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
      (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value ↑v) x) →
        TauCeti.PDE.energyFormH1 a b c u ↑v ≤
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ↑↑f x * ↑↑(TauCeti.W1p.value ↑v) x ∂mu)
  {k : ℝ} (hk : 0 ≤ k) {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ)
  (hcpt : HasCompactSupport ψ) (hts : tsupport ψ ⊆ ↑Omega) :
  have w :=
    TauCeti.W1p.posPartAbove
      TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_memLp._proof_1
      hk u;
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ‖↑↑(TauCeti.W1p.gradient w) x‖ ^ 2 ∂mu ≤
    2 * (2 * Lam / lam) ^ 2 *
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
            ‖gradient ψ x‖ ^ 2 * ↑↑(TauCeti.W1p.value w) x ^ 2 ∂mu +
        (2 * beta / lam) ^ 2 *
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ↑↑(TauCeti.W1p.value w) x ^ 2 ∂mu +
      4 / lam *
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
          ψ x ^ 2 * (↑↑f x - c x * ↑↑(TauCeti.W1p.value u) x) * ↑↑(TauCeti.W1p.value w) x ∂mu

The Caccioppoli inequality for a positive truncation of a weak subsolution. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_memLp.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_memLp.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
  {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {lam Lam : ℝ}
  (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  {f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))} {u : ↥(TauCeti.W1p mu Omega 2)}
  (hu :
    ∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
      (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value ↑v) x) →
        TauCeti.PDE.energyFormH1 a 0 0 u ↑v ≤
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ↑↑f x * ↑↑(TauCeti.W1p.value ↑v) x ∂mu)
  {k : ℝ}
  (hwLp :
    MeasureTheory.MemLp (fun x => max (↑↑(TauCeti.W1p.value u) x - k) 0) 2 (mu.restrict ↑Omega))
  {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcpt : HasCompactSupport ψ)
  (hts : tsupport ψ ⊆ ↑Omega) :
  have w :=
    TauCeti.W1p.posPartAboveOfMemLp
      TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_memLp._proof_1
      k u hwLp;
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ‖↑↑(TauCeti.W1p.gradient w) x‖ ^ 2 ∂mu ≤
    (2 * Lam / lam) ^ 2 *
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
          ‖gradient ψ x‖ ^ 2 * ↑↑(TauCeti.W1p.value w) x ^ 2 ∂mu +
      2 / lam *
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ↑↑f x * ↑↑(TauCeti.W1p.value w) x ∂mu

The Caccioppoli inequality for a positive truncation of a weak subsolution with lower-order terms. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_memLp.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_memLp.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
  {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
  {c : EuclideanSpace ℝ ι → ℝ} {lam Lam beta gamma : ℝ}
  (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  (hb : MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega))
  (hc : MeasureTheory.AEStronglyMeasurable c (mu.restrict ↑Omega))
  (hb_bound : ∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) (hc_bound : ∀ x ∈ ↑Omega, ‖c x‖ ≤ gamma)
  {f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))} {u : ↥(TauCeti.W1p mu Omega 2)}
  (hu :
    ∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
      (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value ↑v) x) →
        TauCeti.PDE.energyFormH1 a b c u ↑v ≤
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ↑↑f x * ↑↑(TauCeti.W1p.value ↑v) x ∂mu)
  {k : ℝ}
  (hwLp :
    MeasureTheory.MemLp (fun x => max (↑↑(TauCeti.W1p.value u) x - k) 0) 2 (mu.restrict ↑Omega))
  {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcpt : HasCompactSupport ψ)
  (hts : tsupport ψ ⊆ ↑Omega) :
  have w :=
    TauCeti.W1p.posPartAboveOfMemLp
      TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_memLp._proof_1
      k u hwLp;
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ‖↑↑(TauCeti.W1p.gradient w) x‖ ^ 2 ∂mu ≤
    2 * (2 * Lam / lam) ^ 2 *
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
            ‖gradient ψ x‖ ^ 2 * ↑↑(TauCeti.W1p.value w) x ^ 2 ∂mu +
        (2 * beta / lam) ^ 2 *
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ↑↑(TauCeti.W1p.value w) x ^ 2 ∂mu +
      4 / lam *
        ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
          ψ x ^ 2 * (↑↑f x - c x * ↑↑(TauCeti.W1p.value u) x) * ↑↑(TauCeti.W1p.value w) x ∂mu

The Caccioppoli inequality for powers of a positive supersolution. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_rpow_mul_norm_gradient_sq_le.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_rpow_mul_norm_gradient_sq_le.{u_1} {ι : Type u_1}
  [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {lam Lam : ℝ} [DecidableEq ι] (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega)) {u : ↥(TauCeti.W1p mu Omega 2)}
  (hu :
    ∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
      (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value ↑v) x) →
        0 ≤ TauCeti.PDE.energyFormH1 a 0 0 u ↑v)
  {ε : ℝ} (hε : 0 < ε)
  (hεu : ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, ε ≤ ↑↑(TauCeti.W1p.value u) x) {p : ℝ}
  (hp : p < 1) {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcpt : HasCompactSupport ψ)
  (hts : tsupport ψ ⊆ ↑Omega) :
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
      ψ x ^ 2 * (↑↑(TauCeti.W1p.value u) x ^ (p - 2) * ‖↑↑(TauCeti.W1p.gradient u) x‖ ^ 2) ∂mu ≤
    (2 * Lam / ((1 - p) * lam)) ^ 2 *
      ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ‖gradient ψ x‖ ^ 2 * ↑↑(TauCeti.W1p.value u) x ^ p ∂mu

The Caccioppoli inequality for the power w = u^{p/2} of a positive supersolution. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_le_of_ae_eq_rpow.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_le_of_ae_eq_rpow.{u_1}
  {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {lam Lam : ℝ} [DecidableEq ι] (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega)) {u : ↥(TauCeti.W1p mu Omega 2)}
  (hu :
    ∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
      (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value ↑v) x) →
        0 ≤ TauCeti.PDE.energyFormH1 a 0 0 u ↑v)
  {ε : ℝ} (hε : 0 < ε)
  (hεu : ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, ε ≤ ↑↑(TauCeti.W1p.value u) x) {p : ℝ}
  (hp : p < 1) {w : ↥(TauCeti.W1p mu Omega 2)}
  (hwv :
    ↑↑(TauCeti.W1p.value w) =ᵐ[mu.restrict ↑Omega] fun x => ↑↑(TauCeti.W1p.value u) x ^ (p / 2))
  (hwg :
    ↑↑(TauCeti.W1p.gradient w) =ᵐ[mu.restrict ↑Omega] fun x =>
      (p / 2 * ↑↑(TauCeti.W1p.value u) x ^ (p / 2 - 1)) • ↑↑(TauCeti.W1p.gradient u) x)
  {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcpt : HasCompactSupport ψ)
  (hts : tsupport ψ ⊆ ↑Omega) :
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ψ x ^ 2 * ‖↑↑(TauCeti.W1p.gradient w) x‖ ^ 2 ∂mu ≤
    (|p| * Lam / ((1 - p) * lam)) ^ 2 *
      ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ‖gradient ψ x‖ ^ 2 * ↑↑(TauCeti.W1p.value w) x ^ 2 ∂mu

The Caccioppoli inequality on concentric balls. Formalized in Tau Ceti as TauCeti.PDE.exists_setIntegral_ball_norm_gradient_posPartAbove_sq_le.

TauCeti.PDE.exists_setIntegral_ball_norm_gradient_posPartAbove_sq_le.{u_1} {ι : Type u_1}
  [Fintype ι] [DecidableEq ι] :
  ∃ c,
    0 < c ∧
      ∀ {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [inst : mu.IsAddHaarMeasure]
        {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
        {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {lam Lam : ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
        {k : ℝ}
        (hwLp :
          MeasureTheory.MemLp (fun x => max (↑↑(TauCeti.W1p.value u) x - k) 0) 2
            (mu.restrict ↑Omega))
        {x₀ : EuclideanSpace ℝ ι} {r R : ℝ},
        TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
          MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
            (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
                (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value ↑v) x) →
                  TauCeti.PDE.energyFormH1 a 0 0 u ↑v ≤ 0) →
              0 < r →
                r < R →
                  Metric.ball x₀ R ⊆ ↑Omega →
                    ∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ r,
                        ‖↑↑(TauCeti.W1p.gradient
                                    (TauCeti.W1p.posPartAboveOfMemLp
                                      TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_memLp._proof_1
                                      k u hwLp))
                              x‖ ^
                          2 ∂mu ≤
                      (2 * Lam / lam) ^ 2 * (c / (R - r)) ^ 2 *
                        ∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R,
                          max (↑↑(TauCeti.W1p.value u) x - k) 0 ^ 2 ∂mu

The Caccioppoli inequality on concentric balls, with lower-order terms. Formalized in Tau Ceti as TauCeti.PDE.exists_setIntegral_ball_norm_gradient_posPartAbove_sq_le_lowerOrder.

TauCeti.PDE.exists_setIntegral_ball_norm_gradient_posPartAbove_sq_le_lowerOrder.{u_1} {ι : Type u_1}
  [Fintype ι] [DecidableEq ι] :
  ∃ C,
    0 < C ∧
      ∀ {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [inst : mu.IsAddHaarMeasure]
        {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
        {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
        {c : EuclideanSpace ℝ ι → ℝ} {lam Lam beta gamma : ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
        {k : ℝ} (hk : 0 ≤ k) {x₀ : EuclideanSpace ℝ ι} {r R : ℝ},
        TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
          MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
            MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega) →
              MeasureTheory.AEStronglyMeasurable c (mu.restrict ↑Omega) →
                (∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) →
                  (∀ x ∈ ↑Omega, ‖c x‖ ≤ gamma) →
                    (∀ x ∈ ↑Omega, 0 ≤ c x) →
                      (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)),
                          (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega,
                              0 ≤ ↑↑(TauCeti.W1p.value ↑v) x) →
                            TauCeti.PDE.energyFormH1 a b c u ↑v ≤ 0) →
                        0 < r →
                          r < R →
                            Metric.ball x₀ R ⊆ ↑Omega →
                              ∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ r,
                                  ‖↑↑(TauCeti.W1p.gradient
                                              (TauCeti.W1p.posPartAbove
                                                TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_memLp._proof_1
                                                hk u))
                                        x‖ ^
                                    2 ∂mu ≤
                                (2 * (2 * Lam / lam) ^ 2 * (C / (R - r)) ^ 2 +
                                    (2 * beta / lam) ^ 2) *
                                  ∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R,
                                    max (↑↑(TauCeti.W1p.value u) x - k) 0 ^ 2 ∂mu
Sources
LeanTauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_le · TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le · TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder · TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_memLp · TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_memLp · TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_rpow_mul_norm_gradient_sq_le · TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_le_of_ae_eq_rpow · TauCeti.PDE.exists_setIntegral_ball_norm_gradient_posPartAbove_sq_le · TauCeti.PDE.exists_setIntegral_ball_norm_gradient_posPartAbove_sq_le_lowerOrder
Uses 3 · Used by 3
Proof usesTauCeti.Wkp · Young's inequality for real inner products · The zero-forcing Caccioppoli inequality for a positive truncation of a weak subsolution
Used byDe Giorgi's interior oscillation estimate · Moser's reverse Hölder inequality for powers of a positive supersolution · The logarithmic Caccioppoli inequality

TheoremCauchy--Schwarz for jet fields#

The integral of the product of the jet norms of two Sobolev functions is at most the product of their W^{1,2} norms. This is the estimate that turns the pointwise operator-norm bound on the energy integrand into boundedness of the energy form.

TauCeti.PDE.integral_norm_jetField_mul_le.{u_1} {ι : Type u_1} [Fintype ι]
  {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  (u v : ↥(TauCeti.W1p mu Omega 2)) :
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
      ‖TauCeti.PDE.jetField u x‖ * ‖TauCeti.PDE.jetField v x‖ ∂mu ≤
    ‖u‖ * ‖v‖
Lean

Formalized in Tau Ceti as TauCeti.PDE.integral_norm_jetField_mul_le.

Sources
LeanTauCeti.PDE.integral_norm_jetField_mul_le

TheoremThe centered Harnack inequality on a planar disk#

If f is harmonic on the open disk of radius R about c, continuous on its closure and nonnegative on its boundary circle, then every w in the open disk satisfies

(R - ‖w - c‖) / (R + ‖w - c‖) * f c ≤ f w ≤ (R + ‖w - c‖) / (R - ‖w - c‖) * f c.

InnerProductSpace.HarmonicContOnCl.harnack_inequality_center_of_nonneg_on_sphere {f : ℂ → ℝ}
  {c w : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicContOnCl f (Metric.ball c R))
  (hnonneg : ∀ z ∈ Metric.sphere c R, 0 ≤ f z) (hw : w ∈ Metric.ball c R) :
  (R - ‖w - c‖) / (R + ‖w - c‖) * f c ≤ f w ∧ f w ≤ (R + ‖w - c‖) / (R - ‖w - c‖) * f c
Lean

Formalized in Tau Ceti as InnerProductSpace.HarmonicContOnCl.harnack_inequality_center_of_nonneg_on_sphere.

Other forms

The centered Harnack inequality on an open planar disk. Formalized in Tau Ceti as InnerProductSpace.HarmonicOnNhd.harnack_inequality_center.

InnerProductSpace.HarmonicOnNhd.harnack_inequality_center {f : ℂ → ℝ} {c w : ℂ} {R : ℝ}
  (hf : InnerProductSpace.HarmonicOnNhd f (Metric.ball c R))
  (hnonneg : ∀ z ∈ Metric.ball c R, 0 ≤ f z) (hw : w ∈ Metric.ball c R) :
  (R - ‖w - c‖) / (R + ‖w - c‖) * f c ≤ f w ∧ f w ≤ (R + ‖w - c‖) / (R - ‖w - c‖) * f c
Sources
LeanInnerProductSpace.HarmonicContOnCl.harnack_inequality_center_of_nonneg_on_sphere · InnerProductSpace.HarmonicOnNhd.harnack_inequality_center
Used by 1
Used byHarnack's inequality

TheoremDuhamel's formula for the heat equation#

For φ of class C² with compact support and t > 0, (K_t ⋆ φ)(x) - φ(x) = ∫₀ᵗ (K_s ⋆ Δ φ)(x) ds at every point x.

TauCeti.heatKernel_convolution_sub_eq_integral.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] {t : ℝ} [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] {φ : E → F}
  (hφ : ContDiff ℝ 2 φ) (hc : HasCompactSupport φ) (ht : 0 < t) (x : E) :
  MeasureTheory.convolution (TauCeti.heatKernel t) φ (ContinuousLinearMap.lsmul ℝ ℝ)
        MeasureTheory.volume x -
      φ x =
    ∫ (s : ℝ) in 0..t,
      MeasureTheory.convolution (TauCeti.heatKernel s) (Laplacian.laplacian φ)
        (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume x
Lean

Formalized in Tau Ceti as TauCeti.heatKernel_convolution_sub_eq_integral.

Other forms

Duhamel's formula for the heat semigroup. Formalized in Tau Ceti as TauCeti.heatSemigroup_sub_eq_integral.

TauCeti.heatSemigroup_sub_eq_integral.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {p : ENNReal}
  [Fact (1 ≤ p)] {φ : E → F} (hp : p ≠ ⊤) (hφ : ContDiff ℝ 2 φ) (hc : HasCompactSupport φ)
  {f g : ↥(MeasureTheory.Lp F p MeasureTheory.volume)} (hf : ↑↑f =ᵐ[MeasureTheory.volume] φ)
  (hg : ↑↑g =ᵐ[MeasureTheory.volume] Laplacian.laplacian φ) {t : ℝ} (ht : 0 < t) :
  ((TauCeti.heatSemigroup hp).realOperator t) f - f =
    ∫ (s : ℝ) in Set.Ioc 0 t, ((TauCeti.heatSemigroup hp).realOperator s) g
Sources
LeanTauCeti.heatKernel_convolution_sub_eq_integral · TauCeti.heatSemigroup_sub_eq_integral
Uses 1
Proof usesYoung's inequality for an L¹ kernel

TheoremDuhamel's identity in supremum norm#

For bounded uniformly continuous C² data f with bounded first and second derivatives and bounded uniformly continuous Laplacian g, e^{tΔ} f - f = ∫₀ᵗ e^{sΔ} g ds as a Banach-valued integral.

TauCeti.heatSemigroupBUC_sub_eq_integral.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
  {f g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)} {M₁ M₂ : ℝ}
  (hf : ContDiff ℝ 2 ⇑↑f) (h₁ : ∀ (y : E), ‖fderiv ℝ (⇑↑f) y‖ ≤ M₁)
  (h₂ : ∀ (y : E), ‖fderiv ℝ (fderiv ℝ ⇑↑f) y‖ ≤ M₂) (hg : Laplacian.laplacian ⇑↑f = ⇑↑g) {t : ℝ}
  (ht : 0 < t) :
  (TauCeti.heatSemigroupBUC.realOperator t) f - f =
    ∫ (s : ℝ) in Set.Ioc 0 t, (TauCeti.heatSemigroupBUC.realOperator s) g
Lean

Formalized in Tau Ceti as TauCeti.heatSemigroupBUC_sub_eq_integral.

Sources
LeanTauCeti.heatSemigroupBUC_sub_eq_integral

TheoremDuhamel's principle in integrated form#

Let f be jointly measurable and essentially bounded on (0, t) × E, with f(s, ·) α-Hölder for almost every 0 < s < t, where α > 0. Then the Duhamel potential w satisfies w(t, x) = ∫₀ᵗ (Δw(σ, x) + f(σ, x)) dσ.

TauCeti.heatDuhamelPotential_eq_integral.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → E → F}
  {M t : ℝ} {H α : NNReal} (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f))
  (hfM : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), ∀ᵐ (y : E), ‖f s y‖ ≤ M)
  (hH : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), HolderWith H α (f s)) (hα : 0 < α)
  (ht : 0 ≤ t) (x : E) :
  TauCeti.heatDuhamelPotential f t x =
    ∫ (σ : ℝ) in 0..t, Laplacian.laplacian (TauCeti.heatDuhamelPotential f σ) x + f σ x
Lean

Formalized in Tau Ceti as TauCeti.heatDuhamelPotential_eq_integral.

Sources
LeanTauCeti.heatDuhamelPotential_eq_integral
Uses 3
Proof usesHölder bound on the Laplacian of a heat convolution · Hölder bounds on the derivatives of a heat convolution · The temporal Hölder estimate of the Cauchy heat potential

TheoremThe Fredholm alternative in eigenvalue language#

On a bounded domain, if κ is not a Dirichlet eigenvalue then L u - κ u = f in Ω, u = 0 on ∂Ω, has exactly one weak solution for every f ∈ L²(Ω).

TauCeti.PDE.existsUnique_isWeakSolutionDirichlet_sub_const_of_not_isDirichletEigenvalue.{u_1}
  {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ}
  (hcoeff :
    MeasureTheory.MemLp (fun x => TauCeti.PDE.energyIntegrand (a x) (b x) (c x)) ⊤
      (mu.restrict ↑Omega))
  (hcoercive : IsCoercive (TauCeti.PDE.energyFormH1L0 hcoeff)) (hOmega : Bornology.IsBounded ↑Omega)
  {kappa : ℝ} (hkappa : ¬TauCeti.PDE.IsDirichletEigenvalue mu Omega a b c kappa)
  (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))) :
  ∃! u, TauCeti.PDE.IsWeakSolutionDirichlet a b (fun x => c x - kappa) f u
Lean

Formalized in Tau Ceti as TauCeti.PDE.existsUnique_isWeakSolutionDirichlet_sub_const_of_not_isDirichletEigenvalue.

Other forms

The Fredholm alternative for the mass-shifted Dirichlet problem. Formalized in Tau Ceti as TauCeti.PDE.fredholmAlternative_isWeakSolutionDirichlet_sub_const.

TauCeti.PDE.fredholmAlternative_isWeakSolutionDirichlet_sub_const.{u_1} {ι : Type u_1} [Fintype ι]
  {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ}
  (hcoeff :
    MeasureTheory.MemLp (fun x => TauCeti.PDE.energyIntegrand (a x) (b x) (c x)) ⊤
      (mu.restrict ↑Omega))
  (hcoercive : IsCoercive (TauCeti.PDE.energyFormH1L0 hcoeff)) (hOmega : Bornology.IsBounded ↑Omega)
  (kappa : ℝ) :
  (∃ u, u ≠ 0 ∧ TauCeti.PDE.IsWeakSolutionDirichlet a b (fun x => c x - kappa) 0 u) ∨
    ∀ (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))),
      ∃! u, TauCeti.PDE.IsWeakSolutionDirichlet a b (fun x => c x - kappa) f u
Sources
LeanTauCeti.PDE.existsUnique_isWeakSolutionDirichlet_sub_const_of_not_isDirichletEigenvalue · TauCeti.PDE.fredholmAlternative_isWeakSolutionDirichlet_sub_const
Uses 2 · Used by 1
Proof usesRellich–Kondrachov on bounded Lipschitz domains · The variational Fredholm alternative
Used byExistence and uniqueness for the Dirichlet problem with c ≥ 0

TheoremThe global Schauder estimate on the whole space#

Let 0 < α < 1, and let λ, Λ and L be given. Then there is a constant C, depending only on n, α, λ, Λ and L, with the following property. Let a be a matrix-valued coefficient on ℝ^{n+1} which is uniformly elliptic and bounded with constants 0 < λ ≤ Λ (UniformlyEllipticOn univ a λ Λ) and globally α-Hölder entrywise with constant L, and put L u = ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼu. Let u be C² with |u| ≤ N, and with D²u bounded and globally α-Hölder (with any constant). If L u is globally α-Hölder with constant K, then D²u is globally α-Hölder with constant C (K + N), and ‖Du‖ and ‖D²u‖ are bounded by C (K + N).

TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv {n : ℕ}
  {α : NNReal} (hα : 0 < α) (hα1 : α < 1) (lam Lam : ℝ) (L : NNReal) :
  ∃ C,
    ∀ {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ},
      TauCeti.PDE.UniformlyEllipticOn Set.univ a lam Lam →
        (∀ (i j : Fin (n + 1)), HolderWith L α fun x => a x i j) →
          ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {N K : NNReal},
            ContDiff ℝ 2 u →
              (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), |u x| ≤ ↑N) →
                BddAbove (Set.range fun x => ‖iteratedFDeriv ℝ 2 u x‖) →
                  MemHolder α (iteratedFDeriv ℝ 2 u) →
                    (HolderWith K α fun x =>
                        ∑ i,
                          ∑ j,
                            a x i j •
                              ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1))
                                (EuclideanSpace.single j 1)) →
                      HolderWith (C * (K + N)) α (iteratedFDeriv ℝ 2 u) ∧
                        (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), ‖fderiv ℝ u x‖ ≤ ↑C * (↑K + ↑N)) ∧
                          ∀ (x : EuclideanSpace ℝ (Fin (n + 1))),
                            ‖iteratedFDeriv ℝ 2 u x‖ ≤ ↑C * (↑K + ↑N)
Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv.

Other forms

The global Schauder estimate in the C_b^{2,α} norm. Formalized in Tau Ceti as TauCeti.PDE.exists_norm_le_of_sum_smul_fderiv_fderiv.

TauCeti.PDE.exists_norm_le_of_sum_smul_fderiv_fderiv {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1)
  (lam Lam : ℝ) (L : NNReal) :
  ∃ C,
    ∀ {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ},
      TauCeti.PDE.UniformlyEllipticOn Set.univ a lam Lam →
        (∀ (i j : Fin (n + 1)), HolderWith L α fun x => a x i j) →
          ∀ (u : TauCeti.CkHolderSpace 2 α (EuclideanSpace ℝ (Fin (n + 1))) ℝ) {N K : NNReal},
            (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), |u x| ≤ ↑N) →
              (HolderWith K α fun x =>
                  ∑ i,
                    ∑ j,
                      a x i j •
                        ((fderiv ℝ (fderiv ℝ ⇑u) x) (EuclideanSpace.single i 1))
                          (EuclideanSpace.single j 1)) →
                ‖u‖ ≤ ↑C * (↑K + ↑N)

The global Schauder estimate with lower-order bounds. Formalized in Tau Ceti as TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_of_holderWith.

TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_of_holderWith {n : ℕ}
  {α : NNReal} (hα : 0 < α) (hα1 : α < 1) (lam Lam : ℝ) (L : NNReal) :
  ∃ C,
    ∀ {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ},
      TauCeti.PDE.UniformlyEllipticOn Set.univ a lam Lam →
        (∀ (i j : Fin (n + 1)), HolderWith L α fun x => a x i j) →
          ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {N K : NNReal},
            ContDiff ℝ 2 u →
              (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), |u x| ≤ ↑N) →
                (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), ‖fderiv ℝ u x‖ ≤ ↑N) →
                  (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), ‖iteratedFDeriv ℝ 2 u x‖ ≤ ↑N) →
                    (∀ (S : Set (EuclideanSpace ℝ (Fin (n + 1)))),
                        IsCompact S → ∃ V, HolderOnWith V α (iteratedFDeriv ℝ 2 u) S) →
                      (HolderWith K α fun x =>
                          ∑ i,
                            ∑ j,
                              a x i j •
                                ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1))
                                  (EuclideanSpace.single j 1)) →
                        HolderWith (C * (K + N)) α (iteratedFDeriv ℝ 2 u)

The global Schauder estimate with lower-order terms on the whole space. Formalized in Tau Ceti as TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul.

TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul
  {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1) (lam Lam : ℝ) (L B : NNReal) :
  ∃ C,
    ∀ {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ}
      {b : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))}
      {c : EuclideanSpace ℝ (Fin (n + 1)) → ℝ},
      TauCeti.PDE.UniformlyEllipticOn Set.univ a lam Lam →
        (∀ (i j : Fin (n + 1)), HolderWith L α fun x => a x i j) →
          HolderWith L α b →
            (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), ‖b x‖ ≤ ↑B) →
              HolderWith L α c →
                (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), |c x| ≤ ↑B) →
                  ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {N K : NNReal},
                    ContDiff ℝ 2 u →
                      (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), |u x| ≤ ↑N) →
                        BddAbove (Set.range fun x => ‖iteratedFDeriv ℝ 2 u x‖) →
                          MemHolder α (iteratedFDeriv ℝ 2 u) →
                            (HolderWith K α fun x =>
                                ∑ i,
                                      ∑ j,
                                        a x i j •
                                          ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1))
                                            (EuclideanSpace.single j 1) +
                                    (fderiv ℝ u x) (b x) +
                                  c x * u x) →
                              HolderWith (C * (K + N)) α (iteratedFDeriv ℝ 2 u) ∧
                                (∀ (x : EuclideanSpace ℝ (Fin (n + 1))),
                                    ‖fderiv ℝ u x‖ ≤ ↑C * (↑K + ↑N)) ∧
                                  ∀ (x : EuclideanSpace ℝ (Fin (n + 1))),
                                    ‖iteratedFDeriv ℝ 2 u x‖ ≤ ↑C * (↑K + ↑N)
Sources
LeanTauCeti.PDE.exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv · TauCeti.PDE.exists_norm_le_of_sum_smul_fderiv_fderiv · TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_of_holderWith · TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul
Uses 3
Statement usesTauCeti.CkHolderSpace
Proof usesFirst-order Taylor bound for a Hölder derivative · The interior Schauder estimate on small balls

TheoremGreen's first identity against H¹₀(Ω)#

Let u ∈ H¹(Ω) agree almost everywhere on Ω with a function w of class C² on Ω whose Laplacian lies in L²(Ω). Then ∫_Ω ∇v · ∇u = -∫_Ω Δw v for every v ∈ H¹₀(Ω): u solves -Δu = -Δw weakly. No boundary condition is imposed on u.

TauCeti.PDE.energyFormH1_one_zero_zero_eq_setIntegral_neg_laplacian_mul.{u_1} {ι : Type u_1}
  [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {w : EuclideanSpace ℝ ι → ℝ} [DecidableEq ι]
  {u : ↥(TauCeti.W1p mu Omega 2)} (hw : ContDiffOn ℝ 2 w ↑Omega)
  (hu : ↑↑(TauCeti.W1p.value u) =ᵐ[mu.restrict ↑Omega] w)
  (hΔ : MeasureTheory.MemLp (Laplacian.laplacian w) 2 (mu.restrict ↑Omega))
  (v : ↥(TauCeti.W1p0 mu Omega 2)) :
  TauCeti.PDE.energyFormH1 (fun x => 1) 0 0 u ↑v =
    ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, -Laplacian.laplacian w x * ↑↑(TauCeti.W1p.value ↑v) x ∂mu
Lean

Formalized in Tau Ceti as TauCeti.PDE.energyFormH1_one_zero_zero_eq_setIntegral_neg_laplacian_mul.

Sources
LeanTauCeti.PDE.energyFormH1_one_zero_zero_eq_setIntegral_neg_laplacian_mul
Uses 1 · Used by 2
Proof usesGreen's second identity against a test function
Used byThe interior Schauder estimate on small balls · The sharp Poincaré inequality on an interval

TheoremGårding's inequality on H¹(Ω)#

For a uniformly elliptic principal coefficient with lower constant λ, a drift bounded by β and a nonnegative mass coefficient,

(λ/2)‖∇u‖²_{L²} - (β²/2λ)‖u‖²_{L²} ≤ a(u, u)

for every u ∈ H¹(Ω). The drift is absorbed by Young's inequality at the cost of half of the ellipticity floor, which is where the negative L² term comes from. Under the stated general assumption c ≥ 0, either a Poincaré inequality or a sufficiently positive mass lower bound is needed to eliminate that term.

TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self.{u_1} {ι : Type u_1} [Fintype ι]
  {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ}
  {lam Lam beta gamma : ℝ} [mu.IsAddHaarMeasure] [DecidableEq ι]
  (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  (hb : MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega))
  (hc : MeasureTheory.AEStronglyMeasurable c (mu.restrict ↑Omega))
  (hb_bound : ∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) (hc_bound : ∀ x ∈ ↑Omega, ‖c x‖ ≤ gamma)
  (hc_nonneg : ∀ x ∈ ↑Omega, 0 ≤ c x) (u : ↥(TauCeti.W1p mu Omega 2)) :
  lam / 2 * ‖TauCeti.W1p.gradient u‖ ^ 2 - beta ^ 2 / (2 * lam) * ‖TauCeti.W1p.value u‖ ^ 2 ≤
    TauCeti.PDE.energyFormH1 a b c u u
Lean

Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self.

Other forms

Gårding's inequality in H¹-norm form, without a sign condition on c. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_norm_of_norm_le.

TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_norm_of_norm_le.{u_1} {ι : Type u_1}
  [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ}
  {lam Lam beta gamma : ℝ} [mu.IsAddHaarMeasure] [DecidableEq ι]
  (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  (hb : MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega))
  (hc : MeasureTheory.AEStronglyMeasurable c (mu.restrict ↑Omega))
  (hb_bound : ∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) (hc_bound : ∀ x ∈ ↑Omega, ‖c x‖ ≤ gamma)
  (u : ↥(TauCeti.W1p mu Omega 2)) :
  lam / 2 * ‖u‖ ^ 2 - (lam / 2 + gamma + beta ^ 2 / (2 * lam)) * ‖TauCeti.W1p.value u‖ ^ 2 ≤
    TauCeti.PDE.energyFormH1 a b c u u

Gårding's inequality in the roadmap's H¹-norm form. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_norm.

TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_norm.{u_1} {ι : Type u_1} [Fintype ι]
  {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ}
  {lam Lam beta gamma : ℝ} [mu.IsAddHaarMeasure] [DecidableEq ι]
  (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  (hb : MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega))
  (hc : MeasureTheory.AEStronglyMeasurable c (mu.restrict ↑Omega))
  (hb_bound : ∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) (hc_bound : ∀ x ∈ ↑Omega, ‖c x‖ ≤ gamma)
  (hc_nonneg : ∀ x ∈ ↑Omega, 0 ≤ c x) (u : ↥(TauCeti.W1p mu Omega 2)) :
  lam / 2 * ‖u‖ ^ 2 - (lam / 2 + beta ^ 2 / (2 * lam)) * ‖TauCeti.W1p.value u‖ ^ 2 ≤
    TauCeti.PDE.energyFormH1 a b c u u
Sources
LeanTauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self · TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_norm_of_norm_le · TauCeti.PDE.UniformlyEllipticOn.garding_energyFormH1_self_norm
Used by 3
Used byDe Giorgi's theorem: Hölder continuity of weak solutions · The interior Schauder estimate on small balls · The sharp Poincaré inequality on an interval

TheoremHarnack's convergence theorem#

Let F be a family of functions harmonic on a preconnected open set U, monotone at each point of U and bounded above at some point x₀ ∈ U. Then F converges locally uniformly on U to its pointwise supremum.

TauCeti.tendstoLocallyUniformlyOn_iSup_of_monotone.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [SemilatticeSup ι] [Nonempty ι]
  {F : ι → E → ℝ} {U : Set E} (hU : IsOpen U) (hUc : IsPreconnected U)
  (hF : ∀ (i : ι), InnerProductSpace.HarmonicOnNhd (F i) U)
  (hmono : ∀ x ∈ U, Monotone fun i => F i x) {x₀ : E} (hx₀ : x₀ ∈ U)
  (hbdd : BddAbove (Set.range fun i => F i x₀)) :
  TendstoLocallyUniformlyOn F (fun x => ⨆ i, F i x) Filter.atTop U
Lean

Formalized in Tau Ceti as TauCeti.tendstoLocallyUniformlyOn_iSup_of_monotone.

Sources
LeanTauCeti.tendstoLocallyUniformlyOn_iSup_of_monotone
Uses 1 · Used by 1
Proof usesHarnack's inequality
Used byThe limit in Harnack's convergence theorem is harmonic

TheoremHarnack's inequality#

Let K be a compact subset of a preconnected open set U. There is a constant C, depending only on K and U, such that every function u harmonic and nonnegative on U satisfies u x ≤ C * u y for all x, y ∈ K; that is, sup_K u ≤ C * inf_K u.

IsCompact.harnack_inequality.{u_1} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hUc : IsPreconnected U)
  (hKU : K ⊆ U) :
  ∃ C,
    0 ≤ C ∧
      ∀ (u : E → ℝ),
        InnerProductSpace.HarmonicOnNhd u U → (∀ z ∈ U, 0 ≤ u z) → ∀ x ∈ K, ∀ y ∈ K, u x ≤ C * u y
Lean

Formalized in Tau Ceti as IsCompact.harnack_inequality.

Other forms

Harnack's inequality on a smaller closed disk. Formalized in Tau Ceti as InnerProductSpace.HarmonicOnNhd.harnack_inequality.

InnerProductSpace.HarmonicOnNhd.harnack_inequality {f : ℂ → ℝ} {c : ℂ} {R : ℝ}
  (hf : InnerProductSpace.HarmonicOnNhd f (Metric.ball c R))
  (hnonneg : ∀ z ∈ Metric.ball c R, 0 ≤ f z) {r : ℝ} (hrR : r < R) {x y : ℂ}
  (hx : x ∈ Metric.closedBall c r) (hy : y ∈ Metric.closedBall c r) :
  f x ≤ ((R + r) / (R - r)) ^ 2 * f y

Harnack's inequality on a smaller closed disk, from boundary nonnegativity. Formalized in Tau Ceti as InnerProductSpace.HarmonicContOnCl.harnack_inequality_of_nonneg_on_sphere.

InnerProductSpace.HarmonicContOnCl.harnack_inequality_of_nonneg_on_sphere {f : ℂ → ℝ} {c : ℂ}
  {R : ℝ} (hf : InnerProductSpace.HarmonicContOnCl f (Metric.ball c R))
  (hnonneg : ∀ z ∈ Metric.sphere c R, 0 ≤ f z) {r : ℝ} (hrR : r < R) {x y : ℂ}
  (hx : x ∈ Metric.closedBall c r) (hy : y ∈ Metric.closedBall c r) :
  f x ≤ ((R + r) / (R - r)) ^ 2 * f y
Sources
LeanIsCompact.harnack_inequality · InnerProductSpace.HarmonicOnNhd.harnack_inequality · InnerProductSpace.HarmonicContOnCl.harnack_inequality_of_nonneg_on_sphere
Uses 2 · Used by 1
Proof usesThe centered Harnack inequality on a planar disk · The local Harnack inequality
Used byHarnack's convergence theorem

TheoremThe Hopf–Lax subsolution inequality#

For a convex Lagrangian L, moving from (t, x) at velocity w for time h ≥ 0 raises the Hopf–Lax value by at most h L w: u (t + h, x + h w) ≤ u (t, x) + h L w for t > 0.

TauCeti.hopfLax_add_add_smul_le.{u_1} {E : Type u_1} [AddCommGroup E] [_root_.Module ℝ E]
  {L φ : E → ℝ} {t h : ℝ} (hφ : BddBelow (Set.range φ)) (hL : BddBelow (Set.range L))
  (hLc : ConvexOn ℝ Set.univ L) (ht : 0 < t) (hh : 0 ≤ h) (x w : E) :
  TauCeti.hopfLax L φ (t + h) (x + h • w) ≤ TauCeti.hopfLax L φ t x + h * L w
Lean

Formalized in Tau Ceti as TauCeti.hopfLax_add_add_smul_le.

Other forms

The Hopf–Lax subsolution inequality for the p-th power cost. Formalized in Tau Ceti as TauCeti.hopfLax_norm_rpow_add_add_smul_le.

TauCeti.hopfLax_norm_rpow_add_add_smul_le.{u_1} {E : Type u_1} [SeminormedAddCommGroup E]
  [NormedSpace ℝ E] {φ : E → ℝ} {t h p : ℝ} (hp : 1 ≤ p) (hφ : BddBelow (Set.range φ)) (ht : 0 < t)
  (hh : 0 ≤ h) (x w : E) :
  TauCeti.hopfLax (fun x => ‖x‖ ^ p) φ (t + h) (x + h • w) ≤
    TauCeti.hopfLax (fun x => ‖x‖ ^ p) φ t x + h * ‖w‖ ^ p
Sources
LeanTauCeti.hopfLax_add_add_smul_le · TauCeti.hopfLax_norm_rpow_add_add_smul_le
Used by 1
Used byThe Benamou–Brenier lower bound

TheoremHölder bound on the Laplacian of a heat convolution#

The Laplacian of the heat convolution of a bounded α-Hölder function with constant H is O(H τ^((α - 2)/2)), uniformly in the function.

TauCeti.exists_norm_laplacian_heatKernel_convolution_le.{u_1, u_2} {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] [MeasurableSpace E] [BorelSpace E] [CompleteSpace F] {α : NNReal} :
  ∃ C ≥ 0,
    ∀ {g : E → F} {M τ : ℝ} {H : NNReal},
      MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume →
        (∀ᵐ (y : E), ‖g y‖ ≤ M) →
          HolderWith H α g →
            0 < τ →
              ∀ (x : E),
                ‖Laplacian.laplacian
                      (MeasureTheory.convolution (TauCeti.heatKernel τ) g
                        (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)
                      x‖ ≤
                  C * ↑H * τ ^ ((↑α - 2) / 2)
Lean

Formalized in Tau Ceti as TauCeti.exists_norm_laplacian_heatKernel_convolution_le.

Sources
LeanTauCeti.exists_norm_laplacian_heatKernel_convolution_le
Uses 1 · Used by 1
Proof usesHölder bounds on the derivatives of a heat convolution
Used byDuhamel's principle in integrated form

TheoremHölder bounds on the derivatives of a heat convolution#

If g is bounded and α-Hölder with constant H, then for m ≥ 1 and t > 0, ‖D^m (K_t ⋆ g)(x)‖ ≤ H ∫ ‖D^m K_t(z)‖ ‖z‖^α dz. By TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_mul_rpow_le the right side is O(H t^((α - m) / 2)), which for m = 2 is integrable in time near t = 0 when α > 0.

TauCeti.norm_iteratedFDeriv_heatKernel_convolution_le_of_holderWith.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {g : E → F} {M t : ℝ} [MeasurableSpace E] [BorelSpace E]
  [CompleteSpace F] (ht : 0 < t) (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume)
  (hM : ∀ᵐ (y : E), ‖g y‖ ≤ M) {H α : NNReal} (hH : HolderWith H α g) {m : ℕ} (hm : m ≠ 0) (x : E) :
  ‖iteratedFDeriv ℝ m
        (MeasureTheory.convolution (TauCeti.heatKernel t) g (ContinuousLinearMap.lsmul ℝ ℝ)
          MeasureTheory.volume)
        x‖ ≤
    ↑H * ∫ (z : E), ‖iteratedFDeriv ℝ m (TauCeti.heatKernel t) z‖ * ‖z‖ ^ ↑α
Lean

Formalized in Tau Ceti as TauCeti.norm_iteratedFDeriv_heatKernel_convolution_le_of_holderWith.

Sources
LeanTauCeti.norm_iteratedFDeriv_heatKernel_convolution_le_of_holderWith
Used by 4
Used byDuhamel's principle in integrated form · Hölder bound on the Laplacian of a heat convolution · The Hölder estimate for the Hessian of the Duhamel potential · The temporal Hölder estimate of the Cauchy heat potential

TheoremThe Hölder estimate for the Hessian of the Duhamel potential#

For 0 < α < 1 there is a constant C, depending only on α and the dimension, such that the Hessian D² w(t, ·) is α-Hölder with constant C H whenever f is jointly measurable and essentially bounded on (0, t) × E and f(s, ·) is α-Hölder with constant H for almost every 0 < s < t. Neither the bound on f nor the time t enters the estimate.

TauCeti.exists_holderWith_iteratedFDeriv_two_heatDuhamelPotential.{u_1, u_2} {E : Type u_1}
  {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
  {α : NNReal} (hα₀ : 0 < α) (hα₁ : α < 1) :
  ∃ C,
    ∀ {f : ℝ → E → F} {M t : ℝ} {H : NNReal},
      MeasureTheory.StronglyMeasurable (Function.uncurry f) →
        (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), ∀ᵐ (y : E), ‖f s y‖ ≤ M) →
          (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), HolderWith H α (f s)) →
            0 < t → HolderWith (C * H) α (iteratedFDeriv ℝ 2 (TauCeti.heatDuhamelPotential f t))
Lean

Formalized in Tau Ceti as TauCeti.exists_holderWith_iteratedFDeriv_two_heatDuhamelPotential.

Sources
LeanTauCeti.exists_holderWith_iteratedFDeriv_two_heatDuhamelPotential
Uses 1
Proof usesHölder bounds on the derivatives of a heat convolution

TheoremThe interior Calderón–Zygmund estimate for continuous coefficients#

Let 0 < n and 1 < p < ∞, let Ω ⊆ ℝⁿ be open and K ⊆ Ω compact, and let a be a matrix-valued coefficient, measurable on Ω and continuous at each x ∈ K, such that a x is elliptic at each x ∈ K, that is, λₓ ‖ξ‖² ≤ ξᵀ a(x) ξ for some λₓ > 0. Let b and c be measurable lower-order coefficients with ‖b(x)‖ ≤ β and |c(x)| ≤ γ for almost every x ∈ Ω. Then there is a constant C, depending on a, β, γ, K and Ω but not on u or f, such that every u ∈ W^{2,p}(Ω) with ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼu + ⟪b, ∇u⟫ + c u = f ∈ Lᵖ(Ω) almost everywhere on Ω satisfies

‖D²u‖_{Lᵖ(K)} ≤ C (‖f‖_{Lᵖ(Ω)} + ‖u‖_{Lᵖ(Ω)}),

where D²u is the weak Hessian TauCeti.Wkp.iteratedGradient 1 u and ∇u the weak gradient TauCeti.Wkp.iteratedGradient 0 (TauCeti.Wkp.lowerOrder 1 u). No boundary condition on u and no regularity of Ω are assumed, and the gradient of u does not appear on the right.

TauCeti.PDE.exists_lpNorm_iteratedGradient_le_of_sum_mul_inner_add_inner_add_mul_eq_of_continuousAt
  {n : ℕ} {p : ENNReal} [Fact (1 ≤ p)] (hn : 0 < n) (hp : 1 < p) (hp_top : p ≠ ⊤)
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))} {K : Set (EuclideanSpace ℝ (Fin n))}
  (hK : IsCompact K) (hKΩ : K ⊆ ↑Omega) {a : EuclideanSpace ℝ (Fin n) → Matrix (Fin n) (Fin n) ℝ}
  (ha : MeasureTheory.AEStronglyMeasurable a (MeasureTheory.volume.restrict ↑Omega))
  (hcont : ∀ x ∈ K, ContinuousAt a x)
  (hell :
    ∀ x ∈ K,
      ∃ lam,
        0 < lam ∧ ∀ (ξ : EuclideanSpace ℝ (Fin n)), lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp)
  {b : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {β : ℝ}
  (hb : MeasureTheory.AEStronglyMeasurable b (MeasureTheory.volume.restrict ↑Omega))
  (hbβ : ∀ᵐ (x : EuclideanSpace ℝ (Fin n)) ∂MeasureTheory.volume.restrict ↑Omega, ‖b x‖ ≤ β)
  {c : EuclideanSpace ℝ (Fin n) → ℝ} {γ : ℝ}
  (hc : MeasureTheory.AEStronglyMeasurable c (MeasureTheory.volume.restrict ↑Omega))
  (hcγ : ∀ᵐ (x : EuclideanSpace ℝ (Fin n)) ∂MeasureTheory.volume.restrict ↑Omega, |c x| ≤ γ) :
  ∃ C,
    ∀ (u : TauCeti.Wkp MeasureTheory.volume Omega p 2)
      (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑Omega))),
      (∀ᵐ (x : EuclideanSpace ℝ (Fin n)) ∂MeasureTheory.volume.restrict ↑Omega,
          ∑ i,
                  ∑ j,
                    a x i j *
                      inner ℝ ((↑↑(TauCeti.Wkp.iteratedGradient 1 u) x) (EuclideanSpace.single i 1))
                        (EuclideanSpace.single j 1) +
                inner ℝ (b x) (↑↑(TauCeti.Wkp.iteratedGradient 0 (TauCeti.Wkp.lowerOrder 1 u)) x) +
              c x * ↑↑(TauCeti.Wkp.value 2 u) x =
            ↑↑f x) →
        MeasureTheory.lpNorm (↑↑(TauCeti.Wkp.iteratedGradient 1 u)) p
            (MeasureTheory.volume.restrict K) ≤
          C * (‖f‖ + ‖TauCeti.Wkp.value 2 u‖)
Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_lpNorm_iteratedGradient_le_of_sum_mul_inner_add_inner_add_mul_eq_of_continuousAt.

Other forms

The interior Calderón–Zygmund estimate on balls for coefficients of small oscillation. Formalized in Tau Ceti as TauCeti.PDE.exists_mul_lpNorm_iteratedGradient_ball_le_of_sum_mul_inner_add_inner_add_mul_eq.

TauCeti.PDE.exists_mul_lpNorm_iteratedGradient_ball_le_of_sum_mul_inner_add_inner_add_mul_eq {n : ℕ}
  {p : ENNReal} [Fact (1 ≤ p)] (hn : 0 < n) (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C δ,
    0 < δ ∧
      ∀ {A : Matrix (Fin n) (Fin n) ℝ} {lam : ℝ},
        0 < lam →
          (∀ (ξ : EuclideanSpace ℝ (Fin n)), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) →
            ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))}
              {x₀ : EuclideanSpace ℝ (Fin n)} {r R : ℝ},
              r < R →
                Metric.ball x₀ R ⊆ ↑Omega →
                  ∀ {a : EuclideanSpace ℝ (Fin n) → Matrix (Fin n) (Fin n) ℝ}
                    {b : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)}
                    {c : EuclideanSpace ℝ (Fin n) → ℝ} {ε Λ β γ : ℝ},
                    MeasureTheory.AEStronglyMeasurable a
                        (MeasureTheory.volume.restrict (Metric.ball x₀ R)) →
                      ε ≤ δ * lam →
                        (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                            x ∈ Metric.ball x₀ R → ∀ (i j : Fin n), |a x i j - A i j| ≤ ε) →
                          (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                              x ∈ Metric.ball x₀ R → ∀ (i j : Fin n), |a x i j| ≤ Λ) →
                            MeasureTheory.AEStronglyMeasurable b
                                (MeasureTheory.volume.restrict (Metric.ball x₀ R)) →
                              (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                                  x ∈ Metric.ball x₀ R → ‖b x‖ ≤ β) →
                                MeasureTheory.AEStronglyMeasurable c
                                    (MeasureTheory.volume.restrict (Metric.ball x₀ R)) →
                                  (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                                      x ∈ Metric.ball x₀ R → |c x| ≤ γ) →
                                    ∀ (u : TauCeti.Wkp MeasureTheory.volume Omega p 2)
                                      (f : EuclideanSpace ℝ (Fin n) → ℝ),
                                      (∀ᵐ (x :
                                          EuclideanSpace ℝ
                                            (Fin
                                              n)) ∂MeasureTheory.volume.restrict (Metric.ball x₀ R),
                                          ∑ i,
                                                  ∑ j,
                                                    a x i j *
                                                      inner ℝ
                                                        ((↑↑(TauCeti.Wkp.iteratedGradient 1 u) x)
                                                          (EuclideanSpace.single i 1))
                                                        (EuclideanSpace.single j 1) +
                                                inner ℝ (b x)
                                                  (↑↑(TauCeti.Wkp.iteratedGradient 0
                                                          (TauCeti.Wkp.lowerOrder 1 u))
                                                    x) +
                                              c x * ↑↑(TauCeti.Wkp.value 2 u) x =
                                            f x) →
                                        (R - r) ^ 2 *
                                            MeasureTheory.lpNorm
                                              (↑↑(TauCeti.Wkp.iteratedGradient 1 u)) p
                                              (MeasureTheory.volume.restrict (Metric.ball x₀ r)) ≤
                                          ↑C *
                                            (R ^ 2 / lam *
                                                MeasureTheory.lpNorm f p
                                                  (MeasureTheory.volume.restrict
                                                    (Metric.ball x₀ R)) +
                                              (1 + (Λ + β * R + γ * R ^ 2) / lam) ^ 2 *
                                                MeasureTheory.lpNorm (↑↑(TauCeti.Wkp.value 2 u)) p
                                                  (MeasureTheory.volume.restrict
                                                    (Metric.ball x₀ R)))
Sources
LeanTauCeti.PDE.exists_lpNorm_iteratedGradient_le_of_sum_mul_inner_add_inner_add_mul_eq_of_continuousAt · TauCeti.PDE.exists_mul_lpNorm_iteratedGradient_ball_le_of_sum_mul_inner_add_inner_add_mul_eq
Uses 3 · Used by 1
Statement usesTauCeti.Wkp
Proof usesHölder's inequality for the integral of a product · The localized Calderón–Zygmund estimate for coefficients of small oscillation
Used byThe Calderón–Zygmund estimate ‖D²u‖_p ≤ C ‖Δu‖_p

TheoremThe interior Schauder estimate on small balls#

Let 0 < α < 1. There is C₀ > 0, depending only on dimension and α, with the following property. Let 0 < λ, Λ, L, M and 0 < R be given, put κ = C₀ (Λ / λ)^(1 + (n+1)/4 + α/2), and assume the scale condition

2 κ (n+1)² (1 + 2ᵅ) L Rᵅ ≤ λ.

Then for every ρ < R there is C, depending only on n, α, λ, Λ, L, M, R and ρ, with the following property. Let a be α-Hölder entrywise with constant L and bounded entrywise by M on the closed ball closedBall x₀ R, and suppose a x₀ has ellipticity bounds λ, Λ. Put L u = ∑ᵢⱼ aᵢⱼ ∂ᵢⱼu. Let u be C² on the open ball B_R, with |u|, ‖Du‖ and ‖D²u‖ bounded by N there and with D²u α-Hölder on B_R (with any constant). If L u is α-Hölder on B_R with constant K, then D²u is α-Hölder on closedBall x₀ ρ with constant C (K + N).

The constant C does not depend on the centre x₀ or on the coefficient field a beyond the bounds λ, Λ, L and M; this uniformity is what makes the estimate usable on infinitely many balls at once.

TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_closedBall_of_sum_smul_fderiv_fderiv {n : ℕ}
  {α : NNReal} (hα : 0 < α) (hα1 : α < 1) :
  ∃ C₀,
    0 < C₀ ∧
      ∀ {lam Lam : ℝ} {L M : NNReal} {R : ℝ},
        0 < lam →
          0 < R →
            2 * (C₀ * (Lam / lam) ^ (1 + (↑n + 1) / 4 + ↑α / 2)) * (↑n + 1) ^ 2 *
                  ((1 + 2 ^ ↑α) * ↑L * R ^ ↑α) ≤
                lam →
              ∀ {ρ : ℝ},
                ρ < R →
                  ∃ C,
                    ∀ {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ}
                      {x₀ : EuclideanSpace ℝ (Fin (n + 1))},
                      (∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))),
                          lam * ‖ξ‖ ^ 2 ≤ (a x₀).toQuadraticForm' ξ.ofLp) →
                        (∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))),
                            (a x₀).toQuadraticForm' ξ.ofLp ≤ Lam * ‖ξ‖ ^ 2) →
                          (∀ (i j : Fin (n + 1)),
                              HolderOnWith L α (fun x => a x i j) (Metric.closedBall x₀ R)) →
                            (∀ x ∈ Metric.closedBall x₀ R, ∀ (i j : Fin (n + 1)), |a x i j| ≤ ↑M) →
                              ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {N K V : NNReal},
                                ContDiffOn ℝ 2 u (Metric.ball x₀ R) →
                                  (∀ x ∈ Metric.ball x₀ R, |u x| ≤ ↑N) →
                                    (∀ x ∈ Metric.ball x₀ R, ‖fderiv ℝ u x‖ ≤ ↑N) →
                                      (∀ x ∈ Metric.ball x₀ R, ‖iteratedFDeriv ℝ 2 u x‖ ≤ ↑N) →
                                        HolderOnWith V α (iteratedFDeriv ℝ 2 u) (Metric.ball x₀ R) →
                                          HolderOnWith K α
                                              (fun x =>
                                                ∑ i,
                                                  ∑ j,
                                                    a x i j •
                                                      ((fderiv ℝ (fderiv ℝ u) x)
                                                          (EuclideanSpace.single i 1))
                                                        (EuclideanSpace.single j 1))
                                              (Metric.ball x₀ R) →
                                            HolderOnWith (C * (K + N)) α (iteratedFDeriv ℝ 2 u)
                                              (Metric.closedBall x₀ ρ)
Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_closedBall_of_sum_smul_fderiv_fderiv.

Other forms

Interior Schauder estimate for constant-coefficient operators, classical form. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv.

TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv {n : ℕ} {α : NNReal}
  (hα : 0 < α) (hα1 : α < 1) :
  ∃ C,
    0 ≤ C ∧
      ∀ {A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} {lam Lam : ℝ},
        0 < lam →
          (∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) →
            (∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))), A.toQuadraticForm' ξ.ofLp ≤ Lam * ‖ξ‖ ^ 2) →
              ∀ {U S : Set (EuclideanSpace ℝ (Fin (n + 1)))}
                {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {K : NNReal} {R : ℝ},
                IsOpen U →
                  ContDiffOn ℝ 2 u U →
                    Bornology.IsBounded S →
                      0 < R →
                        Metric.cthickening R S ⊆ U →
                          HolderOnWith K α
                              (fun x =>
                                ∑ i,
                                  ∑ j,
                                    A i j •
                                      ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1))
                                        (EuclideanSpace.single j 1))
                              (Metric.thickening R S) →
                            HolderOnWith
                              (C * (Lam / lam) ^ (1 + (↑n + 1) / 4 + ↑α / 2) *
                                  (↑K / lam +
                                    R ^ (-((↑n + 1) / 2 + ↑α)) *
                                      (MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 u) 2
                                          (MeasureTheory.volume.restrict
                                            (Metric.thickening R S))).toReal)).toNNReal
                              α (iteratedFDeriv ℝ 2 u) S

The interior Schauder estimate for Hölder coefficients. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_of_holderOnWith.

TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_of_holderOnWith {n : ℕ}
  {α : NNReal} (hα : 0 < α) (hα1 : α < 1) {Ω K : Set (EuclideanSpace ℝ (Fin (n + 1)))}
  (hΩ : IsOpen Ω) (hK : IsCompact K) (hKΩ : K ⊆ Ω)
  {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ}
  (ha :
    ∀ x ∈ K,
      ∃ r > 0, ∃ L, ∀ (i j : Fin (n + 1)), HolderOnWith L α (fun y => a y i j) (Metric.ball x r))
  (hell :
    ∀ x ∈ K,
      ∃ lam,
        0 < lam ∧
          ∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))), lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp) :
  ∃ C,
    ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {N M : NNReal},
      ContDiffOn ℝ 2 u Ω →
        (∀ x ∈ Ω, |u x| ≤ ↑N) →
          (∀ x ∈ Ω, ‖fderiv ℝ u x‖ ≤ ↑N) →
            (∀ x ∈ Ω, ‖iteratedFDeriv ℝ 2 u x‖ ≤ ↑N) →
              (∀ S ⊆ Ω, IsCompact S → ∃ V, HolderOnWith V α (iteratedFDeriv ℝ 2 u) S) →
                HolderOnWith M α
                    (fun x =>
                      ∑ i,
                        ∑ j,
                          a x i j •
                            ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1))
                              (EuclideanSpace.single j 1))
                    Ω →
                  HolderOnWith (C * (M + N)) α (iteratedFDeriv ℝ 2 u) K

Interior Schauder estimate for Poisson's equation, classical form. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_laplacian.

TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_laplacian {n : ℕ} {α : NNReal} (hα : 0 < α)
  (hα1 : α < 1) :
  ∃ C,
    0 ≤ C ∧
      ∀ {U S : Set (EuclideanSpace ℝ (Fin (n + 1)))} {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
        {K : NNReal} {R : ℝ},
        IsOpen U →
          ContDiffOn ℝ 2 u U →
            Bornology.IsBounded S →
              0 < R →
                Metric.cthickening R S ⊆ U →
                  HolderOnWith K α (Laplacian.laplacian u) (Metric.thickening R S) →
                    HolderOnWith
                      (C *
                          (↑K +
                            R ^ (-((↑n + 1) / 2 + ↑α)) *
                              (MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 u) 2
                                  (MeasureTheory.volume.restrict
                                    (Metric.thickening R S))).toReal)).toNNReal
                      α (iteratedFDeriv ℝ 2 u) S

The interior Schauder estimate with lower-order terms. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul.

TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul
  {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1) {Ω K : Set (EuclideanSpace ℝ (Fin (n + 1)))}
  (hΩ : IsOpen Ω) (hK : IsCompact K) (hKΩ : K ⊆ Ω)
  {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ}
  {b : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))}
  {c : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}
  (ha :
    ∀ x ∈ K,
      ∃ r > 0, ∃ L, ∀ (i j : Fin (n + 1)), HolderOnWith L α (fun y => a y i j) (Metric.ball x r))
  (hb : ∀ x ∈ K, ∃ r > 0, ∃ L, HolderOnWith L α b (Metric.ball x r))
  (hc : ∀ x ∈ K, ∃ r > 0, ∃ L, HolderOnWith L α c (Metric.ball x r))
  (hell :
    ∀ x ∈ K,
      ∃ lam,
        0 < lam ∧
          ∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))), lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp) :
  ∃ C,
    ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {N M : NNReal},
      ContDiffOn ℝ 2 u Ω →
        (∀ x ∈ Ω, |u x| ≤ ↑N) →
          (∀ x ∈ Ω, ‖fderiv ℝ u x‖ ≤ ↑N) →
            (∀ x ∈ Ω, ‖iteratedFDeriv ℝ 2 u x‖ ≤ ↑N) →
              (∀ S ⊆ Ω, IsCompact S → ∃ V, HolderOnWith V α (iteratedFDeriv ℝ 2 u) S) →
                HolderOnWith M α
                    (fun x =>
                      ∑ i,
                            ∑ j,
                              a x i j •
                                ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1))
                                  (EuclideanSpace.single j 1) +
                          (fderiv ℝ u x) (b x) +
                        c x * u x)
                    Ω →
                  HolderOnWith (C * (M + N)) α (iteratedFDeriv ℝ 2 u) K
Sources
LeanTauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_closedBall_of_sum_smul_fderiv_fderiv · TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv · TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_of_holderOnWith · TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_laplacian · TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul
Uses 15 · Used by 1
Proof usesThe du Bois-Reymond lemma · Green's first identity against H¹₀(Ω) · Green's second identity against a test function · Gårding's inequality on H¹(Ω) · Hölder's bound on an average · Hölder's inequality for the integral of a product · Jensen's inequality for the square of a mean · The Lipschitz bound for bounded harmonic functions · The local Campanato estimate · Meyers–Serrin: H = W in W^{k,p}(Ω) · The Poincaré inequality on a ball · Rademacher's theorem for locally Lipschitz functions · Schauder estimate for a Hessian supported in a ball · TauCeti.Wkp · Weyl's lemma for continuous functions
Used byThe global Schauder estimate on the whole space

TheoremThe limit in Harnack's convergence theorem is harmonic#

Let F be a family of functions harmonic on a preconnected open set U, monotone at each point of U and bounded above at some point x₀ ∈ U. Then its pointwise supremum is harmonic on U.

TauCeti.harmonicOnNhd_iSup_of_monotone.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ι : Type u_2} [SemilatticeSup ι] [Nonempty ι]
  {F : ι → E → ℝ} {U : Set E} (hU : IsOpen U) (hUc : IsPreconnected U)
  (hF : ∀ (i : ι), InnerProductSpace.HarmonicOnNhd (F i) U)
  (hmono : ∀ x ∈ U, Monotone fun i => F i x) {x₀ : E} (hx₀ : x₀ ∈ U)
  (hbdd : BddAbove (Set.range fun i => F i x₀)) :
  InnerProductSpace.HarmonicOnNhd (fun x => ⨆ i, F i x) U
Lean

Formalized in Tau Ceti as TauCeti.harmonicOnNhd_iSup_of_monotone.

Sources
LeanTauCeti.harmonicOnNhd_iSup_of_monotone
Uses 3 · Used by 1
Proof usesThe du Bois-Reymond lemma · Green's second identity against a test function · Harnack's convergence theorem
Used byPerron's theorem

TheoremThe local Harnack inequality#

If u is harmonic and nonnegative on ball c (4 * r), then any two of its values on ball c r are within the factor 3 ^ n of each other, where n is the dimension of E.

InnerProductSpace.HarmonicOnNhd.le_three_pow_mul_of_nonneg.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {x y c : E}
  {r : ℝ} (hu : InnerProductSpace.HarmonicOnNhd u (Metric.ball c (4 * r)))
  (hnonneg : ∀ z ∈ Metric.ball c (4 * r), 0 ≤ u z) (hx : x ∈ Metric.ball c r)
  (hy : y ∈ Metric.ball c r) : u x ≤ 3 ^ Module.finrank ℝ E * u y
Lean

Formalized in Tau Ceti as InnerProductSpace.HarmonicOnNhd.le_three_pow_mul_of_nonneg.

Sources
LeanInnerProductSpace.HarmonicOnNhd.le_three_pow_mul_of_nonneg
Uses 2 · Used by 1
Proof usesThe du Bois-Reymond lemma · Green's second identity against a test function
Used byHarnack's inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.