Foundation Pair Kernel Newtonian3 Integrable Inv Sq Profile Comp Norm

A technical step in a larger proof

The declaration integrable_invSqProfile_comp_norm is a technical lemma within a formal library of machine-checked theorems. It states that a particular function, defined on three-dimensional Euclidean space, is integrable. This is a necessary condition for the integral of that function to be well-defined, a stepping stone in a larger proof.

The function in question takes a point in space, measures its distance from the origin, and returns the inverse square of that distance, but only if the distance is below a certain cutoff. Beyond that cutoff, the function returns zero. This is a common way to handle the infinite reach of the inverse square law in a finite calculation.

The proof of this integrability is not a trivial matter. The inverse square function is not integrable over all of space, so the cutoff is essential. The proof uses the fact that the function is bounded and has compact support, meaning it is zero outside a finite region. This allows the integral to be computed using standard techniques.

This declaration does not, by itself, prove any physical law or establish any new constant. It is a technical prerequisite. The larger proof it serves aims to show that a certain Fourier integral, related to the Newtonian potential, has the expected value. This declaration is one of many lemmas that make up that proof.

private theorem integrable_invSqProfile_comp_norm {R : ℝ} :
    Integrable (fun x : EuclideanSpace ℝ (Fin 3) => invSqProfile R ‖x‖) := by
  rw [MeasureTheory.integrable_fun_norm_addHaar]
  simp only [finrank_euclideanSpace_fin]
  show IntegrableOn (fun y : ℝ => y ^ 2 • invSqProfile R y) (Set.Ioi 0) volume
  have hIoo : IntegrableOn (fun _ : ℝ => (1 : ℝ)) (Set.Ioo 0 R) :=
    integrableOn_const (hs := by rw [Real.volume_Ioo]; exact ENNReal.ofReal_ne_top)
  have hind : Integrable ((Set.Ioo (0 : ℝ) R).indicator fun _ => (1 : ℝ)) :=
    (integrable_indicator_iff measurableSet_Ioo).2 hIoo
  refine hind.integrableOn.congr_fun ?_ measurableSet_Ioi
  intro y hy
  rw [Set.mem_Ioi] at hy
  simp only [Set.indicator_apply, Set.mem_Ioo, smul_eq_mul, invSqProfile]
  by_cases hlt : y < R
  · rw [if_pos ⟨hy, hlt⟩, if_pos hlt, mul_inv_cancel₀ (pow_ne_zero 2 (ne_of_gt hy))]
  · rw [if_neg fun h => hlt h.2, if_neg hlt, mul_zero]

What this page does not claim

This declaration does not prove the Newtonian Fourier identity itself. This declaration does not establish any physical law or constant. This declaration does not provide a value for the integral, only its existence.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PairKernelNewtonian3.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: