The localized Calderón–Zygmund… to The zero-forcing Caccioppoli…

TheoremThe localized Calderón–Zygmund estimate for coefficients of small oscillation #

Let 0 < n and 1 < p < ∞. There are constants C and δ > 0, depending only on n and p, with the following property. Let A be a matrix with λ ‖ξ‖² ≤ ξᵀ A ξ and 0 < λ, let Ω be open, and let ζ be smooth with compact support in Ω, ‖∇ζ‖ ≤ M₁ and ‖D²ζ‖ ≤ M₂. Let a be a measurable matrix-valued coefficient on Ω with |aᵢⱼ(x) - Aᵢⱼ| ≤ ε and |aᵢⱼ(x)| ≤ Λ for almost every x in the support of ζ, where ε ≤ δ λ and 0 ≤ Λ. Then every u ∈ W^{2,p}(Ω) with ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼu = f almost everywhere on Ω, with f ∈ Lᵖ(Ω), satisfies

‖ζ D²u‖_{Lᵖ(Ω)} ≤ (C / λ) ‖ζ f‖_{Lᵖ(Ω)} + (C n² Λ / λ + 1) (2 M₁ ‖∇u‖_{Lᵖ(Ω)} + M₂ ‖u‖_{Lᵖ(Ω)}),

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

TauCeti.PDE.exists_lpNorm_smul_iteratedGradient_le_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) →
            ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin n))}
              {zeta : EuclideanSpace ℝ (Fin n) → ℝ} {M₁ M₂ : ℝ},
              ContDiff ℝ (↑⊤) zeta →
                HasCompactSupport zeta →
                  tsupport zeta ⊆ ↑Omega →
                    (∀ (x : EuclideanSpace ℝ (Fin n)), ‖gradient zeta x‖ ≤ M₁) →
                      (∀ (x : EuclideanSpace ℝ (Fin n)), ‖fderiv ℝ (gradient zeta) x‖ ≤ M₂) →
                        ∀ {a : EuclideanSpace ℝ (Fin n) → Matrix (Fin n) (Fin n) ℝ} {ε Λ : ℝ},
                          MeasureTheory.AEStronglyMeasurable a
                              (MeasureTheory.volume.restrict ↑Omega) →
                            ε ≤ δ * lam →
                              (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                                  x ∈ tsupport zeta → ∀ (i j : Fin n), |a x i j - A i j| ≤ ε) →
                                0 ≤ Λ →
                                  (∀ᵐ (x : EuclideanSpace ℝ (Fin n)),
                                      x ∈ tsupport zeta → ∀ (i j : Fin n), |a x i j| ≤ Λ) →
                                    ∀ (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) =
                                            ↑↑f x) →
                                        MeasureTheory.lpNorm
                                            (fun x =>
                                              zeta x • ↑↑(TauCeti.Wkp.iteratedGradient 1 u) x)
                                            p (MeasureTheory.volume.restrict ↑Omega) ≤
                                          ↑C / lam *
                                              MeasureTheory.lpNorm (fun x => zeta x * ↑↑f x) p
                                                (MeasureTheory.volume.restrict ↑Omega) +
                                            (↑C / lam * ↑n ^ 2 * Λ + 1) *
                                              (2 * M₁ *
                                                  ‖TauCeti.Wkp.iteratedGradient 0
                                                      (TauCeti.Wkp.lowerOrder 1 u)‖ +
                                                M₂ * ‖TauCeti.Wkp.value 2 u‖)

Uses 1 · Used by 1

Statement usesTauCeti.Wkp

Used byThe interior Calderón–Zygmund estimate for continuous coefficients

TheoremMoser's lower bound from small negative powers #

For every 0 < p ≤ 2 and every positive weak supersolution in any dimension n ≥ 1, u⁻¹ ≤ D R^{-n/p} (∫_{B(x₀, R)} u⁻ᵖ)^{1/p} almost everywhere on B(x₀, R/2). The constant depends only on λ, Λ, p, the dimension and Haar normalization, not on the positive lower bound for u. No boundary regularity is required.

TauCeti.PDE.exists_ae_inv_value_le_mul_rpow_mul_setIntegral_rpow.{u_1} {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure]
  {lam Lam : ℝ} [Nonempty ι] {p : ℝ} (hp : 0 < p) (hp2 : p ≤ 2) :
  ∃ D,
    0 < D ∧
      ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
        {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {u : ↥(TauCeti.W1p mu Omega 2)} {m : ℝ}
        {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) →
              0 < m →
                (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, m ≤ ↑↑(TauCeti.W1p.value u) x) →
                  0 < R →
                    Metric.ball x₀ R ⊆ ↑Omega →
                      ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict (Metric.ball x₀ (R / 2)),
                        (↑↑(TauCeti.W1p.value u) x)⁻¹ ≤
                          D * R ^ (-↑(Fintype.card ι) / p) *
                            (∫ (x : EuclideanSpace ℝ ι) in Metric.ball x₀ R,
                                (↑↑(TauCeti.W1p.value u) x)⁻¹ ^ p ∂mu) ^
                              p⁻¹

Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_ae_inv_value_le_mul_rpow_mul_setIntegral_rpow.

Sources

LeanTauCeti.PDE.exists_ae_inv_value_le_mul_rpow_mul_setIntegral_rpow

Uses 4 · Used by 1

Proof usesThe L² Leibniz estimate · 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

Used byMoser's weak Harnack inequality

TheoremThe parabolic Hölder estimate of the Cauchy heat potential #

If g is continuous and α-Hölder with constant H, its Cauchy potential is α-Hölder on parabolic space-time, whose distance is ‖x - x'‖ + √|t - s|, with constant H (1 + M_α). Here M_α = ∫ ‖y‖^α K_1(y) dy is TauCeti.heatKernelMoment, which depends only on α and the dimension. Continuity is automatic when α > 0 (HolderWith.continuous).

TauCeti.holderWith_heatCauchyPotential.{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] {g : E → F} {H α : NNReal}
  (hg : HolderWith H α g) (hgc : Continuous g) :
  HolderWith (H * (1 + TauCeti.heatKernelMoment E α)) α fun p =>
    TauCeti.heatCauchyPotential g p.time p.space

Lean

Formalized in Tau Ceti as TauCeti.holderWith_heatCauchyPotential.

Sources

LeanTauCeti.holderWith_heatCauchyPotential

Used by 1

Used byThe value-field parabolic Hölder estimate for the Duhamel potential

TheoremPerron's theorem #

Let Ω be a bounded open set, let g be bounded above on frontier Ω, and suppose the Perron family of g is nonempty. Then the Perron solution TauCeti.perronSolution Ω g is harmonic in Ω.

In Perron's setting of bounded boundary data the family is nonempty by TauCeti.perronFamily_nonempty.

TauCeti.harmonicOnNhd_perronSolution.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : Set E} {g : E → ℝ} [MeasurableSpace E]
  [BorelSpace E] (hΩ : IsOpen Ω) (hb : Bornology.IsBounded Ω) (hg : BddAbove (g '' frontier Ω))
  (hne : (TauCeti.perronFamily Ω g).Nonempty) :
  InnerProductSpace.HarmonicOnNhd (TauCeti.perronSolution Ω g) Ω

Lean

Formalized in Tau Ceti as TauCeti.harmonicOnNhd_perronSolution.

Sources

LeanTauCeti.harmonicOnNhd_perronSolution

Uses 4

Proof usesThe du Bois-Reymond lemma · Green's second identity against a test function · Hopf's boundary-point lemma · The limit in Harnack's convergence theorem is harmonic

TheoremPointwise Gårding inequality #

With a nonnegative mass coefficient (c ≥ 0), the diagonal of the jet form is bounded below by (λ/2)‖∇u‖² − (β²/2λ)|u|². The ellipticity floor λ‖∇u‖² pays for the drift term via Young's inequality, leaving half the floor and a mass defect proportional to β²/λ. Integrating over Ω this is Gårding's inequality a(u, u) ≥ (λ/2)‖∇u‖²_{L²} − (β²/2λ)‖u‖²_{L²}.

TauCeti.PDE.garding_energyIntegrand_self_of_bounds.{u_1} {n : Type u_1} [Fintype n] {lam beta : ℝ}
  (hlam : 0 < lam) {A : Matrix n n ℝ} {b₀ : EuclideanSpace ℝ n} {c₀ : ℝ}
  (hQ : ∀ (ξ : EuclideanSpace ℝ n), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) (hb : ‖b₀‖ ≤ beta)
  (hc : 0 ≤ c₀) (U : ℝ × EuclideanSpace ℝ n) :
  lam / 2 * ‖U.2‖ ^ 2 - beta ^ 2 / (2 * lam) * U.1 ^ 2 ≤ ((TauCeti.PDE.energyIntegrand A b₀ c₀) U) U

Lean

Formalized in Tau Ceti as TauCeti.PDE.garding_energyIntegrand_self_of_bounds.

Sources

LeanTauCeti.PDE.garding_energyIntegrand_self_of_bounds

TheoremThe Rayleigh principle for the Dirichlet problem #

On a nonempty bounded domain with a symmetric energy form, the first Dirichlet eigenvalue is the minimum of the Rayleigh quotient

a(u, u) / ‖u‖²_{L²(Ω)}

over the u ∈ H¹₀(Ω) with nonzero L² value; the minimum is attained at an eigenfunction. Boundedness of Ω enters only through the attainment, by way of Rellich--Kondrachov: the inequality alone is TauCeti.PDE.firstDirichletEigenvalue_mul_norm_value_sq_le.

TauCeti.PDE.isLeast_rayleighQuotient_firstDirichletEigenvalue.{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)
  (hsymm :
    ∀ (u v : ↥(TauCeti.W1p0 mu Omega 2)),
      TauCeti.PDE.energyFormH1 a b c ↑u ↑v = TauCeti.PDE.energyFormH1 a b c ↑v ↑u)
  (hOmega_nonempty : (↑Omega).Nonempty) :
  IsLeast
    {r |
      ∃ u,
        TauCeti.W1p.value ↑u ≠ 0 ∧
          TauCeti.PDE.energyFormH1 a b c ↑u ↑u / ‖TauCeti.W1p.value ↑u‖ ^ 2 = r}
    (TauCeti.PDE.firstDirichletEigenvalue hcoeff hcoercive)

Lean

Formalized in Tau Ceti as TauCeti.PDE.isLeast_rayleighQuotient_firstDirichletEigenvalue.

Sources

LeanTauCeti.PDE.isLeast_rayleighQuotient_firstDirichletEigenvalue

Uses 2

Proof usesThe Rayleigh principle · Rellich–Kondrachov on bounded Lipschitz domains

TheoremSchauder estimate for a Hessian supported in a ball #

Let 0 < α < 1. There is C > 0, depending only on dimension and α, with the following property. Let a be α-Hölder entrywise with constant L on the support ball, and suppose a x₀ has ellipticity bounds λ, Λ, with λ > 0. Put

Lu = ∑ᵢⱼ aᵢⱼ ∂ᵢⱼu.

If the Hessian of a global C² function u is supported in the closed ball of radius R about x₀ and is globally α-Hölder a priori, then the scale condition

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

where κ = C (Λ / λ)^(1 + (n+1)/4 + α/2), implies the estimate

[D²u]ᵅ ≤ 2 κ ([Lu]ᵅ / λ + ((n+1)² 2ᵅ L / λ |Bᵣ|⁻¹/² + r^(-(n+1)/2-α)) ‖D²u‖₂).

Thus no uniform comparison of a with one constant matrix is assumed: the support condition allows the coefficients to be retracted to the support ball and frozen at its centre.

TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_of_support_subset_closedBall {n : ℕ} {α : NNReal}
  (hα : 0 < α) (hα1 : α < 1) :
  ∃ C,
    0 < C ∧
      ∀ {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ}
        {x₀ : EuclideanSpace ℝ (Fin (n + 1))} {lam Lam : ℝ},
        0 < lam →
          (∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))), lam * ‖ξ‖ ^ 2 ≤ (a x₀).toQuadraticForm' ξ.ofLp) →
            (∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))),
                (a x₀).toQuadraticForm' ξ.ofLp ≤ Lam * ‖ξ‖ ^ 2) →
              ∀ {L K : NNReal} {R r : ℝ},
                0 ≤ R →
                  0 < r →
                    2 * (C * (Lam / lam) ^ (1 + (↑n + 1) / 4 + ↑α / 2)) * (↑n + 1) ^ 2 *
                          (↑L * R ^ ↑α + ↑L * 2 ^ ↑α * r ^ ↑α) ≤
                        lam →
                      (∀ (i j : Fin (n + 1)),
                          HolderOnWith L α (fun x => a x i j) (Metric.closedBall x₀ R)) →
                        ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ},
                          ContDiff ℝ 2 u →
                            MemHolder α (iteratedFDeriv ℝ 2 u) →
                              Function.support (iteratedFDeriv ℝ 2 u) ⊆ Metric.closedBall x₀ R →
                                (HolderWith K α fun x =>
                                    ∑ i,
                                      ∑ j,
                                        a x i j •
                                          ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1))
                                            (EuclideanSpace.single j 1)) →
                                  HolderWith
                                    (2 * (C * (Lam / lam) ^ (1 + (↑n + 1) / 4 + ↑α / 2)) *
                                        (↑K / lam +
                                          ((↑n + 1) ^ 2 * (↑L * 2 ^ ↑α) / lam *
                                                (MeasureTheory.volume (Metric.ball 0 r) ^
                                                    (-2⁻¹)).toReal +
                                              r ^ (-((↑n + 1) / 2 + ↑α))) *
                                            (MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 u) 2
                                                MeasureTheory.volume).toReal)).toNNReal
                                    α (iteratedFDeriv ℝ 2 u)

Informally uses

The interior Schauder estimate on small balls

Lean

Formalized in Tau Ceti as TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_of_support_subset_closedBall.

Sources

LeanTauCeti.PDE.exists_holderWith_iteratedFDeriv_two_of_support_subset_closedBall

Uses 1 · Used by 1

Proof usesHölder's bound on an average

Used byThe interior Schauder estimate on small balls

TheoremThe sharp Poincaré inequality on an interval #

For every u ∈ H¹₀(a, b),

(π / (b - a))² ∫_a^b u² ≤ ∫_a^b |u'|²,

and (π / (b - a))² is the largest constant for which this holds: it is the first Dirichlet eigenvalue (TauCeti.PDE.firstDirichletEigenvalue_laplacian_intervalDomain).

TauCeti.PDE.isGreatest_mul_norm_value_sq_le_energyFormH1_intervalDomain {a b : ℝ} (hab : a < b) :
  IsGreatest
    {C |
      ∀ (u : ↥(TauCeti.W1p0 MeasureTheory.volume (TauCeti.PDE.intervalDomain a b) 2)),
        C * ‖TauCeti.W1p.value ↑u‖ ^ 2 ≤ TauCeti.PDE.energyFormH1 (fun x => 1) 0 0 ↑u ↑u}
    ((Real.pi / (b - a)) ^ 2)

Lean

Formalized in Tau Ceti as TauCeti.PDE.isGreatest_mul_norm_value_sq_le_energyFormH1_intervalDomain.

Sources

LeanTauCeti.PDE.isGreatest_mul_norm_value_sq_le_energyFormH1_intervalDomain

Uses 6

Proof usesGreen's first identity against H¹₀(Ω) · Gårding's inequality on H¹(Ω) · The Poincaré inequality on a ball · The Rayleigh lower bound · Rellich–Kondrachov on bounded Lipschitz domains · TauCeti.Wkp

TheoremThe spatial Hölder estimate of the Cauchy heat potential #

If g is continuous and α-Hölder with constant H, then so is every time slice of its Cauchy potential, with the same constant.

HolderWith.heatCauchyPotential.{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] {g : E → F} {H α : NNReal} (hg : HolderWith H α g)
  (hgc : Continuous g) (t : ℝ) : HolderWith H α (TauCeti.heatCauchyPotential g t)

Lean

Formalized in Tau Ceti as HolderWith.heatCauchyPotential.

Sources

LeanHolderWith.heatCauchyPotential

TheoremThe spectral theorem for the Dirichlet problem #

on a bounded domain and for a symmetric energy form, the eigenvectors of the solution operator span a dense subspace of L²(Ω).

TauCeti.PDE.orthogonalComplement_iSup_eigenspaces_dirichletSolutionOperator_eq_bot.{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)
  (hsymm :
    ∀ (u v : ↥(TauCeti.W1p0 mu Omega 2)),
      TauCeti.PDE.energyFormH1 a b c ↑u ↑v = TauCeti.PDE.energyFormH1 a b c ↑v ↑u) :
  (⨆ nu, Module.End.eigenspace (↑(TauCeti.PDE.dirichletSolutionOperator hcoeff hcoercive)) nu)ᗮ = ⊥

Lean

Formalized in Tau Ceti as TauCeti.PDE.orthogonalComplement_iSup_eigenspaces_dirichletSolutionOperator_eq_bot.

Sources

LeanTauCeti.PDE.orthogonalComplement_iSup_eigenspaces_dirichletSolutionOperator_eq_bot

Uses 2

Proof usesRellich–Kondrachov on bounded Lipschitz domains · The spectral theorem for the solution operator

TheoremStampacchia's global bound #

Let Ω have finite measure, let a be measurable and uniformly elliptic on Ω with constants 0 < λ ≤ Λ, and let c be bounded, measurable and nonnegative. Suppose that W^{1,2}_0(Ω) satisfies a Sobolev inequality ‖v‖_{Lˢ} ≤ S ‖∇v‖_{L²}, and let f ∈ Lʳ(Ω) with s (1 - 1/r) > 2. If u ∈ H¹(Ω) is a weak subsolution of

-∂ᵢ(aⁱʲ ∂ⱼu) + c u ≤ f in Ω,

that is a(u, v) ≤ ∫_Ω f v for every nonnegative v ∈ H¹₀(Ω), and u ≤ k on ∂Ω for a level k ≥ 0, in the sense that (u - k)⁺ ∈ H¹₀(Ω), then almost everywhere in Ω

u ≤ k + 2 ^ (β / (β - 1)) S² ‖f‖_{Lʳ} / λ · |Ω| ^ (1 - 1/r - 2/s), where β = s (1 - 1/r) - 1.

No regularity of ∂Ω or of the coefficients beyond measurability is needed.

TauCeti.PDE.UniformlyEllipticOn.ae_value_le_add_of_forall_eLpNorm_le.{u_1} {ι : Type u_1}
  [Fintype ι] [DecidableEq ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)}
  [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
  {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {c : EuclideanSpace ℝ ι → ℝ} {lam Lam gamma : ℝ}
  (h : TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam)
  (ha : MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega))
  (hc : MeasureTheory.AEStronglyMeasurable c (mu.restrict ↑Omega))
  (hc_bound : ∀ x ∈ ↑Omega, ‖c x‖ ≤ gamma) (hc_nonneg : ∀ x ∈ ↑Omega, 0 ≤ c x)
  (hOmega : mu ↑Omega ≠ ⊤) {r s S : NNReal} (hr : 0 < r) (hrs : 2 < ↑s * (1 - (↑r)⁻¹))
  (hS :
    ∀ v ∈ TauCeti.w1p0Submodule mu Omega 2,
      MeasureTheory.eLpNorm (↑↑(TauCeti.W1p.value v)) (↑s) (mu.restrict ↑Omega) ≤
        ↑S * ‖TauCeti.W1p.gradient v‖ₑ)
  {f : EuclideanSpace ℝ ι → ℝ} (hf : MeasureTheory.MemLp f (↑r) (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 c u ↑v ≤
          ∫ (x : EuclideanSpace ℝ ι) in ↑Omega, f x * ↑↑(TauCeti.W1p.value ↑v) x ∂mu)
  {k : ℝ} (hk : 0 ≤ k)
  (hboundary :
    TauCeti.W1p.posPartAbove
        TauCeti.PDE.UniformlyEllipticOn.ae_value_le_add_of_forall_eLpNorm_le._proof_1 hk u ∈
      TauCeti.w1p0Submodule mu Omega 2) :
  ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega,
    ↑↑(TauCeti.W1p.value u) x ≤
      k +
        2 ^ ((↑s * (1 - (↑r)⁻¹) - 1) / (↑s * (1 - (↑r)⁻¹) - 2)) * ↑S ^ 2 *
              (MeasureTheory.eLpNorm f (↑r) (mu.restrict ↑Omega)).toReal /
            lam *
          mu.real ↑Omega ^ (1 - (↑r)⁻¹ - 2 / ↑s)

Lean

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

Other forms

Stampacchia's global bound, in every dimension. Formalized in Tau Ceti as TauCeti.PDE.exists_ae_value_le_add_mul_div_mul_rpow.

TauCeti.PDE.exists_ae_value_le_add_mul_div_mul_rpow.{u_1} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] [Nonempty ι] {r : NNReal}
  (hr : 1 < r) (hrn : ↑(Fintype.card ι) < 2 * ↑r) :
  ∃ C,
    0 < C ∧
      ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ ι)}
        {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {c : EuclideanSpace ℝ ι → ℝ} {lam Lam gamma : ℝ}
        {f : EuclideanSpace ℝ ι → ℝ} {u : ↥(TauCeti.W1p mu Omega 2)} {k : ℝ} (hk : 0 ≤ k),
        mu ↑Omega ≠ ⊤ →
          TauCeti.PDE.UniformlyEllipticOn (↑Omega) a lam Lam →
            MeasureTheory.AEStronglyMeasurable a (mu.restrict ↑Omega) →
              MeasureTheory.AEStronglyMeasurable c (mu.restrict ↑Omega) →
                (∀ x ∈ ↑Omega, ‖c x‖ ≤ gamma) →
                  (∀ x ∈ ↑Omega, 0 ≤ c x) →
                    MeasureTheory.MemLp f (↑r) (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 c u ↑v ≤
                              ∫ (x : EuclideanSpace ℝ ι) in ↑Omega,
                                f x * ↑↑(TauCeti.W1p.value ↑v) x ∂mu) →
                        TauCeti.W1p.posPartAbove
                              TauCeti.PDE.UniformlyEllipticOn.ae_value_le_add_of_forall_eLpNorm_le._proof_1
                              hk u ∈
                            TauCeti.w1p0Submodule mu Omega 2 →
                          ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega,
                            ↑↑(TauCeti.W1p.value u) x ≤
                              k +
                                C * (MeasureTheory.eLpNorm f (↑r) (mu.restrict ↑Omega)).toReal /
                                    lam *
                                  mu.real ↑Omega ^ (2 / ↑(Fintype.card ι) - (↑r)⁻¹)

Sources

LeanTauCeti.PDE.UniformlyEllipticOn.ae_value_le_add_of_forall_eLpNorm_le · TauCeti.PDE.exists_ae_value_le_add_mul_div_mul_rpow

Uses 4 · Used by 2

Proof usesHölder's inequality for Young's exponents · The Sobolev inequality on W^{1,p}_0 of a ball · Stampacchia's lemma · TauCeti.Wkp

Used byDe Giorgi's interior oscillation estimate · De Giorgi's theorem: Hölder continuity of weak solutions

TheoremThe temporal Hölder estimate of the Cauchy heat potential #

If g is continuous and α-Hölder with constant H, its Cauchy potential u satisfies ‖u(t, x) - u(s, x)‖ ≤ H M_α |t - s|^(α/2), where M_α = ∫ ‖y‖^α K_1(y) dy is TauCeti.heatKernelMoment.

TauCeti.norm_heatCauchyPotential_sub_heatCauchyPotential_le.{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] {g : E → F} {H α : NNReal}
  (hg : HolderWith H α g) (hgc : Continuous g) (t s : ℝ) (x : E) :
  ‖TauCeti.heatCauchyPotential g t x - TauCeti.heatCauchyPotential g s x‖ ≤
    ↑H * ↑(TauCeti.heatKernelMoment E α) * |t - s| ^ (↑α / 2)

Lean

Formalized in Tau Ceti as TauCeti.norm_heatCauchyPotential_sub_heatCauchyPotential_le.

Other forms

The temporal Hölder estimate for the Hessian of the Duhamel potential. Formalized in Tau Ceti as TauCeti.exists_holderOnWith_iteratedFDeriv_two_heatDuhamelPotential.

TauCeti.exists_holderOnWith_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α₂ : α < 2) :
  ∃ 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)) →
            ∀ (x : E),
              HolderOnWith (C * H) (α / 2)
                (fun t => iteratedFDeriv ℝ 2 (TauCeti.heatDuhamelPotential f t) x) (Set.Icc 0 T)

Sources

LeanTauCeti.norm_heatCauchyPotential_sub_heatCauchyPotential_le · TauCeti.exists_holderOnWith_iteratedFDeriv_two_heatDuhamelPotential

Uses 1 · Used by 1

Proof usesHölder bounds on the derivatives of a heat convolution

Used byDuhamel's principle in integrated form

TheoremThe value-field parabolic Hölder estimate for the Duhamel potential #

If the forcing is jointly measurable and its spatial slices on [0,T] are bounded by M and α-Hölder with constant H, where 0 < α ≤ 2, then its Duhamel potential is parabolically α-Hölder on the closed slab, with constant T H (1 + M_α) + M max(1,T). Here M_α is the heat-kernel moment. No temporal continuity of the forcing is assumed.

TauCeti.holderWith_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] {f : ℝ → E → F} {H α : NNReal}
  (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) {T M : NNReal}
  (hM : ∀ r ∈ Set.Icc 0 ↑T, ∀ (y : E), ‖f r y‖ ≤ ↑M) (hH : ∀ r ∈ Set.Icc 0 ↑T, HolderWith H α (f r))
  (hα : 0 < α) (hα₂ : α ≤ 2) :
  HolderWith (T * H * (1 + TauCeti.heatKernelMoment E α) + M * max 1 T) α fun p =>
    TauCeti.heatDuhamelPotential f (↑p).time (↑p).space

Lean

Formalized in Tau Ceti as TauCeti.holderWith_heatDuhamelPotential.

Sources

LeanTauCeti.holderWith_heatDuhamelPotential

Uses 1

Proof usesThe parabolic Hölder estimate of the Cauchy heat potential

TheoremThe Weitzenböck formula at a vortex #

where the vortex equation holds, L_x L_x* = (-Δ + P) ⊕ (-Δ_a + 1 / 8 + P / 2) with P = p² + q² = |α|² / 4. The section part is displayed in real coordinates as in gaugeFixedOperator_gaugeFixedAdjoint.

TauCeti.Vortex.gaugeFixedOperator_gaugeFixedAdjoint_of_equation_eq_zero
  {x η : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : DifferentiableAt ℝ x z)
  (hη : ContDiffAt ℝ 2 η z) (hsol : TauCeti.Vortex.equation x z = 0) :
  TauCeti.Vortex.gaugeFixedOperator x (TauCeti.Vortex.gaugeFixedAdjoint x η) z =
    !₂[-Laplacian.laplacian (fun w => (η w).ofLp 0) z +
        ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (η z).ofLp 0,
      -Laplacian.laplacian (fun w => (η w).ofLp 1) z +
        ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (η z).ofLp 1,
      -Laplacian.laplacian (fun w => (η w).ofLp 2) z +
            (1 / 8 + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 + (x z).ofLp 0 ^ 2 +
                (x z).ofLp 1 ^ 2) *
              (η z).ofLp 2 +
          ((fderiv ℝ (fun w => (x w).ofLp 0) z) 1 +
              (fderiv ℝ (fun w => (x w).ofLp 1) z) Complex.I) *
            (η z).ofLp 3 +
        2 *
          ((x z).ofLp 0 * (fderiv ℝ (fun w => (η w).ofLp 3) z) 1 +
            (x z).ofLp 1 * (fderiv ℝ (fun w => (η w).ofLp 3) z) Complex.I),
      -Laplacian.laplacian (fun w => (η w).ofLp 3) z +
            (1 / 8 + ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 + (x z).ofLp 0 ^ 2 +
                (x z).ofLp 1 ^ 2) *
              (η z).ofLp 3 -
          ((fderiv ℝ (fun w => (x w).ofLp 0) z) 1 +
              (fderiv ℝ (fun w => (x w).ofLp 1) z) Complex.I) *
            (η z).ofLp 2 -
        2 *
          ((x z).ofLp 0 * (fderiv ℝ (fun w => (η w).ofLp 2) z) 1 +
            (x z).ofLp 1 * (fderiv ℝ (fun w => (η w).ofLp 2) z) Complex.I)]

Lean

Formalized in Tau Ceti as TauCeti.Vortex.gaugeFixedOperator_gaugeFixedAdjoint_of_equation_eq_zero.

Other forms

The Weitzenböck formula for L_x L_x*. Formalized in Tau Ceti as TauCeti.Vortex.gaugeFixedOperator_gaugeFixedAdjoint.

TauCeti.Vortex.gaugeFixedOperator_gaugeFixedAdjoint {x η : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ}
  (hx : DifferentiableAt ℝ x z) (hη : ContDiffAt ℝ 2 η z) :
  TauCeti.Vortex.gaugeFixedOperator x (TauCeti.Vortex.gaugeFixedAdjoint x η) z =
    !₂[-Laplacian.laplacian (fun w => (η w).ofLp 0) z +
            ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (η z).ofLp 0 -
          (η z).ofLp 2 * (TauCeti.Vortex.equation x z).ofLp 2 +
        (η z).ofLp 3 * (TauCeti.Vortex.equation x z).ofLp 1,
      -Laplacian.laplacian (fun w => (η w).ofLp 1) z +
            ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (η z).ofLp 1 +
          (η z).ofLp 2 * (TauCeti.Vortex.equation x z).ofLp 1 +
        (η z).ofLp 3 * (TauCeti.Vortex.equation x z).ofLp 2,
      -Laplacian.laplacian (fun w => (η w).ofLp 2) z +
                ((TauCeti.Vortex.equation x z).ofLp 0 + 1 / 8 +
                        ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 +
                      (x z).ofLp 0 ^ 2 +
                    (x z).ofLp 1 ^ 2) *
                  (η z).ofLp 2 +
              ((fderiv ℝ (fun w => (x w).ofLp 0) z) 1 +
                  (fderiv ℝ (fun w => (x w).ofLp 1) z) Complex.I) *
                (η z).ofLp 3 +
            2 *
              ((x z).ofLp 0 * (fderiv ℝ (fun w => (η w).ofLp 3) z) 1 +
                (x z).ofLp 1 * (fderiv ℝ (fun w => (η w).ofLp 3) z) Complex.I) -
          (TauCeti.Vortex.equation x z).ofLp 2 * (η z).ofLp 0 +
        (TauCeti.Vortex.equation x z).ofLp 1 * (η z).ofLp 1,
      -Laplacian.laplacian (fun w => (η w).ofLp 3) z +
                ((TauCeti.Vortex.equation x z).ofLp 0 + 1 / 8 +
                        ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 +
                      (x z).ofLp 0 ^ 2 +
                    (x z).ofLp 1 ^ 2) *
                  (η z).ofLp 3 -
              ((fderiv ℝ (fun w => (x w).ofLp 0) z) 1 +
                  (fderiv ℝ (fun w => (x w).ofLp 1) z) Complex.I) *
                (η z).ofLp 2 -
            2 *
              ((x z).ofLp 0 * (fderiv ℝ (fun w => (η w).ofLp 2) z) 1 +
                (x z).ofLp 1 * (fderiv ℝ (fun w => (η w).ofLp 2) z) Complex.I) +
          (TauCeti.Vortex.equation x z).ofLp 1 * (η z).ofLp 0 +
        (TauCeti.Vortex.equation x z).ofLp 2 * (η z).ofLp 1]

The Weitzenböck formula for L_x* L_x at an arbitrary field. Formalized in Tau Ceti as TauCeti.Vortex.gaugeFixedAdjoint_gaugeFixedOperator.

TauCeti.Vortex.gaugeFixedAdjoint_gaugeFixedOperator {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ}
  (hx : DifferentiableAt ℝ x z) (hy : ContDiffAt ℝ 2 y z) :
  TauCeti.Vortex.gaugeFixedAdjoint x (TauCeti.Vortex.gaugeFixedOperator x y) z =
    !₂[-Laplacian.laplacian (fun w => (y w).ofLp 0) z +
            ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (y z).ofLp 0 +
          ((x z).ofLp 0 * (x z).ofLp 2 + (x z).ofLp 1 * (x z).ofLp 3 -
                (fderiv ℝ (fun w => (x w).ofLp 2) z) Complex.I +
              (fderiv ℝ (fun w => (x w).ofLp 3) z) 1) *
            (y z).ofLp 2 -
        ((x z).ofLp 1 * (x z).ofLp 2 - (x z).ofLp 0 * (x z).ofLp 3 +
              (fderiv ℝ (fun w => (x w).ofLp 2) z) 1 +
            (fderiv ℝ (fun w => (x w).ofLp 3) z) Complex.I) *
          (y z).ofLp 3,
      -Laplacian.laplacian (fun w => (y w).ofLp 1) z +
            ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (y z).ofLp 1 +
          ((x z).ofLp 1 * (x z).ofLp 2 - (x z).ofLp 0 * (x z).ofLp 3 +
                (fderiv ℝ (fun w => (x w).ofLp 2) z) 1 +
              (fderiv ℝ (fun w => (x w).ofLp 3) z) Complex.I) *
            (y z).ofLp 2 +
        ((x z).ofLp 0 * (x z).ofLp 2 + (x z).ofLp 1 * (x z).ofLp 3 -
              (fderiv ℝ (fun w => (x w).ofLp 2) z) Complex.I +
            (fderiv ℝ (fun w => (x w).ofLp 3) z) 1) *
          (y z).ofLp 3,
      -Laplacian.laplacian (fun w => (y w).ofLp 2) z +
                (TauCeti.Vortex.curvature x z + (x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2 +
                      (x z).ofLp 0 ^ 2 +
                    (x z).ofLp 1 ^ 2) *
                  (y z).ofLp 2 +
              ((fderiv ℝ (fun w => (x w).ofLp 0) z) 1 +
                  (fderiv ℝ (fun w => (x w).ofLp 1) z) Complex.I) *
                (y z).ofLp 3 +
            2 *
              ((x z).ofLp 0 * (fderiv ℝ (fun w => (y w).ofLp 3) z) 1 +
                (x z).ofLp 1 * (fderiv ℝ (fun w => (y w).ofLp 3) z) Complex.I) +
          ((x z).ofLp 0 * (x z).ofLp 2 + (x z).ofLp 1 * (x z).ofLp 3 -
                (fderiv ℝ (fun w => (x w).ofLp 2) z) Complex.I +
              (fderiv ℝ (fun w => (x w).ofLp 3) z) 1) *
            (y z).ofLp 0 +
        ((x z).ofLp 1 * (x z).ofLp 2 - (x z).ofLp 0 * (x z).ofLp 3 +
              (fderiv ℝ (fun w => (x w).ofLp 2) z) 1 +
            (fderiv ℝ (fun w => (x w).ofLp 3) z) Complex.I) *
          (y z).ofLp 1,
      -Laplacian.laplacian (fun w => (y w).ofLp 3) z +
                (TauCeti.Vortex.curvature x z + (x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2 +
                      (x z).ofLp 0 ^ 2 +
                    (x z).ofLp 1 ^ 2) *
                  (y z).ofLp 3 -
              ((fderiv ℝ (fun w => (x w).ofLp 0) z) 1 +
                  (fderiv ℝ (fun w => (x w).ofLp 1) z) Complex.I) *
                (y z).ofLp 2 -
            2 *
              ((x z).ofLp 0 * (fderiv ℝ (fun w => (y w).ofLp 2) z) 1 +
                (x z).ofLp 1 * (fderiv ℝ (fun w => (y w).ofLp 2) z) Complex.I) -
          ((x z).ofLp 1 * (x z).ofLp 2 - (x z).ofLp 0 * (x z).ofLp 3 +
                (fderiv ℝ (fun w => (x w).ofLp 2) z) 1 +
              (fderiv ℝ (fun w => (x w).ofLp 3) z) Complex.I) *
            (y z).ofLp 0 +
        ((x z).ofLp 0 * (x z).ofLp 2 + (x z).ofLp 1 * (x z).ofLp 3 -
              (fderiv ℝ (fun w => (x w).ofLp 2) z) Complex.I +
            (fderiv ℝ (fun w => (x w).ofLp 3) z) 1) *
          (y z).ofLp 1]

The Weitzenböck formula for L_x* L_x at a vortex. Formalized in Tau Ceti as TauCeti.Vortex.gaugeFixedAdjoint_gaugeFixedOperator_of_equation_eq_zero.

TauCeti.Vortex.gaugeFixedAdjoint_gaugeFixedOperator_of_equation_eq_zero
  {x y : ℂ → EuclideanSpace ℝ (Fin 4)} {z : ℂ} (hx : DifferentiableAt ℝ x z)
  (hy : ContDiffAt ℝ 2 y z) (hsol : TauCeti.Vortex.equation x z = 0) :
  TauCeti.Vortex.gaugeFixedAdjoint x (TauCeti.Vortex.gaugeFixedOperator x y) z =
    !₂[-Laplacian.laplacian (fun w => (y w).ofLp 0) z +
            ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (y z).ofLp 0 +
          (TauCeti.Vortex.covariantDerivative x z 1).im * (y z).ofLp 2 -
        (TauCeti.Vortex.covariantDerivative x z 1).re * (y z).ofLp 3,
      -Laplacian.laplacian (fun w => (y w).ofLp 1) z +
            ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) * (y z).ofLp 1 +
          (TauCeti.Vortex.covariantDerivative x z 1).re * (y z).ofLp 2 +
        (TauCeti.Vortex.covariantDerivative x z 1).im * (y z).ofLp 3,
      -Laplacian.laplacian (fun w => (y w).ofLp 2) z +
                (3 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 - 1 / 8 + (x z).ofLp 0 ^ 2 +
                    (x z).ofLp 1 ^ 2) *
                  (y z).ofLp 2 +
              ((fderiv ℝ (fun w => (x w).ofLp 0) z) 1 +
                  (fderiv ℝ (fun w => (x w).ofLp 1) z) Complex.I) *
                (y z).ofLp 3 +
            2 *
              ((x z).ofLp 0 * (fderiv ℝ (fun w => (y w).ofLp 3) z) 1 +
                (x z).ofLp 1 * (fderiv ℝ (fun w => (y w).ofLp 3) z) Complex.I) +
          (TauCeti.Vortex.covariantDerivative x z 1).im * (y z).ofLp 0 +
        (TauCeti.Vortex.covariantDerivative x z 1).re * (y z).ofLp 1,
      -Laplacian.laplacian (fun w => (y w).ofLp 3) z +
                (3 * ((x z).ofLp 2 ^ 2 + (x z).ofLp 3 ^ 2) / 2 - 1 / 8 + (x z).ofLp 0 ^ 2 +
                    (x z).ofLp 1 ^ 2) *
                  (y z).ofLp 3 -
              ((fderiv ℝ (fun w => (x w).ofLp 0) z) 1 +
                  (fderiv ℝ (fun w => (x w).ofLp 1) z) Complex.I) *
                (y z).ofLp 2 -
            2 *
              ((x z).ofLp 0 * (fderiv ℝ (fun w => (y w).ofLp 2) z) 1 +
                (x z).ofLp 1 * (fderiv ℝ (fun w => (y w).ofLp 2) z) Complex.I) -
          (TauCeti.Vortex.covariantDerivative x z 1).re * (y z).ofLp 0 +
        (TauCeti.Vortex.covariantDerivative x z 1).im * (y z).ofLp 1]

Sources

LeanTauCeti.Vortex.gaugeFixedOperator_gaugeFixedAdjoint_of_equation_eq_zero · TauCeti.Vortex.gaugeFixedOperator_gaugeFixedAdjoint · TauCeti.Vortex.gaugeFixedAdjoint_gaugeFixedOperator · TauCeti.Vortex.gaugeFixedAdjoint_gaugeFixedOperator_of_equation_eq_zero

TheoremThe zero-forcing Caccioppoli inequality for a positive truncation of a weak subsolution #

This is the specialization of UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_memLp to -∂ᵢ(aⁱʲ ∂ⱼu) ≤ 0.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_nonpos.{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) →
        TauCeti.PDE.energyFormH1 a 0 0 u ↑v ≤ 0)
  {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

Informally uses

The Caccioppoli inequality

Lean

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

Other forms

The zero-forcing Caccioppoli inequality for a nonnegative-level truncation with lower-order terms. Formalized in Tau Ceti as TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_nonpos.

TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_nonpos.{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)
  (hc_nonneg : ∀ x ∈ ↑Omega, 0 ≤ c x) {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 ≤ 0)
  {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

Sources

LeanTauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_of_nonpos · TauCeti.PDE.UniformlyEllipticOn.setIntegral_sq_mul_norm_gradient_posPartAbove_sq_le_lowerOrder_of_nonpos

Uses 1 · Used by 5

Proof usesTauCeti.Wkp

Used byDe Giorgi's interior oscillation estimate · De Giorgi's theorem: Hölder continuity of weak solutions · Moser's Harnack inequality · The Caccioppoli inequality · Moser's lower bound from small negative powers

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

The localized Calderón–Zygmund… to The zero-forcing Caccioppoli…

TheoremThe localized Calderón–Zygmund estimate for coefficients of small oscillation#

Informally uses

Lean

Sources

TheoremMoser's lower bound from small negative powers#

Lean

Sources

TheoremThe parabolic Hölder estimate of the Cauchy heat potential#

Lean

Sources

TheoremPerron's theorem#

Lean

Sources

TheoremPointwise Gårding inequality#

Lean

Sources

TheoremThe Rayleigh principle for the Dirichlet problem#

Lean

Sources

TheoremSchauder estimate for a Hessian supported in a ball#

Informally uses

Lean

Sources

TheoremThe sharp Poincaré inequality on an interval#

Lean

Sources

TheoremThe spatial Hölder estimate of the Cauchy heat potential#

Lean

Sources

TheoremThe spectral theorem for the Dirichlet problem#

Lean

Sources

TheoremStampacchia's global bound#

Lean

Other forms

Sources

TheoremThe temporal Hölder estimate of the Cauchy heat potential#

Lean

Other forms

Sources

TheoremThe value-field parabolic Hölder estimate for the Duhamel potential#

Lean

Sources

TheoremThe Weitzenböck formula at a vortex#

Lean

Other forms

Sources

TheoremThe zero-forcing Caccioppoli inequality for a positive truncation of a weak subsolution#

Informally uses

Lean

Other forms

Sources

TheoremThe localized Calderón–Zygmund estimate for coefficients of small oscillation #

TheoremMoser's lower bound from small negative powers #

TheoremThe parabolic Hölder estimate of the Cauchy heat potential #

TheoremPerron's theorem #

TheoremPointwise Gårding inequality #

TheoremThe Rayleigh principle for the Dirichlet problem #

TheoremSchauder estimate for a Hessian supported in a ball #

TheoremThe sharp Poincaré inequality on an interval #

TheoremThe spatial Hölder estimate of the Cauchy heat potential #

TheoremThe spectral theorem for the Dirichlet problem #

TheoremStampacchia's global bound #

TheoremThe temporal Hölder estimate of the Cauchy heat potential #

TheoremThe value-field parabolic Hölder estimate for the Duhamel potential #

TheoremThe Weitzenböck formula at a vortex #

TheoremThe zero-forcing Caccioppoli inequality for a positive truncation of a weak subsolution #