Partial differential equations

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremExistence and uniqueness for the Dirichlet problem with `c ≥ 0`#

Let Ω ⊆ ℝⁿ, n ≥ 1, be a bounded open set, and let L u = -∂ᵢ(aⁱʲ ∂ⱼu) + bⁱ ∂ᵢu + c u have measurable, uniformly elliptic a, measurable b with ‖b‖ ≤ β and measurable c with 0 ≤ c ≤ γ. Then for every f ∈ L²(Ω) there is exactly one u ∈ H¹₀(Ω) with a(u, v) = ∫_Ω f v for all v ∈ H¹₀(Ω). Since β is arbitrary, the energy form of L need not be coercive.

TauCeti.PDE.UniformlyEllipticOn.existsUnique_isWeakSolutionDirichlet_of_mass_nonneg.{u_1}
  {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ}
  {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ}
  {lam Lam beta gamma : ℝ} [DecidableEq ι] [Nonempty ι]
  (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) (hOmega : Bornology.IsBounded ↑Omega)
  (f : ↥(MeasureTheory.Lp ℝ 2 (mu.restrict ↑Omega))) :
  ∃! u, TauCeti.PDE.IsWeakSolutionDirichlet a b c f u

Lean

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

Sources

LeanTauCeti.PDE.UniformlyEllipticOn.existsUnique_isWeakSolutionDirichlet_of_mass_nonneg

Uses 3

Proof usesThe Fredholm alternative in eigenvalue language · The Sobolev inequality on W^{1,p}_0 of a ball · TauCeti.Wkp

TheoremDe Giorgi's theorem: Hölder continuity of weak solutions #

Let n ≥ 1 be the dimension. There are α ∈ (0, 1] and C > 0, depending only on λ, Λ, the dimension and the normalization of the additive Haar measure mu, such that the following holds. Let a be measurable and uniformly elliptic on Ω with constants λ, Λ, and let u ∈ H¹(Ω) be a weak solution of -∂ᵢ(aⁱʲ ∂ⱼu) = 0. If the closed R-thickening of a set K lies in Ω, then the precise representative of u is Hölder continuous on K with exponent α and constant C R^(-α - n/2) ‖u‖_{L²(Ω)}.

The precise representative agrees with u almost everywhere on Ω (TauCeti.W1p.ae_eq_preciseRepresentative). No regularity of the coefficients beyond measurability is assumed. This is the case b = 0 of TauCeti.PDE.exists_holderOnWith_preciseRepresentative_drift.

TauCeti.PDE.exists_holderOnWith_preciseRepresentative.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {lam Lam : ℝ} [Nonempty ι] :
  ∃ α C,
    0 < α ∧
      α ≤ 1 ∧
        0 < C ∧
          ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
            {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
            {K : Set (EuclideanSpace ℝ ι)} {R : ℝ},
            TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
              MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
                (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)), TauCeti.PDE.energyFormH1 a 0 0 u ↑v = 0) →
                  0 < R →
                    Metric.cthickening R K ⊆ ↑Omega →
                      HolderOnWith
                        (C * R ^ (-↑α) *
                            (R ^ (-↑(Fintype.card ι) / 2) *
                              √(∫ (y : EuclideanSpace ℝ ι) in ↑Omega,
                                  ↑↑(TauCeti.W1p.value u) y ^ 2 ∂mu))).toNNReal
                        α (TauCeti.MeasureTheory.preciseRepresentative mu ↑↑(TauCeti.W1p.value u)) K

Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_preciseRepresentative.

Other forms

De Giorgi's theorem on an equation with a discontinuous coefficient. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_preciseRepresentative_jumpCoefficient.

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

De Giorgi's theorem on compact sets. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_isCompact.

TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_isCompact.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {lam Lam : ℝ} :
  ∃ α,
    0 < α ∧
      α ≤ 1 ∧
        ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
          {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
          {K : Set (EuclideanSpace ℝ ι)},
          TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
            MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
              (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)), TauCeti.PDE.energyFormH1 a 0 0 u ↑v = 0) →
                IsCompact K →
                  K ⊆ ↑Omega →
                    ∃ C,
                      HolderOnWith C α
                        (TauCeti.MeasureTheory.preciseRepresentative mu ↑↑(TauCeti.W1p.value u)) K

De Giorgi's theorem with a drift on compact sets. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_isCompact_drift.

TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_isCompact_drift.{u_1} {ι : Type u_1}
  [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  [mu.IsAddHaarMeasure] {lam Lam : ℝ} [Nonempty ι] :
  ∃ α,
    0 < α ∧
      α ≤ 1 ∧
        ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
          {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
          {beta : ℝ} {u : ↥(TauCeti.W1p mu Omega 2)} {K : Set (EuclideanSpace ℝ ι)},
          TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
            MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
              MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega) →
                (∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) →
                  (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)), TauCeti.PDE.energyFormH1 a b 0 u ↑v = 0) →
                    IsCompact K →
                      K ⊆ ↑Omega →
                        ∃ C,
                          HolderOnWith C α
                            (TauCeti.MeasureTheory.preciseRepresentative mu ↑↑(TauCeti.W1p.value u))
                            K

De Giorgi's theorem with a drift: Hölder continuity of weak solutions. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_preciseRepresentative_drift.

TauCeti.PDE.exists_holderOnWith_preciseRepresentative_drift.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {lam Lam : ℝ} [Nonempty ι] (σ : ℝ) :
  ∃ α C,
    0 < α ∧
      α ≤ 1 ∧
        0 < C ∧
          ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
            {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
            {beta : ℝ} {u : ↥(TauCeti.W1p mu Omega 2)} {K : Set (EuclideanSpace ℝ ι)} {R : ℝ},
            TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
              MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
                MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega) →
                  (∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) →
                    (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)), TauCeti.PDE.energyFormH1 a b 0 u ↑v = 0) →
                      0 < R →
                        Metric.cthickening R K ⊆ ↑Omega →
                          beta * R ≤ σ * lam →
                            HolderOnWith
                              (C * R ^ (-↑α) *
                                  (R ^ (-↑(Fintype.card ι) / 2) *
                                    √(∫ (y : EuclideanSpace ℝ ι) in ↑Omega,
                                        ↑↑(TauCeti.W1p.value u) y ^ 2 ∂mu))).toNNReal
                              α
                              (TauCeti.MeasureTheory.preciseRepresentative mu
                                ↑↑(TauCeti.W1p.value u))
                              K

De Giorgi's theorem with a right-hand side. Formalized in Tau Ceti as TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_memLp.

TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_memLp.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  [Nonempty ι] {lam Lam : ℝ} {r : NNReal} (hr : 1 < r) (hrn : ↑(Fintype.card ι) < 2 * ↑r) :
  ∃ α C,
    0 < α ∧
      α ≤ 1 ∧
        0 < C ∧
          ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
            {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {f : EuclideanSpace ℝ ι → ℝ}
            {u : ↥(TauCeti.W1p mu Omega 2)} {K : Set (EuclideanSpace ℝ ι)} {R : ℝ},
            TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
              MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
                MeasureTheory.MemLp f (↑r) (mu.restrict ↑Omega) →
                  (∀ (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) →
                    0 < R →
                      Metric.cthickening R K ⊆ ↑Omega →
                        HolderOnWith
                          (C * R ^ (-↑α) *
                              (R ^ (-↑(Fintype.card ι) / 2) *
                                  √(∫ (y : EuclideanSpace ℝ ι) in ↑Omega,
                                      ↑↑(TauCeti.W1p.value u) y ^ 2 ∂mu) +
                                R ^ (2 - ↑(Fintype.card ι) / ↑r) *
                                    (MeasureTheory.eLpNorm f (↑r) (mu.restrict ↑Omega)).toReal /
                                  lam)).toNNReal
                          α (TauCeti.MeasureTheory.preciseRepresentative mu ↑↑(TauCeti.W1p.value u))
                          K

Sources

LeanTauCeti.PDE.exists_holderOnWith_preciseRepresentative · TauCeti.PDE.exists_holderOnWith_preciseRepresentative_jumpCoefficient · TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_isCompact · TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_isCompact_drift · TauCeti.PDE.exists_holderOnWith_preciseRepresentative_drift · TauCeti.PDE.exists_holderOnWith_preciseRepresentative_of_memLp

Uses 10

Proof usesThe L² Leibniz estimate · The analytic content of the extension theorem · De Giorgi's interior oscillation estimate · Gårding's inequality on H¹(Ω) · Hölder's inequality for Young's exponents · The Poincaré inequality on a ball · The Sobolev inequality on W^{1,p}_0 of a ball · Stampacchia's global bound · TauCeti.Wkp · The zero-forcing Caccioppoli inequality for a positive truncation of a weak subsolution

TheoremMoser's Harnack inequality #

Let n ≥ 1 be the dimension. There is C > 0, depending only on λ, Λ, the dimension and the normalization of the additive Haar measure mu, with the following property. Let a be measurable and uniformly elliptic on Ω with constants λ, Λ, and let u ∈ H¹(Ω) be a weak solution of -∂ᵢ(aⁱʲ ∂ⱼu) = 0, that is a(u, v) = 0 for every v ∈ H¹₀(Ω), with u ≥ 0 almost everywhere. Then on every ball with B(x₀, 16√n r) ⊆ Ω,

u(y) ≤ C u(x) for almost every x, y ∈ B(x₀, r),

that is, ess sup_{B(x₀, r)} u ≤ C ess inf_{B(x₀, r)} u. The constant does not depend on u or the ball.

TauCeti.PDE.exists_ae_ae_value_le_mul_value.{u_1} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {lam Lam : ℝ}
  [Nonempty ι] :
  ∃ C,
    0 < C ∧
      ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
        {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
        {x₀ : EuclideanSpace ℝ ι} {r : ℝ},
        TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
          MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
            (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)), TauCeti.PDE.energyFormH1 a 0 0 u ↑v = 0) →
              (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value u) x) →
                Metric.ball x₀ (16 * √↑(Fintype.card ι) * r) ⊆ ↑Omega →
                  ∀ᵐ (x : EuclideanSpace ℝ ι) (y :
                    EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ r),
                    ↑↑(TauCeti.W1p.value u) y ≤ C * ↑↑(TauCeti.W1p.value u) x

Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_ae_ae_value_le_mul_value.

Sources

LeanTauCeti.PDE.exists_ae_ae_value_le_mul_value

Uses 5

Proof usesThe L² Leibniz estimate · Moser's weak Harnack inequality · The Sobolev inequality on W^{1,p}_0 of a ball · TauCeti.Wkp · The zero-forcing Caccioppoli inequality for a positive truncation of a weak subsolution

TheoremThe Mihlin–Hörmander multiplier theorem on `Lᵖ`#

Let V be a real inner product space of finite dimension n ≥ 1, let 2N > n and 1 < p < ∞. There is a constant C such that for every symbol m of temperate growth satisfying Mihlin's condition of order N with constant A,

‖D^k m ξ‖ ≤ A / ‖ξ‖ ^ k for every k ≤ N and every ξ ≠ 0,

the Fourier multiplier 𝓕⁻ (m • 𝓕 f) of the tempered distribution of any f ∈ Lᵖ(V, F) is an Lᵖ function g with ‖g‖_p ≤ C A ‖f‖_p.

TauCeti.exists_fourierMultiplierCLM_eq_and_norm_le_of_norm_iteratedFDeriv_le.{u_1, u_2}
  {V : Type u_1} {F : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [FiniteDimensional ℝ V] [MeasurableSpace V]
  [BorelSpace V] [CompleteSpace F] [Nontrivial V] {N : ℕ} (hN : Module.finrank ℝ V < 2 * N)
  {p : ENNReal} [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ {m : V → ℂ},
      Function.HasTemperateGrowth m →
        ∀ {A : NNReal},
          (∀ k ≤ N, ∀ (ξ : V), ξ ≠ 0 → ‖iteratedFDeriv ℝ k m ξ‖ ≤ ↑A / ‖ξ‖ ^ k) →
            ∀ (f : ↥(MeasureTheory.Lp F p MeasureTheory.volume)),
              ∃ g,
                (TemperedDistribution.fourierMultiplierCLM F m)
                      (MeasureTheory.Lp.toTemperedDistribution f) =
                    MeasureTheory.Lp.toTemperedDistribution g ∧
                  ‖g‖ ≤ ↑C * ↑A * ‖f‖

Lean

Formalized in Tau Ceti as TauCeti.exists_fourierMultiplierCLM_eq_and_norm_le_of_norm_iteratedFDeriv_le.

Other forms

The Mihlin–Hörmander multiplier theorem. Formalized in Tau Ceti as TauCeti.exists_eLpNorm_fourierMultiplierCLM_le_of_norm_iteratedFDeriv_le.

TauCeti.exists_eLpNorm_fourierMultiplierCLM_le_of_norm_iteratedFDeriv_le.{u_1, u_2} {V : Type u_1}
  {F : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup F]
  [InnerProductSpace ℂ F] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
  [CompleteSpace F] [Nontrivial V] {N : ℕ} (hN : Module.finrank ℝ V < 2 * N) {p : ENNReal}
  (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ {m : V → ℂ},
      ContDiffOn ℝ (↑⊤) m {0}ᶜ →
        ∀ {A : NNReal},
          (∀ k ≤ N, ∀ (ξ : V), ξ ≠ 0 → ‖iteratedFDeriv ℝ k m ξ‖ ≤ ↑A / ‖ξ‖ ^ k) →
            ∀ (m' : ↥(MeasureTheory.Lp ℂ ⊤ MeasureTheory.volume)),
              ↑↑m' =ᵐ[MeasureTheory.volume] m →
                ∀ (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)),
                  MeasureTheory.eLpNorm (↑↑((MeasureTheory.Lp.fourierMultiplierCLM F m') f)) p
                      MeasureTheory.volume ≤
                    ↑C * ↑A * MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume

Sources

LeanTauCeti.exists_fourierMultiplierCLM_eq_and_norm_le_of_norm_iteratedFDeriv_le · TauCeti.exists_eLpNorm_fourierMultiplierCLM_le_of_norm_iteratedFDeriv_le

Uses 5 · Used by 1

Proof usesThe Calderón–Zygmund theorem · Hölder's inequality for the integral of a product · Plancherel bound for Fourier multipliers · Plancherel's theorem for the inverse Fourier transform of Schwartz functions · The weighted Plancherel bound

Used byThe Calderón–Zygmund inequality for the Cauchy–Riemann operator

TheoremThe Calderón–Zygmund estimate `‖D²u‖_p ≤ C ‖Δu‖_p`#

Let 1 < p < ∞, and let V be a finite-dimensional real inner product space with its volume measure. There is a constant C with

‖D²u‖_{Lᵖ} ≤ C ‖Δu‖_{Lᵖ}

for every Schwartz function u on V with values in a complex Hilbert space, where D²u is the second Fréchet derivative of u.

TauCeti.exists_eLpNorm_iteratedFDeriv_two_le_eLpNorm_laplacian.{u_1, u_2} {F : Type u_1}
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] {V : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V]
  [BorelSpace V] {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (u : SchwartzMap V F),
      MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 ⇑u) p MeasureTheory.volume ≤
        ↑C * MeasureTheory.eLpNorm (⇑(Laplacian.laplacian u)) p MeasureTheory.volume

Lean

Formalized in Tau Ceti as TauCeti.exists_eLpNorm_iteratedFDeriv_two_le_eLpNorm_laplacian.

Other forms

The Calderón–Zygmund estimate ‖D²u‖_p ≤ C ‖Δu‖_p for real functions. Formalized in Tau Ceti as TauCeti.exists_eLpNorm_iteratedFDeriv_two_le_eLpNorm_laplacian_real.

TauCeti.exists_eLpNorm_iteratedFDeriv_two_le_eLpNorm_laplacian_real.{u_2} {V : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V]
  [BorelSpace V] {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (u : SchwartzMap V ℝ),
      MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 ⇑u) p MeasureTheory.volume ≤
        ↑C * MeasureTheory.eLpNorm (⇑(Laplacian.laplacian u)) p MeasureTheory.volume

The Calderón–Zygmund estimate for a second directional derivative. Formalized in Tau Ceti as TauCeti.exists_eLpNorm_lineDerivOp_lineDerivOp_le_eLpNorm_laplacian.

TauCeti.exists_eLpNorm_lineDerivOp_lineDerivOp_le_eLpNorm_laplacian.{u_1} {n : ℕ} {F : Type u_1}
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (v w : EuclideanSpace ℝ (Fin n))
  {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (u : SchwartzMap (EuclideanSpace ℝ (Fin n)) F),
      MeasureTheory.eLpNorm (⇑(LineDeriv.lineDerivOp v (LineDeriv.lineDerivOp w u))) p
          MeasureTheory.volume ≤
        ↑C * MeasureTheory.eLpNorm (⇑(Laplacian.laplacian u)) p MeasureTheory.volume

The Calderón–Zygmund estimate for constant coefficients in W^{2,p}(ℝⁿ). Formalized in Tau Ceti as TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_sum_mul_inner_eq.

TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_sum_mul_inner_eq {n : ℕ} {p : ENNReal}
  [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ {A : Matrix (Fin n) (Fin n) ℝ} {lam : ℝ},
      0 < lam →
        (∀ (ξ : EuclideanSpace ℝ (Fin n)), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) →
          ∀ (u : TauCeti.Wkp MeasureTheory.volume ⊤ p 2)
            (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑⊤))),
            (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                ∑ i,
                    ∑ j,
                      A i j *
                        inner ℝ
                          ((↑↑(TauCeti.Wkp.iteratedGradient 1 u) x) (EuclideanSpace.single i 1))
                          (EuclideanSpace.single j 1) =
                  ↑↑f x) →
              ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ ↑C / lam * ‖f‖

The Calderón–Zygmund estimate for constant-coefficient operators. Formalized in Tau Ceti as TauCeti.PDE.exists_eLpNorm_iteratedFDeriv_two_le_eLpNorm_sum_smul_fderiv_fderiv.

TauCeti.PDE.exists_eLpNorm_iteratedFDeriv_two_le_eLpNorm_sum_smul_fderiv_fderiv.{u_1} {n : ℕ}
  {p : ENNReal} {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
  (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ {A : Matrix (Fin n) (Fin n) ℝ} {lam : ℝ},
      0 < lam →
        (∀ (ξ : EuclideanSpace ℝ (Fin n)), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) →
          ∀ (u : SchwartzMap (EuclideanSpace ℝ (Fin n)) F),
            MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 ⇑u) p MeasureTheory.volume ≤
              ENNReal.ofReal (↑C / lam) *
                MeasureTheory.eLpNorm
                  (fun x =>
                    ∑ i,
                      ∑ j,
                        A i j •
                          ((fderiv ℝ (fderiv ℝ ⇑u) x) (EuclideanSpace.single i 1))
                            (EuclideanSpace.single j 1))
                  p MeasureTheory.volume

The Calderón–Zygmund estimate for constant-coefficient operators, real-valued form. Formalized in Tau Ceti as TauCeti.PDE.exists_eLpNorm_iteratedFDeriv_two_le_eLpNorm_sum_smul_fderiv_fderiv_real.

TauCeti.PDE.exists_eLpNorm_iteratedFDeriv_two_le_eLpNorm_sum_smul_fderiv_fderiv_real {n : ℕ}
  {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ {A : Matrix (Fin n) (Fin n) ℝ} {lam : ℝ},
      0 < lam →
        (∀ (ξ : EuclideanSpace ℝ (Fin n)), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) →
          ∀ (u : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℝ),
            MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 ⇑u) p MeasureTheory.volume ≤
              ENNReal.ofReal (↑C / lam) *
                MeasureTheory.eLpNorm
                  (fun x =>
                    ∑ i,
                      ∑ j,
                        A i j •
                          ((fderiv ℝ (fderiv ℝ ⇑u) x) (EuclideanSpace.single i 1))
                            (EuclideanSpace.single j 1))
                  p MeasureTheory.volume

The Calderón–Zygmund estimate for strong solutions in W^{2,p}. Formalized in Tau Ceti as TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_traceCLM_compLpL_eq.

TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_traceCLM_compLpL_eq.{u_1} {p : ENNReal}
  [Fact (1 ≤ p)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (u : TauCeti.Wkp MeasureTheory.volume ⊤ p 2)
      (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑⊤))),
      (ContinuousLinearMap.compLpL p (MeasureTheory.volume.restrict ↑⊤) (TauCeti.traceCLM ℝ V))
            (TauCeti.Wkp.iteratedGradient 1 u) =
          f →
        ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ ↑C * ‖f‖

The Calderón–Zygmund estimate for the Hessian multiplier. Formalized in Tau Ceti as TauCeti.exists_eLpNorm_fourierMultiplierCLM_hessianSymbolLp_le.

TauCeti.exists_eLpNorm_fourierMultiplierCLM_hessianSymbolLp_le.{u_1} {n : ℕ} {F : Type u_1}
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (hn : 3 ≤ n)
  (v w : EuclideanSpace ℝ (Fin n)) {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (f : ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)),
      MeasureTheory.eLpNorm
          (↑↑((MeasureTheory.Lp.fourierMultiplierCLM F (TauCeti.hessianSymbolLp v w)) f)) p
          MeasureTheory.volume ≤
        ↑C * MeasureTheory.eLpNorm (↑↑f) p MeasureTheory.volume

The Calderón–Zygmund estimate in W^{2,p}(ℝⁿ) for coefficients of small local oscillation. Formalized in Tau Ceti as TauCeti.PDE.exists_norm_iteratedGradient_le_of_sum_mul_inner_eq_of_dist_lt_abs_sub_le.

TauCeti.PDE.exists_norm_iteratedGradient_le_of_sum_mul_inner_eq_of_dist_lt_abs_sub_le {n : ℕ}
  {p : ENNReal} [Fact (1 ≤ p)] (hn : 0 < n) (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C δ,
    0 < δ ∧
      ∀ {lam Λ ρ : ℝ},
        0 < lam →
          0 < ρ →
            ∀ {a : EuclideanSpace ℝ (Fin n) → Matrix (Fin n) (Fin n) ℝ},
              MeasureTheory.AEStronglyMeasurable a MeasureTheory.volume →
                (∀ (x ξ : EuclideanSpace ℝ (Fin n)),
                    lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp) →
                  (∀ (x : EuclideanSpace ℝ (Fin n)) (i j : Fin n), |a x i j| ≤ Λ) →
                    (∀ (x y : EuclideanSpace ℝ (Fin n)),
                        dist x y < ρ → ∀ (i j : Fin n), |a x i j - a y i j| ≤ δ * lam) →
                      ∀ (u : TauCeti.Wkp MeasureTheory.volume ⊤ p 2)
                        (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑⊤))),
                        (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                            ∑ i,
                                ∑ j,
                                  a x i j *
                                    inner ℝ
                                      ((↑↑(TauCeti.Wkp.iteratedGradient 1 u) x)
                                        (EuclideanSpace.single i 1))
                                      (EuclideanSpace.single j 1) =
                              ↑↑f x) →
                          ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤
                            ↑C * (‖f‖ / lam + (1 + Λ / lam) ^ 2 / ρ ^ 2 * ‖TauCeti.Wkp.value 2 u‖)

The Calderón–Zygmund estimate in W^{2,p}(ℝⁿ) for coefficients of small oscillation. Formalized in Tau Ceti as TauCeti.PDE.exists_norm_iteratedGradient_le_mul_norm_of_sum_mul_inner_eq_of_abs_sub_le.

TauCeti.PDE.exists_norm_iteratedGradient_le_mul_norm_of_sum_mul_inner_eq_of_abs_sub_le {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) →
            ∀ {a : EuclideanSpace ℝ (Fin n) → Matrix (Fin n) (Fin n) ℝ}
              {s : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ},
              IsClosed s →
                ε ≤ δ * lam →
                  (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                      x ∈ s → ∀ (i j : Fin n), |a x i j - A i j| ≤ ε) →
                    ∀ (u : TauCeti.Wkp MeasureTheory.volume ⊤ p 2)
                      (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑⊤))),
                      (∀ᵐ (x : EuclideanSpace ℝ (Fin n)), x ∉ s → ↑↑(TauCeti.Wkp.value 2 u) x = 0) →
                        (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                            ∑ i,
                                ∑ j,
                                  a x i j *
                                    inner ℝ
                                      ((↑↑(TauCeti.Wkp.iteratedGradient 1 u) x)
                                        (EuclideanSpace.single i 1))
                                      (EuclideanSpace.single j 1) =
                              ↑↑f x) →
                          ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ ↑C / lam * ‖f‖

The Calderón–Zygmund estimate in W^{2,p}(ℝⁿ) for uniformly continuous coefficients. Formalized in Tau Ceti as TauCeti.PDE.exists_norm_iteratedGradient_le_of_sum_mul_inner_eq_of_uniformContinuous.

TauCeti.PDE.exists_norm_iteratedGradient_le_of_sum_mul_inner_eq_of_uniformContinuous {n : ℕ}
  {p : ENNReal} [Fact (1 ≤ p)] (hn : 0 < n) (hp : 1 < p) (hp_top : p ≠ ⊤)
  {a : EuclideanSpace ℝ (Fin n) → Matrix (Fin n) (Fin n) ℝ} (ha : UniformContinuous a) {lam Λ : ℝ}
  (hlam : 0 < lam)
  (hA : ∀ (x ξ : EuclideanSpace ℝ (Fin n)), lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp)
  (haΛ : ∀ (x : EuclideanSpace ℝ (Fin n)) (i j : Fin n), |a x i j| ≤ Λ) :
  ∃ C,
    ∀ (u : TauCeti.Wkp MeasureTheory.volume ⊤ p 2)
      (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑⊤))),
      (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
          ∑ i,
              ∑ j,
                a x i j *
                  inner ℝ ((↑↑(TauCeti.Wkp.iteratedGradient 1 u) x) (EuclideanSpace.single i 1))
                    (EuclideanSpace.single j 1) =
            ↑↑f x) →
        ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ C * (‖f‖ + ‖TauCeti.Wkp.value 2 u‖)

The Calderón–Zygmund estimate in W^{2,p}, against test functions. Formalized in Tau Ceti as TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_integral_laplacian_smul_eq.

TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_integral_laplacian_smul_eq.{u_1} {p : ENNReal}
  [Fact (1 ≤ p)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (u : TauCeti.Wkp MeasureTheory.volume ⊤ p 2)
      (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑⊤))),
      (∀ (φ : TestFunction ⊤ ℝ ⊤),
          ∫ (x : V), Laplacian.laplacian (⇑φ) x • ↑↑(TauCeti.Wkp.value 2 u) x =
            ∫ (x : V), φ x • ↑↑f x) →
        ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ ↑C * ‖f‖

The Calderón–Zygmund estimate on a half-space for coefficients of small oscillation. Formalized in Tau Ceti as TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_traceCLM_comp_eq_of_norm_sub_le_of_normalHalfSpace.

TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_traceCLM_comp_eq_of_norm_sub_le_of_normalHalfSpace.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C δ,
    0 < δ ∧
      ∀ (a : ℝ) {A : WithLp 2 (ℝ × E) → WithLp 2 (ℝ × E) →L[ℝ] WithLp 2 (ℝ × E)}
        {s : Set (WithLp 2 (ℝ × E))} {μ ε : ℝ},
        0 < μ →
          IsClosed s →
            ε ≤ δ * μ →
              (∀ᵐ (x :
                  WithLp 2 (ℝ × E)) ∂MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a),
                  x ∈ s → ‖A x - μ • 1‖ ≤ ε) →
                ∀ (u : TauCeti.Wkp MeasureTheory.volume (TauCeti.normalHalfSpace a) p 2)
                  (f :
                    ↥(MeasureTheory.Lp ℝ p
                        (MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a)))),
                  TauCeti.Wkp.firstOrder 1 u ∈
                      TauCeti.w1p0Submodule MeasureTheory.volume (TauCeti.normalHalfSpace a) p →
                    (∀ᵐ (x :
                        WithLp 2
                          (ℝ × E)) ∂MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a),
                        x ∉ s → ↑↑(TauCeti.Wkp.value 2 u) x = 0) →
                      (∀ᵐ (x :
                          WithLp 2
                            (ℝ × E)) ∂MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a),
                          (TauCeti.traceCLM ℝ (WithLp 2 (ℝ × E)))
                              (A x ∘SL ↑↑(TauCeti.Wkp.iteratedGradient 1 u) x) =
                            ↑↑f x) →
                        ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ ↑C / μ * ‖f‖

The Calderón–Zygmund estimate on a half-space, against test functions. Formalized in Tau Ceti as TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_integral_laplacian_smul_eq_of_normalHalfSpace.

TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_integral_laplacian_smul_eq_of_normalHalfSpace.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (a : ℝ) (u : TauCeti.Wkp MeasureTheory.volume (TauCeti.normalHalfSpace a) p 2)
      (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a)))),
      TauCeti.Wkp.firstOrder 1 u ∈
          TauCeti.w1p0Submodule MeasureTheory.volume (TauCeti.normalHalfSpace a) p →
        (∀ (φ : TestFunction (TauCeti.normalHalfSpace a) ℝ ⊤),
            ∫ (x : WithLp 2 (ℝ × E)), Laplacian.laplacian (⇑φ) x • ↑↑(TauCeti.Wkp.value 2 u) x =
              ∫ (x : WithLp 2 (ℝ × E)), φ x • ↑↑f x) →
          ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ ↑C * ‖f‖

The Calderón–Zygmund estimate on a half-space, for constant coefficients. Formalized in Tau Ceti as TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_traceCLM_comp_eq_of_normalHalfSpace.

TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_traceCLM_comp_eq_of_normalHalfSpace.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ {A : WithLp 2 (ℝ × E) →L[ℝ] WithLp 2 (ℝ × E)} {lam : ℝ},
      0 < lam →
        (∀ (ξ : WithLp 2 (ℝ × E)), lam * ‖ξ‖ ^ 2 ≤ inner ℝ (A ξ) ξ) →
          ∀ (a : ℝ) (u : TauCeti.Wkp MeasureTheory.volume (TauCeti.normalHalfSpace a) p 2)
            (f :
              ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a)))),
            TauCeti.Wkp.firstOrder 1 u ∈
                TauCeti.w1p0Submodule MeasureTheory.volume (TauCeti.normalHalfSpace a) p →
              (∀ᵐ (x :
                  WithLp 2 (ℝ × E)) ∂MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a),
                  (TauCeti.traceCLM ℝ (WithLp 2 (ℝ × E)))
                      (A ∘SL ↑↑(TauCeti.Wkp.iteratedGradient 1 u) x) =
                    ↑↑f x) →
                ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ ↑C / lam * ‖f‖

The Calderón–Zygmund estimate on a half-space, for strong solutions. Formalized in Tau Ceti as TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_traceCLM_compLpL_eq_of_normalHalfSpace.

TauCeti.exists_norm_iteratedGradient_le_mul_norm_of_traceCLM_compLpL_eq_of_normalHalfSpace.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {p : ENNReal} [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) :
  ∃ C,
    ∀ (a : ℝ) (u : TauCeti.Wkp MeasureTheory.volume (TauCeti.normalHalfSpace a) p 2)
      (f : ↥(MeasureTheory.Lp ℝ p (MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a)))),
      TauCeti.Wkp.firstOrder 1 u ∈
          TauCeti.w1p0Submodule MeasureTheory.volume (TauCeti.normalHalfSpace a) p →
        (ContinuousLinearMap.compLpL p (MeasureTheory.volume.restrict ↑(TauCeti.normalHalfSpace a))
                (TauCeti.traceCLM ℝ (WithLp 2 (ℝ × E))))
              (TauCeti.Wkp.iteratedGradient 1 u) =
            f →
          ‖TauCeti.Wkp.iteratedGradient 1 u‖ ≤ ↑C * ‖f‖

Sources

Uses 6

Statement usesTauCeti.Wkp

Proof usesThe Calderón–Zygmund theorem · The interior Calderón–Zygmund estimate for continuous coefficients · Meyers–Serrin: H = W in W^{k,p}(Ω) · Rademacher's theorem for locally Lipschitz functions · Radial fundamental theorem of calculus

TheoremExistence of weak solutions for linear parabolic equations #

Let V ↪ H ↪ V* be a Gelfand triple: V a separable Hilbert space, H a Hilbert space and ι : V →L[ℝ] H with dense range. Let A(t) : V →L[ℝ] V* be weakly measurable (t ↦ A(t) u v almost everywhere strongly measurable on (a, b) for all u, v), bounded by Λ and satisfy Gårding's inequality α ‖v‖² - β ‖ι v‖² ≤ A(t) v v with α > 0, for almost every t ∈ (a, b). Then for every f ∈ L²(a, b; V*) and u₀ ∈ H there is a weak solution of

u' + A(t) u = f, u(a) = u₀:

a u ∈ L²(a, b; V) such that u' = f - A u ∈ L²(a, b; V*) is the weak time derivative of ι.gelfandDual ∘ ι ∘ u on (a, b), and a representative w of ι ∘ u continuous on [a, b] with w a = u₀. For β ≥ 0 it is unique: see TauCeti.HasWeakLineDerivOn.eqOn_of_gelfandDual and TauCeti.HasWeakLineDerivOn.ae_eq_of_gelfandDual.

TauCeti.exists_hasWeakLineDerivOn_gelfandDual.{u_1, u_2} {V : Type u_1} {H : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  {A : ℝ → V →L[ℝ] StrongDual ℝ V} {f : ℝ → StrongDual ℝ V} {a b α β Λ : ℝ} {ι : V →L[ℝ] H}
  [CompleteSpace V] [TopologicalSpace.SeparableSpace V] [CompleteSpace H] (hι : DenseRange ⇑ι)
  (hab : a ≤ b)
  (hA :
    ∀ (u v : V),
      MeasureTheory.AEStronglyMeasurable (fun t => ((A t) u) v)
        (MeasureTheory.volume.restrict (Set.Ioo a b)))
  (hA_bound : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ‖A t‖ ≤ Λ) (hα : 0 < α)
  (hA_garding :
    ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b),
      ∀ (v : V), α * ‖v‖ ^ 2 - β * ‖ι v‖ ^ 2 ≤ ((A t) v) v)
  (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioo a b))) (u₀ : H) :
  ∃ u w,
    MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (Set.Ioo a b)) ∧
      MeasureTheory.MemLp (fun t => f t - (A t) (u t)) 2
          (MeasureTheory.volume.restrict (Set.Ioo a b)) ∧
        TauCeti.HasWeakLineDerivOn MeasureTheory.volume { carrier := Set.Ioo a b, is_open' := ⋯ }
            (fun t => ι.gelfandDual (ι (u t))) (fun t => f t - (A t) (u t)) 1 ∧
          ContinuousOn w (Set.Icc a b) ∧
            (fun t => ι (u t)) =ᵐ[MeasureTheory.volume.restrict (Set.Ioo a b)] w ∧ w a = u₀

Lean

Formalized in Tau Ceti as TauCeti.exists_hasWeakLineDerivOn_gelfandDual.

Sources

LeanTauCeti.exists_hasWeakLineDerivOn_gelfandDual

Uses 4

Proof usesThe fundamental theorem of calculus for a continuous representative · The fundamental theorem of calculus for weak derivatives · Lions' representation theorem · Pettis' theorem in a separable inner product space

DefinitionTauCeti.Wkp #

The arbitrary-order, real-valued weak Sobolev space W^{k,p}(Ω). At order zero this is Lᵖ(Ω); order one is W1p; every further order adjoins the weak derivative of the highest derivative field from the preceding order.

TauCeti.Wkp.{u} {E : Type u} [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)] : ℕ → Type u

Lean

Formalized in Tau Ceti as TauCeti.Wkp.

Sources

LeanTauCeti.Wkp

Used by 19

Used byDe Giorgi's interior oscillation estimate · De Giorgi's theorem: Hölder continuity of weak solutions · Existence and uniqueness for the Dirichlet problem with c ≥ 0 · Moser's crossover estimate (TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le) · Moser's Harnack inequality · Moser's reverse Hölder inequality for powers of a positive supersolution · The Calderón–Zygmund estimate ‖D²u‖_p ≤ C ‖Δu‖_p · The logarithmic Caccioppoli inequality · The Caccioppoli inequality · The interior Calderón–Zygmund estimate for continuous coefficients · The interior Schauder estimate on small balls · Moser's lower bound from small negative powers · Stampacchia's global bound · The localized Calderón–Zygmund estimate for coefficients of small oscillation · The sharp Poincaré inequality on an interval · The zero-forcing Caccioppoli inequality for a positive truncation of a weak subsolution · De Giorgi's isoperimetric inequality · Meyers–Serrin: H = W in W^{k,p}(Ω) · The Poincaré–Wirtinger inequality on a ball

DefinitionThe trace operator of a bounded Lipschitz domain #

The trace operator of a bounded Lipschitz domain, W^{1,p}(Ω) → Lᵖ(frontier Ω) for p < ∞ and normalized dim E-dimensional Euclidean Hausdorff measure on the frontier. It is characterized by TauCeti.W1p.frontierTrace_ae_eq_of_continuousOn and TauCeti.W1p.eq_frontierTrace: it is the unique bounded linear operator sending every function continuous up to the boundary to its restriction to the frontier.

TauCeti.W1p.frontierTrace.{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)]
  (hp : p ≠ ⊤) (hΩ : (↑Ω).IsLipschitzDomainWith L) (hb : Bornology.IsBounded ↑Ω) :
  ↥(TauCeti.W1p MeasureTheory.volume Ω p) →L[ℝ]
    ↥(MeasureTheory.Lp ℝ p
        ((MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E)).restrict
          (frontier ↑Ω)))

Lean

Formalized in Tau Ceti as TauCeti.W1p.frontierTrace.

Sources

LeanTauCeti.W1p.frontierTrace

Uses 1

Proof usesRademacher's theorem for locally Lipschitz functions

DefinitionTauCeti.CkHolderSpace #

The space of bounded C^k maps whose iterated Fréchet derivatives through order k are bounded and whose k-th iterated derivative is globally α-Hölder. Its norm is

∑_{i ≤ k} ‖D^i f‖_∞ + [D^k f]_α.

TauCeti.CkHolderSpace.{u, v} (k : ℕ) (α : NNReal) (E : Type u) (F : Type v) [NormedAddCommGroup E]
  [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u v)

Lean

Formalized in Tau Ceti as TauCeti.CkHolderSpace.

Sources

LeanTauCeti.CkHolderSpace

Used by 1

Used byThe global Schauder estimate on the whole space

TheoremDe Giorgi's interior oscillation estimate #

Let n ≥ 1 be the dimension. There are α ∈ (0, 1] and C > 0, depending only on λ, Λ, the dimension and the normalization of the additive Haar measure mu, such that the following holds. Let a be measurable and uniformly elliptic on Ω with constants λ, Λ, and let u ∈ H¹(Ω) be a weak solution of -∂ᵢ(aⁱʲ ∂ⱼu) = 0. If B(x₀, R) ⊆ Ω and 0 < r ≤ R/2, then almost everywhere on B(x₀, r) the function u takes values in an interval of length

C (r / R)^α R^{-n/2} ‖u‖_{L²(B(x₀, R))}.

This is the a-priori estimate behind the interior Hölder continuity of weak solutions, and the case b = 0 of TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral_drift.

TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral.{u_1} {ι : Type u_1}
  [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  [mu.IsAddHaarMeasure] {lam Lam : ℝ} [Nonempty ι] :
  ∃ α C,
    0 < α ∧
      α ≤ 1 ∧
        0 < C ∧
          ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
            {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
            {x₀ : EuclideanSpace ℝ ι} {R r : ℝ},
            TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
              MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
                (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)), TauCeti.PDE.energyFormH1 a 0 0 u ↑v = 0) →
                  0 < r →
                    r ≤ R / 2 →
                      Metric.ball x₀ R ⊆ ↑Omega →
                        ∃ m',
                          ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ r),
                            ↑↑(TauCeti.W1p.value u) x ∈
                              Set.Icc m'
                                (m' +
                                  C * (r / R) ^ α *
                                    (R ^ (-↑(Fintype.card ι) / 2) *
                                      √(∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R,
                                          ↑↑(TauCeti.W1p.value u) x ^ 2 ∂mu)))

Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral.

Other forms

De Giorgi's interior oscillation estimate with a drift. Formalized in Tau Ceti as TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral_drift.

TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral_drift.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  [mu.IsAddHaarMeasure] {lam Lam : ℝ} [Nonempty ι] (σ : ℝ) :
  ∃ α C,
    0 < α ∧
      α ≤ 1 ∧
        0 < C ∧
          ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
            {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
            {beta : ℝ} {u : ↥(TauCeti.W1p mu Omega 2)} {x₀ : EuclideanSpace ℝ ι} {R r : ℝ},
            TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
              MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
                MeasureTheory.AEStronglyMeasurable b (mu.restrict ↑Omega) →
                  (∀ x ∈ ↑Omega, ‖b x‖ ≤ beta) →
                    (∀ (v : ↥(TauCeti.W1p0 mu Omega 2)), TauCeti.PDE.energyFormH1 a b 0 u ↑v = 0) →
                      0 < r →
                        r ≤ R / 2 →
                          Metric.ball x₀ R ⊆ ↑Omega →
                            beta * R ≤ σ * lam →
                              ∃ m',
                                ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ r),
                                  ↑↑(TauCeti.W1p.value u) x ∈
                                    Set.Icc m'
                                      (m' +
                                        C * (r / R) ^ α *
                                          (R ^ (-↑(Fintype.card ι) / 2) *
                                            √(∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R,
                                                ↑↑(TauCeti.W1p.value u) x ^ 2 ∂mu)))

De Giorgi's interior oscillation estimate with a right-hand side. Formalized in Tau Ceti as TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_add_of_memLp.

TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_add_of_memLp.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  [Nonempty ι] {lam Lam : ℝ} {r : NNReal} (hr : 1 < r) (hrn : ↑(Fintype.card ι) < 2 * ↑r) :
  ∃ α C,
    0 < α ∧
      α ≤ 1 ∧
        0 < C ∧
          ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
            {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {f : EuclideanSpace ℝ ι → ℝ}
            {u : ↥(TauCeti.W1p mu Omega 2)} {x₀ : EuclideanSpace ℝ ι} {R s : ℝ},
            TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
              MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
                MeasureTheory.MemLp f (↑r) (mu.restrict (Metric.ball x₀ R)) →
                  (∀ (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) →
                    0 < s →
                      s ≤ R / 2 →
                        Metric.ball x₀ R ⊆ ↑Omega →
                          ∃ m',
                            ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ s),
                              ↑↑(TauCeti.W1p.value u) x ∈
                                Set.Icc m'
                                  (m' +
                                    C * (s / R) ^ α *
                                      (R ^ (-↑(Fintype.card ι) / 2) *
                                          √(∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R,
                                              ↑↑(TauCeti.W1p.value u) x ^ 2 ∂mu) +
                                        R ^ (2 - ↑(Fintype.card ι) / ↑r) *
                                            (MeasureTheory.eLpNorm f (↑r)
                                                (mu.restrict (Metric.ball x₀ R))).toReal /
                                          lam))

Sources

LeanTauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral · TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_rpow_mul_sqrt_setIntegral_drift · TauCeti.PDE.exists_ae_value_mem_Icc_add_mul_rpow_mul_add_of_memLp

Uses 8 · Used by 1

Proof usesThe L² Leibniz estimate · The Caccioppoli inequality · De Giorgi's isoperimetric inequality · Hölder's inequality for Young's exponents · The Sobolev inequality on W^{1,p}_0 of a ball · Stampacchia's global bound · TauCeti.Wkp · The zero-forcing Caccioppoli inequality for a positive truncation of a weak subsolution

Used byDe Giorgi's theorem: Hölder continuity of weak solutions

TheoremThe logarithmic Caccioppoli inequality #

Let a be measurable and uniformly elliptic on Ω with constants 0 < λ ≤ Λ, and let u ∈ H¹(Ω) be a weak supersolution of -∂ᵢ(aⁱʲ ∂ⱼu) ≥ 0, that is a(u, v) ≥ 0 for every nonnegative v ∈ H¹₀(Ω), with u ≥ ε almost everywhere for some ε > 0. Then for every smooth ψ compactly supported in Ω,

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

The integrand on the left is ψ² ‖∇ log u‖², and the right side depends on neither u nor ε.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_div_value_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)) {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)
  {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcpt : HasCompactSupport ψ)
  (hts : tsupport ψ ⊆ ↑Omega) :
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
      ψ x ^ 2 * (‖↑↑(TauCeti.W1p.gradient u) x‖ / ↑↑(TauCeti.W1p.value u) x) ^ 2 ∂mu ≤
    (2 * Lam / lam) ^ 2 * ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ‖gradient ψ x‖ ^ 2 ∂mu

Lean

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

Other forms

The logarithmic Caccioppoli inequality. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_div_sq_le.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_div_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)
  {ψ : EuclideanSpace ℝ ι → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hcpt : HasCompactSupport ψ)
  (hts : tsupport ψ ⊆ ↑Omega) {m : ℝ} (hm : 0 < m)
  (hum : ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (tsupport ψ), m ≤ ↑↑(TauCeti.W1p.value u) x) :
  ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
      ψ x ^ 2 * ‖↑↑(TauCeti.W1p.gradient u) x‖ ^ 2 / ↑↑(TauCeti.W1p.value u) x ^ 2 ∂mu ≤
    (2 * Lam / lam) ^ 2 * ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, ‖gradient ψ x‖ ^ 2 ∂mu

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

TauCeti.PDE.exists_setIntegral_ball_norm_gradient_sq_div_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)}
        {x₀ : EuclideanSpace ℝ ι} {r R m : ℝ},
        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) →
                  0 ≤ TauCeti.PDE.energyFormH1 a 0 0 u ↑v) →
              0 < r →
                r < R →
                  Metric.ball x₀ R ⊆ ↑Omega →
                    0 < m →
                      (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ R),
                          m ≤ ↑↑(TauCeti.W1p.value u) x) →
                        ∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ r,
                            ‖↑↑(TauCeti.W1p.gradient u) x‖ ^ 2 / ↑↑(TauCeti.W1p.value u) x ^ 2 ∂mu ≤
                          (2 * Lam / lam) ^ 2 * (c / (R - r)) ^ 2 * mu.real (Metric.ball x₀ R)

Sources

LeanTauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_div_value_sq_le · TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_sq_div_sq_le · TauCeti.PDE.exists_setIntegral_ball_norm_gradient_sq_div_sq_le

Uses 2 · Used by 1

Proof usesThe Caccioppoli inequality · TauCeti.Wkp

Used byMoser's crossover estimate (TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le)

TheoremMoser's crossover estimate (`TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le`)#

There are constants c > 0 and K, depending only on the dimension n ≥ 1, with the following property. Let a be measurable and uniformly elliptic on Ω with constants 0 < λ ≤ Λ, and let u ∈ H¹(Ω) be a weak supersolution of -∂ᵢ(aⁱʲ ∂ⱼu) ≥ 0 with u ≥ ε almost everywhere for some ε > 0. Then for every ball with B(x₀, 4√n r) ⊆ Ω and every exponent |p| ≤ c λ/Λ,

⨍_{B(x₀, r)} u^p · ⨍_{B(x₀, r)} u^{-p} ≤ K.

The bound is independent of u, ε, λ, Λ and the ball.

TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] [Nonempty ι] :
  ∃ c,
    0 < c ∧
      ∃ K,
        ∀ (mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)) [inst : mu.IsAddHaarMeasure]
          {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
          {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {lam Lam : ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
          {ε : ℝ} {x₀ : EuclideanSpace ℝ ι} {r p : ℝ},
          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) →
                    0 ≤ TauCeti.PDE.energyFormH1 a 0 0 u ↑v) →
                0 < ε →
                  (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, ε ≤ ↑↑(TauCeti.W1p.value u) x) →
                    Metric.ball x₀ (4 * √↑(Fintype.card ι) * r) ⊆ ↑Omega →
                      |p| ≤ c * (lam / Lam) →
                        (⨍ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ r,
                              ↑↑(TauCeti.W1p.value u) x ^ p ∂mu) *
                            ⨍ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ r,
                              ↑↑(TauCeti.W1p.value u) x ^ (-p) ∂mu ≤
                          K

Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le.

Sources

LeanTauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le

Uses 4 · Used by 1

Proof usesThe logarithmic Caccioppoli inequality · Moser's crossover estimate (TauCeti.exists_setLIntegral_exp_mul_mul_setLIntegral_exp_neg_mul_ball_le) · The Poincaré–Wirtinger inequality on a ball · TauCeti.Wkp

Used byMoser's weak Harnack inequality

TheoremMoser's reverse Hölder inequality for powers of a positive supersolution #

There is a constant C ≥ 0, depending only on the dimension, with the following property. Let a be measurable and uniformly elliptic on Ω with constants 0 < λ ≤ Λ, and suppose that W^{1,2}_0(Ω) satisfies the Sobolev inequality ‖v‖_q ≤ S ‖∇v‖₂. Let u ∈ H¹(Ω) be a weak supersolution of -∂ᵢ(aⁱʲ ∂ⱼu) ≥ 0, that is a(u, v) ≥ 0 for every nonnegative v ∈ H¹₀(Ω), with u ≥ ε almost everywhere for some ε > 0. Then for every p < 1 and all concentric balls B(x₀, r) ⊂ B(x₀, ρ) ⊆ Ω,

‖u^{p/2}‖_{L^q(B(x₀, r))} ≤ S C (1 + |p| Λ / ((1 - p) λ)) / (ρ - r) · ‖u^{p/2}‖_{L²(B(x₀, ρ))}.

The constant depends on neither u nor ε.

TauCeti.PDE.exists_eLpNorm_rpow_le_mul_eLpNorm_rpow.{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 : ℝ} {q : ENNReal} {S : NNReal}
        {u : ↥(TauCeti.W1p mu Omega 2)} {ε p : ℝ} {x₀ : EuclideanSpace ℝ ι} {r ρ : ℝ},
        TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
          MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
            (∀ v ∈ TauCeti.w1p0Submodule mu Omega 2,
                MeasureTheory.eLpNorm (↑↑(TauCeti.W1p.value v)) q (mu.restrict ↑Omega) ≤
                  ↑S * ‖TauCeti.W1p.gradient v‖ₑ) →
              (∀ (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) →
                0 < ε →
                  (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, ε ≤ ↑↑(TauCeti.W1p.value u) x) →
                    p < 1 →
                      0 < r →
                        r < ρ →
                          Metric.ball x₀ ρ ⊆ ↑Omega →
                            MeasureTheory.eLpNorm (fun x => ↑↑(TauCeti.W1p.value u) x ^ (p / 2)) q
                                (mu.restrict (Metric.ball x₀ r)) ≤
                              ↑S *
                                  ENNReal.ofReal (C * (1 + |p| * Lam / ((1 - p) * lam)) / (ρ - r)) *
                                MeasureTheory.eLpNorm (fun x => ↑↑(TauCeti.W1p.value u) x ^ (p / 2))
                                  2 (mu.restrict (Metric.ball x₀ ρ))

Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_eLpNorm_rpow_le_mul_eLpNorm_rpow.

Sources

LeanTauCeti.PDE.exists_eLpNorm_rpow_le_mul_eLpNorm_rpow

Uses 3 · Used by 1

Proof usesThe L² Leibniz estimate · The Caccioppoli inequality · TauCeti.Wkp

Used byMoser's weak Harnack inequality

TheoremMoser's weak Harnack inequality #

Let n ≥ 1 be the dimension. For every exponent s > 0 with (n - 2) s < n, that is s < n/(n - 2) when n ≥ 3 and s arbitrary when n ≤ 2, there is C > 0, depending only on λ, Λ, s, the dimension and the normalization of the additive Haar measure mu, with the following property. Let a be measurable and uniformly elliptic on Ω with constants λ, Λ, and let u ∈ H¹(Ω) be a nonnegative weak supersolution of -∂ᵢ(aⁱʲ ∂ⱼu) ≥ 0, that is a(u, v) ≥ 0 for every nonnegative v ∈ H¹₀(Ω). Then on every ball with B(x₀, 8√n r) ⊆ Ω,

(⨍_{B(x₀, r)} u^s)^{1/s} ≤ C u(x) for almost every x ∈ B(x₀, r),

and u^s is integrable on B(x₀, r), so the left side is a genuine average even for s > 2. The constant does not depend on u or the ball.

TauCeti.PDE.exists_ae_setAverage_rpow_rpow_inv_le_mul_value.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {lam Lam : ℝ} [Nonempty ι] {s : ℝ} (hs : 0 < s)
  (hsn : (↑(Fintype.card ι) - 2) * s < ↑(Fintype.card ι)) :
  ∃ C,
    0 < C ∧
      ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
        {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
        {x₀ : EuclideanSpace ℝ ι} {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) →
                  0 ≤ TauCeti.PDE.energyFormH1 a 0 0 u ↑v) →
              (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(TauCeti.W1p.value u) x) →
                Metric.ball x₀ (8 * √↑(Fintype.card ι) * r) ⊆ ↑Omega →
                  MeasureTheory.IntegrableOn (fun y => ↑↑(TauCeti.W1p.value u) y ^ s)
                      (Metric.ball x₀ r) mu ∧
                    ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ r),
                      (⨍ (y : EuclideanSpace ℝ ι) in Metric.ball x₀ r,
                            ↑↑(TauCeti.W1p.value u) y ^ s ∂mu) ^
                          s⁻¹ ≤
                        C * ↑↑(TauCeti.W1p.value u) x

Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_ae_setAverage_rpow_rpow_inv_le_mul_value.

Other forms

Moser's weak Harnack inequality at a small exponent. Formalized in Tau Ceti as TauCeti.PDE.exists_pos_ae_setAverage_rpow_rpow_inv_le_mul_value.

TauCeti.PDE.exists_pos_ae_setAverage_rpow_rpow_inv_le_mul_value.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {lam Lam : ℝ} [Nonempty ι] :
  ∃ p₀,
    0 < p₀ ∧
      p₀ ≤ 2 ∧
        ∃ C,
          0 < C ∧
            ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
              {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(TauCeti.W1p mu Omega 2)}
              {x₀ : EuclideanSpace ℝ ι} {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) →
                        0 ≤ TauCeti.PDE.energyFormH1 a 0 0 u ↑v) →
                    (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega,
                        0 ≤ ↑↑(TauCeti.W1p.value u) x) →
                      Metric.ball x₀ (8 * √↑(Fintype.card ι) * r) ⊆ ↑Omega →
                        ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ r),
                          (⨍ (y : EuclideanSpace ℝ ι) in Metric.ball x₀ (2 * r),
                                ↑↑(TauCeti.W1p.value u) y ^ p₀ ∂mu) ^
                              p₀⁻¹ ≤
                            C * ↑↑(TauCeti.W1p.value u) x

Sources

LeanTauCeti.PDE.exists_ae_setAverage_rpow_rpow_inv_le_mul_value · TauCeti.PDE.exists_pos_ae_setAverage_rpow_rpow_inv_le_mul_value

Uses 4 · Used by 1

Proof usesMoser's crossover estimate (TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le) · Moser's lower bound from small negative powers · Moser's reverse Hölder inequality for powers of a positive supersolution · The Sobolev inequality on W^{1,p}_0 of a ball

Used byMoser's Harnack inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Partial differential equations

TheoremExistence and uniqueness for the Dirichlet problem with c ≥ 0#

Lean

Sources

TheoremDe Giorgi's theorem: Hölder continuity of weak solutions#

Lean

Other forms

Sources

TheoremMoser's Harnack inequality#

Lean

Sources

TheoremThe Mihlin–Hörmander multiplier theorem on Lᵖ#

Lean

Other forms

Sources

TheoremThe Calderón–Zygmund estimate ‖D²u‖_p ≤ C ‖Δu‖_p#

Lean

Other forms

Sources

TheoremExistence of weak solutions for linear parabolic equations#

Lean

Sources

DefinitionTauCeti.Wkp#

Lean

Sources

DefinitionThe trace operator of a bounded Lipschitz domain#

Lean

Sources

DefinitionTauCeti.CkHolderSpace#

Lean

Sources

TheoremDe Giorgi's interior oscillation estimate#

Lean

Other forms

Sources

TheoremThe logarithmic Caccioppoli inequality#

Lean

Other forms

Sources

TheoremMoser's crossover estimate (TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le)#

Lean

Sources

TheoremMoser's reverse Hölder inequality for powers of a positive supersolution#

Lean

Sources

TheoremMoser's weak Harnack inequality#

Lean

Other forms

Sources

TheoremExistence and uniqueness for the Dirichlet problem with `c ≥ 0`#

TheoremDe Giorgi's theorem: Hölder continuity of weak solutions #

TheoremMoser's Harnack inequality #

TheoremThe Mihlin–Hörmander multiplier theorem on `Lᵖ`#

TheoremThe Calderón–Zygmund estimate `‖D²u‖_p ≤ C ‖Δu‖_p`#

TheoremExistence of weak solutions for linear parabolic equations #

DefinitionTauCeti.Wkp #

DefinitionThe trace operator of a bounded Lipschitz domain #

DefinitionTauCeti.CkHolderSpace #

TheoremDe Giorgi's interior oscillation estimate #

TheoremThe logarithmic Caccioppoli inequality #

TheoremMoser's crossover estimate (`TauCeti.PDE.exists_setAverage_rpow_mul_setAverage_rpow_neg_le`)#

TheoremMoser's reverse Hölder inequality for powers of a positive supersolution #

TheoremMoser's weak Harnack inequality #