Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 2026-10-02
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.

Interior oscillation controls the harmonic gradient

Statement

Assume Countable Choice and n≥2. Let u be real or complex harmonic on an open set Ω⊆Rn with Br(x)‾⊂Ω, r>0. Then ∣Du(x)∣≤Cn r−1osc⁡Br(x)u,osc⁡Br(x)u:=sup⁡y,z∈Br(x)∣u(y)−u(z)∣. The constant Cn depends only on n.

Facts & Assumptions

Given: Countable Choice, an integer n≥2, an open set Ω, a harmonic u on Ω, a point x∈Ω and r>0 with Br(x)‾⊂Ω.

[F1]

For harmonic v on an open set containing Br(x)‾ and every multi-index α, ∣Dαv(x)∣≤Cn,α′r−∣α∣sup⁡Br(x)∣v∣ (Harmonic Cauchy estimates in supremum norm).

[F2]

Countable Choice ACω is the standing hypothesis (The Axiom of Countable Choice (ACω)).

Proof

technique · direct
1.1givenF2algebra

Work under [F2] and put v:=u−u(x), which is harmonic on Ω with the same derivatives as u, in particular Dv(x)=Du(x); moreover ∣v(y)∣=∣u(y)−u(x)∣≤osc⁡Br(x)u for every y∈Br(x), so sup⁡Br(x)∣v∣≤osc⁡Br(x)u.

2.1step 1.1F1algebra

Apply [F1] with α=ei to the harmonic function v on Br(x): ∣∂iu(x)∣=∣∂iv(x)∣≤Cn,ei′r−1sup⁡Br(x)∣v∣≤Cn,ei′r−1osc⁡Br(x)u, with a constant depending only on n and the coordinate; taking Cn:=max⁡iCn,ei′ gives ∣∂iu(x)∣≤Cnr−1osc⁡Br(x)u for every i.

3.1step 2.1algebra∎

Summing the coordinate bounds, ∣Du(x)∣=(∑i∣∂iu(x)∣2)1/2≤nmax⁡i∣∂iu(x)∣≤n Cnr−1osc⁡Br(x)u; absorbing n into the constant gives the assertion with a constant depending only on n.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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