Standalone Lean project
Lean 4 formalization of De Giorgi-Nash-Moser theory
Flagship declarations
BareFunction.ae_eq_of_tendsto_eLpNorm_sub
Plain-language statement
Lp limit uniqueness: if f_n → g₁ and f_n → g₂ in eLpNorm, then g₁ =ᵐ g₂.
Source project: DeGiorgi
Person-level attribution pending.
BareFunction.eLpNorm_pi_le_sum_component
Plain-language statement
Vector eLpNorm ≤ sum of component eLpNorms for Pi-valued functions. Uses eLpNorm_mono_real for the pointwise bound together with eLpNorm_sum_le for ℝ-valued functions, avoiding Pi instance synthesis.
Source project: DeGiorgi
Person-level attribution pending.
BareFunction.memLp_of_tendsto_eLpNorm
Plain-language statement
If f n → g in eLpNorm and each f n ∈ Lp, then g ∈ Lp, provided g is AEStronglyMeasurable. Avoids the Lp type entirely. The key observation: eLpNorm (f n - g) → 0 means eLpNorm (f N - g) < 1 for some N. Then eLpNorm g ≤ eLpNorm (f N - g) + eLpNorm (f N) < ∞.
Source project: DeGiorgi
Person-level attribution pending.
BareFunction.scalar_cauchy_to_limit
Plain-language statement
Scalar Cauchy → limit. Generic over codomain E and domain α.
Source project: DeGiorgi
Person-level attribution pending.
BareFunction.tendsto_eLpNorm_pi_component
Plain-language statement
Vector eLpNorm convergence → component eLpNorm convergence. Uses eLpNorm_pi_component_le via an explicit function equality to avoid expensive defeq checks.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.abs_ballAverage_sub_sixBallAverage_le
Plain-language statement
The average shift estimate: |(u)_B - (u)_{6B}| ≤ 6^d * M.
Source project: DeGiorgi
Person-level attribution pending.
Project index
Showing 8 of 140 additional declarations. Use project search for the complete index.
DeGiorgi.abs_sub_const_bmo_le_two
Plain-language statement
The absolute value function |u - c| has BMO seminorm at most 2M whenever u has BMO seminorm at most M. Uses the reverse triangle inequality ||a| - |b|| ≤ |a - b|.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.abs_subballAverage_sub_ballAverage_le
Plain-language statement
The average on a sub-ball differs from the average on a larger ball by at most the volume ratio times the mean oscillation on the larger ball.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.ae_eq_dyadicBallAverageLimit_on_halfBall
Plain-language statement
On the inner ball, the dyadic Campanato average limit agrees a.e. with the original function.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.ae_eq_zero_of_memH01_of_gradLpOfWitness_eq_zero
Plain-language statement
A zero-trace Sobolev function with vanishing L² gradient class vanishes almost everywhere.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aestronglyMeasurable_bilinFormIntegrandOfCoeff
Plain-language statement
The bilinear-form integrand is a.e. strongly measurable on Ω.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aestronglyMeasurable_divergenceRHSIntegrandOfField
Plain-language statement
The divergence-form RHS integrand is a.e. strongly measurable on Ω.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aestronglyMeasurable_unitBallExtension_of_memLp
Plain-language statement
AEStronglyMeasurable for unitBallExtension of rough u. Uses measurable representative + ae_eq transfer.
Source project: DeGiorgi
Person-level attribution pending.
DeGiorgi.aHarmonic_replacement_exists
Plain-language statement
A-harmonic replacement: given u ∈ W^{1,2}(B_R), there exists h that is A-harmonic with h - u ∈ W₀^{1,2}(B_R).
Source project: DeGiorgi
Person-level attribution pending.