Whole-plane mass of the face-charge density

At positive height, the whole-plane face-charge density has mass exactly Z.

theorem LiebThirring.lintegral_planar_faceDensity_mass (a Z : ℝ) (ha : 0 < a) (hZ : 0 ≤ Z) : ∫⁻ (q : Planar), ENNReal.ofReal (Z * a / (2 * Real.pi * √(‖q‖ ^ 2 + a ^ 2) ^ 3)) = ENNReal.ofReal Z

Exact mass of the radial form of the planar face-charge density.

theorem LiebThirring.lintegral_plane_faceDensity_mass (n b c : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (Z : ℝ) (hZ : 0 ≤ Z) (ha : 0 < planeHeight n b c) : ∫⁻ (y : Position), ENNReal.ofReal (Z * planeHeight n b c / (2 * Real.pi * ‖y - c‖ ^ 3)) ∂planeMeasure F = ENNReal.ofReal Z

The whole-plane face charge face-charge density has mass exactly Z.