A proved interior bound for ordinary three-dimensional harmonic functions

The constant is built from fixed smooth cutoffs and the already proved Fourier Sobolev inequality. It is independent of the harmonic function. The argument uses two actual Caccioppoli estimates; no harmonic mean-value theorem or interior regularity estimate is assumed.

The actual second-derivative estimate for the localized harmonic function.

Actual nested smooth cutoffs, with finite derivative bounds independent of the field.

theorem EulerMeanHarmonic.derivative_bound_exists (f : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport f) (hs : ContDiff ℝ (↑⊤) f) (n : ℕ) : ∃ (C : ℝ), ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n f x‖ ≤ C

noncomputable def EulerMeanHarmonic.derivativeBound (f : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport f) (hs : ContDiff ℝ (↑⊤) f) (n : ℕ) : ℝ

Derivative bound, given by max 1 (Classical.choose (derivative_bound_exists f hc hs n)).

Equations

• EulerMeanHarmonic.derivativeBound f hc hs n = max 1 (Classical.choose ⋯)

theorem EulerMeanHarmonic.one_le_derivativeBound (f : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport f) (hs : ContDiff ℝ (↑⊤) f) (n : ℕ) : 1 ≤ derivativeBound f hc hs n

theorem EulerMeanHarmonic.norm_iteratedFDeriv_le_derivativeBound (f : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport f) (hs : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n f x‖ ≤ derivativeBound f hc hs n

theorem EulerMeanHarmonic.norm_gradient_le_derivativeBound (f : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport f) (hs : ContDiff ℝ (↑⊤) f) (x : EulerSmoothLimit.Space) : ‖gradient f x‖ ≤ derivativeBound f hc hs 1

theorem EulerMeanHarmonic.abs_secondPartial_le_derivativeBound (f : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport f) (hs : ContDiff ℝ (↑⊤) f) (i : Fin 3) (x : EulerSmoothLimit.Space) : |EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative f i) i x| ≤ derivativeBound f hc hs 2

noncomputable def EulerMeanHarmonic.innerBump : ContDiffBump 0

Inner bump, given by ⟨1/2, 5/8, by norm_num, by norm_num⟩.

Equations

• EulerMeanHarmonic.innerBump = { rIn := 1 / 2, rOut := 5 / 8, rIn_pos := EulerMeanHarmonic.innerBump._proof_1, rIn_lt_rOut := EulerMeanHarmonic.innerBump._proof_2 }

noncomputable def EulerMeanHarmonic.middleBump : ContDiffBump 0

Middle bump, given by ⟨3/4, 13/16, by norm_num, by norm_num⟩.

Equations

• EulerMeanHarmonic.middleBump = { rIn := 3 / 4, rOut := 13 / 16, rIn_pos := EulerMeanHarmonic.middleBump._proof_1, rIn_lt_rOut := EulerMeanHarmonic.middleBump._proof_2 }

noncomputable def EulerMeanHarmonic.outerBump : ContDiffBump 0

Outer bump, given by ⟨7/8, 15/16, by norm_num, by norm_num⟩.

Equations

• EulerMeanHarmonic.outerBump = { rIn := 7 / 8, rOut := 15 / 16, rIn_pos := EulerMeanHarmonic.outerBump._proof_1, rIn_lt_rOut := EulerMeanHarmonic.outerBump._proof_2 }

noncomputable def EulerMeanHarmonic.innerCutoff : EulerSmoothLimit.Space → ℝ

Inner cutoff, given by innerBump.

Equations

• EulerMeanHarmonic.innerCutoff = ↑EulerMeanHarmonic.innerBump

noncomputable def EulerMeanHarmonic.middleCutoff : EulerSmoothLimit.Space → ℝ

Middle cutoff, given by middleBump.

Equations

• EulerMeanHarmonic.middleCutoff = ↑EulerMeanHarmonic.middleBump

noncomputable def EulerMeanHarmonic.outerCutoff : EulerSmoothLimit.Space → ℝ

Outer cutoff, given by outerBump.

Equations

• EulerMeanHarmonic.outerCutoff = ↑EulerMeanHarmonic.outerBump

theorem EulerMeanHarmonic.inner_smooth : ContDiff ℝ (↑⊤) innerCutoff

theorem EulerMeanHarmonic.middle_smooth : ContDiff ℝ (↑⊤) middleCutoff

theorem EulerMeanHarmonic.outer_smooth : ContDiff ℝ (↑⊤) outerCutoff

theorem EulerMeanHarmonic.inner_compact : HasCompactSupport innerCutoff

theorem EulerMeanHarmonic.middle_compact : HasCompactSupport middleCutoff

theorem EulerMeanHarmonic.outer_compact : HasCompactSupport outerCutoff

theorem EulerMeanHarmonic.inner_support : tsupport innerCutoff = Metric.closedBall 0 (5 / 8)

theorem EulerMeanHarmonic.middle_support : tsupport middleCutoff = Metric.closedBall 0 (13 / 16)

theorem EulerMeanHarmonic.outer_support : tsupport outerCutoff = Metric.closedBall 0 (15 / 16)

theorem EulerMeanHarmonic.abs_inner_le_one (x : EulerSmoothLimit.Space) : |innerCutoff x| ≤ 1

theorem EulerMeanHarmonic.abs_middle_le_one (x : EulerSmoothLimit.Space) : |middleCutoff x| ≤ 1

theorem EulerMeanHarmonic.abs_outer_le_one (x : EulerSmoothLimit.Space) : |outerCutoff x| ≤ 1

theorem EulerMeanHarmonic.inner_one_on_halfBall {x : EulerSmoothLimit.Space} (hx : x ∈ Metric.closedBall 0 (1 / 2)) : innerCutoff x = 1

theorem EulerMeanHarmonic.middle_one_on_inner_support {x : EulerSmoothLimit.Space} (hx : x ∈ tsupport innerCutoff) : middleCutoff x = 1

theorem EulerMeanHarmonic.outer_one_on_middle_support {x : EulerSmoothLimit.Space} (hx : x ∈ tsupport middleCutoff) : outerCutoff x = 1

theorem EulerMeanHarmonic.outer_one_on_inner_support {x : EulerSmoothLimit.Space} (hx : x ∈ tsupport innerCutoff) : outerCutoff x = 1

theorem EulerMeanHarmonic.outer_support_unitBall : tsupport outerCutoff ⊆ Metric.ball 0 1

theorem EulerMeanHarmonic.middle_support_unitBall : tsupport middleCutoff ⊆ Metric.ball 0 1

Two local energy steps for smooth harmonic functions on the unit ball.

noncomputable def EulerMeanHarmonic.outerDerivativeBound : ℝ

Outer derivative bound, given by derivativeBound outerCutoff outer_compact outer_smooth 1.

Equations

• EulerMeanHarmonic.outerDerivativeBound = EulerMeanHarmonic.derivativeBound EulerMeanHarmonic.outerCutoff EulerMeanHarmonic.outer_compact EulerMeanHarmonic.outer_smooth 1

noncomputable def EulerMeanHarmonic.middleDerivativeBound : ℝ

Middle derivative bound, given by derivativeBound middleCutoff middle_compact middle_smooth 1.

Equations

• EulerMeanHarmonic.middleDerivativeBound = EulerMeanHarmonic.derivativeBound EulerMeanHarmonic.middleCutoff EulerMeanHarmonic.middle_compact EulerMeanHarmonic.middle_smooth 1

noncomputable def EulerMeanHarmonic.innerDerivativeBound : ℝ

Inner derivative bound, given by derivativeBound innerCutoff inner_compact inner_smooth 1.

Equations

• EulerMeanHarmonic.innerDerivativeBound = EulerMeanHarmonic.derivativeBound EulerMeanHarmonic.innerCutoff EulerMeanHarmonic.inner_compact EulerMeanHarmonic.inner_smooth 1

noncomputable def EulerMeanHarmonic.innerSecondBound : ℝ

Inner second bound, given by derivativeBound innerCutoff inner_compact inner_smooth 2.

Equations

• EulerMeanHarmonic.innerSecondBound = EulerMeanHarmonic.derivativeBound EulerMeanHarmonic.innerCutoff EulerMeanHarmonic.inner_compact EulerMeanHarmonic.inner_smooth 2

theorem EulerMeanHarmonic.outer_bound_nonneg : 0 ≤ outerDerivativeBound

theorem EulerMeanHarmonic.middle_bound_nonneg : 0 ≤ middleDerivativeBound

theorem EulerMeanHarmonic.inner_bound_nonneg : 0 ≤ innerDerivativeBound

theorem EulerMeanHarmonic.inner_second_nonneg : 0 ≤ innerSecondBound

theorem EulerMeanHarmonic.outer_gradient_energy_le (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hLp : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hharmonic : ∀ x ∈ Metric.ball 0 1, Laplacian.laplacian h x = 0) : ∫ (x : EulerSmoothLimit.Space), outerCutoff x ^ 2 * ‖gradient h x‖ ^ 2 ≤ 4 * outerDerivativeBound ^ 2 * MeasureTheory.lpNorm h 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.outer_partial_energy_le (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hLp : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hharmonic : ∀ x ∈ Metric.ball 0 1, Laplacian.laplacian h x = 0) (i : Fin 3) : ∫ (x : EulerSmoothLimit.Space), outerCutoff x ^ 2 * EulerVectorCalculus.partialDerivative h i x ^ 2 ≤ 4 * outerDerivativeBound ^ 2 * MeasureTheory.lpNorm h 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.middle_second_energy_le (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hLp : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hharmonic : ∀ x ∈ Metric.ball 0 1, Laplacian.laplacian h x = 0) (i : Fin 3) : ∫ (x : EulerSmoothLimit.Space), middleCutoff x ^ 2 * ‖gradient (EulerVectorCalculus.partialDerivative h i) x‖ ^ 2 ≤ 16 * middleDerivativeBound ^ 2 * outerDerivativeBound ^ 2 * MeasureTheory.lpNorm h 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.localized_second_pointwise (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (i : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative (innerCutoff * h) i) i x ^ 2 ≤ 3 * (innerSecondBound ^ 2 * h x ^ 2 + 4 * innerDerivativeBound ^ 2 * (outerCutoff x ^ 2 * ‖gradient h x‖ ^ 2) + middleCutoff x ^ 2 * ‖gradient (EulerVectorCalculus.partialDerivative h i) x‖ ^ 2)

noncomputable def EulerMeanHarmonic.interiorSecondEnergyConstant : ℝ

Interior second energy constant, constructed using 3.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerMeanHarmonic.interiorSecondEnergyConstant_nonneg : 0 ≤ interiorSecondEnergyConstant

theorem EulerMeanHarmonic.localized_second_memLp (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (i : Fin 3) : MeasureTheory.MemLp (EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative (innerCutoff * h) i) i) 2 MeasureTheory.volume

theorem EulerMeanHarmonic.localized_second_energy_le (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hLp : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hharmonic : ∀ x ∈ Metric.ball 0 1, Laplacian.laplacian h x = 0) (i : Fin 3) : MeasureTheory.lpNorm (EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative (innerCutoff * h) i) i) 2 MeasureTheory.volume ^ 2 ≤ interiorSecondEnergyConstant * MeasureTheory.lpNorm h 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.localized_second_norm_le (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hLp : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hharmonic : ∀ x ∈ Metric.ball 0 1, Laplacian.laplacian h x = 0) (i : Fin 3) : MeasureTheory.lpNorm (EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative (innerCutoff * h) i) i) 2 MeasureTheory.volume ≤ √interiorSecondEnergyConstant * MeasureTheory.lpNorm h 2 MeasureTheory.volume

theorem EulerMeanHarmonic.localized_norm_le (h : EulerSmoothLimit.Space → ℝ) (hLp : MeasureTheory.MemLp h 2 MeasureTheory.volume) : MeasureTheory.lpNorm (innerCutoff * h) 2 MeasureTheory.volume ≤ MeasureTheory.lpNorm h 2 MeasureTheory.volume

noncomputable def EulerMeanHarmonic.harmonicInteriorConstant : ℝ

Harmonic interior constant, given by embeddingConstant 3 2 (by norm_num) * (1 + (2 * Real.pi) ^ (-2 : ℤ) * (3 * Real.sqrt interiorSecondEnergyConstant)).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerMeanHarmonic.harmonicInteriorConstant_nonneg : 0 ≤ harmonicInteriorConstant

theorem EulerMeanHarmonic.harmonic_pointwise_halfBall (h : EulerSmoothLimit.Space → ℝ) (hh : ContDiff ℝ (↑⊤) h) (hLp : MeasureTheory.MemLp h 2 MeasureTheory.volume) (hharmonic : ∀ x ∈ Metric.ball 0 1, Laplacian.laplacian h x = 0) (x : EulerSmoothLimit.Space) (hx : x ∈ Metric.closedBall 0 (1 / 2)) : |h x| ≤ harmonicInteriorConstant * MeasureTheory.lpNorm h 2 MeasureTheory.volume

A genuine L²-to-pointwise interior estimate on the unit ball in R³.