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.
Harmonic Functions and Mean Values in Rn — Examples
1 · Prerequisites
- Areas of Elementary Plane Figures
- Binary Operations, Monoids, Groups and Subgroups
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Differentiability and the Cauchy–Riemann Equations
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Harmonic Functions and Mean Values in Rn
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Polynomial Rings, the Division Algorithm and Roots
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Regular Surfaces and Surface Integrals
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Simple Field Extensions and the Construction of the Complex Numbers
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Divergence Theorem and Classical Stokes
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Lebesgue Integral and the Convergence Theorems
- The Maximal Function and Lebesgue Differentiation
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
Examples distinguish global mean-value structure from isolated identities and classical smoothness from distributional harmonicity.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Affine functions and mixed quadratic monomials are harmonic
Example
Let , , and . Every affine function is harmonic on . If and are distinct, then is harmonic on .
Verification
Given: the displayed dimension, coefficients, coordinate indices, and the classical Laplacian The Laplacian of a function and of a vector field.
All second partial derivatives of vanish [given].
For , each diagonal second derivative of vanishes [given]. ∎
Real and imaginary parts of holomorphic monomials
Example
For , the components and , and likewise those of every , are harmonic on .
Verification
Given: .
The real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair makes its two components harmonic [step 1.1]. ∎
Radial harmonic functions away from the origin
Example
Let and . The radial function given by is harmonic precisely when Thus the families are for , for , and for .
Verification
Given: , , and .
Direct differentiation gives [given].
Multiplying by gives , whose integrations give the listed cases [given, algebra]. ∎
Harmonic on a punctured domain need not extend
Statement refuted
A function harmonic on a punctured domain need not extend harmonically across the puncture.
Counterexample
Given: .
On take ; for take , both harmonic by Radial harmonic functions away from the origin [given].
Each is unbounded as , so it has no continuous, hence no harmonic, extension [given]. ∎
One centred ball-mean identity does not force harmonicity
Statement refuted
One ball-mean identity at one centre forces harmonicity.
Counterexample
Given: , , and defined by
Polar coordinates Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma give and , hence [given, algebra].
Yet , which is not identically zero [given, algebra]. ∎
Distributional harmonicity removes an apparent interior corner
Example
Let and define by . This apparent corner is not distributionally harmonic on ; indeed . Thus a distributionally harmonic locally integrable function has a unique smooth harmonic representative; in particular, the actual corner cannot be distributionally harmonic on any open set meeting the hyperplane .
Verification
Given: , the domain , and the distributional derivative convention Distributional harmonicity and Poisson's equation on an open subset of Rn.
In one variable, integrating by parts twice gives ; tensoring with the remaining variables gives the stated hyperplane term [given].
Conversely Weyl's lemma for the Laplacian gives every distributionally harmonic distribution a smooth representative [step 1.1]. ∎