Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Scaled Caccioppoli inequality on concentric balls

Statement

In the setting of The Caccioppoli inequality for weak elliptic solutions, for concentric balls Br(x0)⋐BR(x0)⋐Ω one has, with the explicit scale, ∥Du∥L2(Br(x0))2≤C(1(R−r)2∥u∥L2(BR(x0))2+∥u∥L2(BR(x0))2+∥f∥L2(BR(x0))2), where C=C(n,θ,Ma,Mb,Mc) does not depend on r,R or on x0. The displayed (R−r)−2 is the scale used in the nested-ball iteration; the constants are not asserted to be sharp, and no claim is made as r→R.

Facts & Assumptions

Given: Countable Choice; the setting of The Caccioppoli inequality for weak elliptic solutions: an open set Ω⊆Rn, a scalar field K, coefficients aij,bi,c with ellipticity constant θ and bounds Ma,Mb,Mc, a class f∈Lloc2(Ω) and a local weak solution u∈H1(Ω) of Lu=f; and concentric balls Br(x0)⋐BR(x0)⋐Ω.

[F1]

Caccioppoli estimate: for every ball BR(x0)⋐Ω and every 0<r<R there is C=C(n,θ,Ma,Mb,Mc) with ∫Br(x0)∣Du∣2 dx≤C(1(R−r)2∫BR(x0)∣u∣2 dx+∫BR(x0)∣u∣2 dx+∫BR(x0)∣f∣2 dx). (The Caccioppoli inequality for weak elliptic solutions)

[F2]

L2 norms of classes are ∥w∥L2(A)=(∫A∣w∣2 dx)1/2, so each integral in [F1] is the square of the corresponding L2 norm. (The space Lp(μ) as the quotient by null functions)

Proof

technique · direct
1.1F1given

The hypotheses of [F1] are exactly those of the given setting, so [F1] provides a constant C=C(n,θ,Ma,Mb,Mc) with ∫Br(x0)∣Du∣2 dx≤C(1(R−r)2∫BR(x0)∣u∣2 dx+∫BR(x0)∣u∣2 dx+∫BR(x0)∣f∣2 dx). The constant does not depend on x0,r,R because [F1] itself manufactures it only from n,θ,Ma,Mb,Mc.

2.1F2step 1.1algebra∎

Writing each integral as the square of the L2 norm via [F2], the inequality of step 1.1 becomes exactly the displayed estimate: the left side is ∥Du∥L2(Br(x0))2 and the right side is C((R−r)−2∥u∥L2(BR(x0))2+∥u∥L2(BR(x0))2+∥f∥L2(BR(x0))2). Nothing was changed except the notation, so the scale (R−r)−2 and the independence of the constant from r,R,x0 hold as asserted.

Source notes

Simon's Lemma 1 (printed p. 59) records the constant C(M,θ,ρ,R,n) for the estimate; Hunter's (4.39) (printed p. 112) uses the same scale. The zero-order term is retained explicitly because it cannot be absorbed into the (R−r)−2 term when R−r≥1; it is controlled at the base of every nested-ball iteration.

Depends on

Used by

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources