Imports
/-
Copyright (c) 2026 Robert Sneiderman. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Sneiderman
-/
module
public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.Line
Half-plane surface in Space 3
The half-plane is the coordinate plane in Space 3 with nonnegative second
coordinate.
@[expose] public sectionA. The definition of the half-plane surface
The domain of the half-plane inside Space 2.
def halfPlaneDomain : Set (Space 2) := {x | 0 ≤ x (1 : Fin 2)}
The coordinate plane embedding used for the half-plane surface in Space 3.
lemma halfPlane_eq : halfPlane = (slice (2 : Fin 3)).symm ∘ (fun x : Space 2 => (0, x)) := rfllemma halfPlane_injective : Function.Injective halfPlane := ⊢ Function.Injective halfPlane
x:Space 2y:Space 2h:x.halfPlane = y.halfPlane⊢ x = y
x:Space 2y:Space 2h:x.halfPlane = y.halfPlaneh':(slice 2) x.halfPlane = (slice 2) y.halfPlane⊢ x = y
x:Space 2y:Space 2h:x.halfPlane = y.halfPlaneh':x = y⊢ x = y
All goals completed! 🐙⊢ Continuous (⇑(slice 2).symm ∘ fun x => (0, x))
All goals completed! 🐙lemma halfPlane_measurableEmbedding : MeasurableEmbedding halfPlane :=
Continuous.measurableEmbedding halfPlane_continuous halfPlane_injectivex:Space 2⊢ √(‖0‖ ^ 2 + ‖x‖ ^ 2) = ‖x‖
All goals completed! 🐙B. The measure associated with the half-plane
The measure on Space 3 corresponding to integration over a half-plane.
def halfPlaneMeasure : Measure (Space 3) :=
MeasureTheory.Measure.map halfPlane (volume.restrict halfPlaneDomain)𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ Integrable ((fun x => (1 + ‖x‖) ^ (-↑n)) ∘ halfPlane) (volume.restrict halfPlaneDomain)
𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volume⊢ (fun x => (1 + ‖x‖) ^ (-↑n)) ∘ halfPlane = fun x => (1 + ‖x‖) ^ (-↑n)
𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fn:ℕhn:Integrable (fun x => (1 + ‖x‖) ^ (-↑n)) volumex:Space 2⊢ ((fun x => (1 + ‖x‖) ^ (-↑n)) ∘ halfPlane) x = (1 + ‖x‖) ^ (-↑n)
All goals completed! 🐙𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ F⊢ SFinite (Measure.map halfPlane (volume.restrict halfPlaneDomain))
All goals completed! 🐙C. The distribution associated with the half-plane
The distribution on Space 3 corresponding to integration over a half-plane.
def halfPlaneDist : (Space 3) →d[ℝ] ℝ :=
SchwartzMap.integralCLM ℝ halfPlaneMeasureAll goals completed! 🐙All goals completed! 🐙D. The half-plane has ambient volume zero
The coordinate plane containing the half-plane in Space 3.
All goals completed! 🐙lemma halfPlane_mem_halfPlaneSubmodule (x : Space 2) : halfPlane x ∈ halfPlaneSubmodule := x:Space 2⊢ x.halfPlane ∈ halfPlaneSubmodule
All goals completed! 🐙lemma halfPlane_image_domain_subset_halfPlaneSubmodule :
halfPlane '' halfPlaneDomain ⊆ (halfPlaneSubmodule : Set (Space 3)) := ⊢ halfPlane '' halfPlaneDomain ⊆ ↑halfPlaneSubmodule
y:Space 2left✝:y ∈ halfPlaneDomain⊢ y.halfPlane ∈ ↑halfPlaneSubmodule
All goals completed! 🐙htop:halfPlaneSubmodule = ⊤hbasis:basis 2 ∈ halfPlaneSubmodule⊢ False
All goals completed! 🐙⊢ basis.toBasis.addHaar ↑halfPlaneSubmodule = 0
All goals completed! 🐙