Distance from a point to a parametrized affine plane

The perpendicular foot on a plane with unit normal.

The nonnegative height of a point above a plane with unit normal.

noncomputable def LiebThirring.planeFoot (n b x : Position) : Position

The perpendicular foot on a plane with unit normal.

Equations

• LiebThirring.planeFoot n b x = x - inner ℝ n (x - b) • n

noncomputable def LiebThirring.planeHeight (n b x : Position) : ℝ

The nonnegative height of a point above a plane with unit normal.

Equations

• LiebThirring.planeHeight n b x = |inner ℝ n (x - b)|

theorem LiebThirring.planeHeight_nonneg (n b x : Position) : 0 ≤ planeHeight n b x

theorem LiebThirring.planeFoot_mem (n b x : Position) (hn : ‖n‖ = 1) : planeFoot n b x ∈ affinePlane n b

The perpendicular foot satisfies the literal plane equation.

theorem LiebThirring.sub_planeFoot (n b x : Position) : x - planeFoot n b x = inner ℝ n (x - b) • n

The centre-to-foot vector is the signed height times the unit normal.

theorem LiebThirring.inner_sub_planeFoot_sub_eq_zero (n b x y : Position) (hn : ‖n‖ = 1) (hy : y ∈ affinePlane n b) : inner ℝ (x - planeFoot n b x) (planeFoot n b x - y) = 0

Every vector in the plane is perpendicular to its centre-to-foot vector.

theorem LiebThirring.norm_sub_sq_eq_planeFoot (n b x y : Position) (hn : ‖n‖ = 1) (hy : y ∈ affinePlane n b) : ‖x - y‖ ^ 2 = ‖planeFoot n b x - y‖ ^ 2 + planeHeight n b x ^ 2

Pythagoras for the perpendicular foot and any point of the plane.

noncomputable def LiebThirring.planeFrameAtFoot (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) : PlaneFrame (affinePlane n b)

Rebase an orthonormal frame at the perpendicular foot of the centre.

Equations

• LiebThirring.planeFrameAtFoot n b x hn F = (AffineIsometryEquiv.constVAdd ℝ LiebThirring.Planar ((AffineIsometryEquiv.symm F) ⟨LiebThirring.planeFoot n b x, ⋯⟩)).trans F

@[simp]

theorem LiebThirring.planeFrameAtFoot_zero (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) : ↑((planeFrameAtFoot n b x hn F) 0) = planeFoot n b x

theorem LiebThirring.norm_sub_planeFrameAtFoot_sq (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (q : Planar) : ‖x - ↑((planeFrameAtFoot n b x hn F) q)‖ ^ 2 = ‖q‖ ^ 2 + planeHeight n b x ^ 2

Radial planar coordinates give the exact squared distance, including off-plane centres.

theorem LiebThirring.norm_sub_planeFrameAtFoot_eq_sqrt (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (q : Planar) : ‖x - ↑((planeFrameAtFoot n b x hn F) q)‖ = √(‖q‖ ^ 2 + planeHeight n b x ^ 2)

The literal distance in a foot-based frame is the radial square-root expression.

theorem LiebThirring.coulombKernel_planeFrameAtFoot (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (q : Planar) : coulombKernel x ↑((planeFrameAtFoot n b x hn F) q) = (ENNReal.ofReal √(‖q‖ ^ 2 + planeHeight n b x ^ 2))⁻¹

Exact radial Coulomb expression; when both radius and height vanish its value is infinity.

theorem LiebThirring.lintegral_planeMeasure_atFoot (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (f : Position → ENNReal) (hf : Measurable f) : ∫⁻ (y : Position), f y ∂planeMeasure F = ∫⁻ (q : Planar), f ↑((planeFrameAtFoot n b x hn F) q)

Frame independence permits the perpendicular-foot chart for all measurable integrands.

theorem LiebThirring.lintegral_coulombKernel_ball_planeMeasure (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (ε : ℝ) : ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂planeMeasure F = ∫⁻ (q : Planar), if √(‖q‖ ^ 2 + planeHeight n b x ^ 2) < ε then (ENNReal.ofReal √(‖q‖ ^ 2 + planeHeight n b x ^ 2))⁻¹ else 0

The ambient ball truncation becomes its exact radial square-root cutoff. No positivity condition on the radius and no restriction on the centre is needed.