Euclidean cap volumes

Volume coordinates separating height x 2 from the horizontal Euclidean plane.

The open unit cone selected by the height-to-radius threshold t.

noncomputable def LiebThirring.sphereHeightSplit : Position ≃ᵐ ℝ × EuclideanSpace ℝ (Fin 2)

Volume coordinates separating height x 2 from the horizontal Euclidean plane.

Equations

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

theorem LiebThirring.sphereHeightSplit_preserving : MeasureTheory.MeasurePreserving (⇑sphereHeightSplit) MeasureTheory.volume MeasureTheory.volume

theorem LiebThirring.sphereHeightSplit_fst (x : Position) : (sphereHeightSplit x).1 = x.ofLp 2

theorem LiebThirring.sphereHeightSplit_norm (x : Position) : ‖x‖ ^ 2 = (sphereHeightSplit x).1 ^ 2 + ‖(sphereHeightSplit x).2‖ ^ 2

theorem LiebThirring.height_sub_one (x : Position) (hx : ‖x‖ < 1) : x.ofLp 2 < 1

theorem LiebThirring.cap_slice_low {t s q n : ℝ} (ht : 0 < t) (ht1 : t < 1) (hs : 0 < s) (hst : s ≤ t) (hq : 0 ≤ q) (hn : 0 ≤ n) (hn2 : n ^ 2 = s ^ 2 + q ^ 2) : n < 1 ∧ t * n < s ↔ q < s * √(1 - t ^ 2) / t

theorem LiebThirring.cap_slice_high {t s q n : ℝ} (ht : 0 < t) (hst : t ≤ s) (hs1 : s < 1) (hq : 0 ≤ q) (hn : 0 ≤ n) (hn2 : n ^ 2 = s ^ 2 + q ^ 2) : n < 1 ∧ t * n < s ↔ q < √(1 - s ^ 2)

def LiebThirring.sphereCone (t : ℝ) : Set Position

The open unit cone selected by the height-to-radius threshold t.

Equations

• LiebThirring.sphereCone t = {x : LiebThirring.Position | ‖x‖ < 1 ∧ t * ‖x‖ < x.ofLp 2}

theorem LiebThirring.measurableSet_sphereCone (t : ℝ) : MeasurableSet (sphereCone t)

theorem LiebThirring.cap_cone_eq (t : ℝ) : Set.Ioo 0 1 • Subtype.val '' {ω : ↑(Metric.sphere 0 1) | t < (↑ω).ofLp 2} = sphereCone t

theorem LiebThirring.cone_slice_eq_disk_low {t s : ℝ} (ht : 0 < t) (ht1 : t < 1) (hs : 0 < s) (hst : s ≤ t) : (fun (y : EuclideanSpace ℝ (Fin 2)) => sphereHeightSplit.symm (s, y)) ⁻¹' sphereCone t = Metric.ball 0 (s * √(1 - t ^ 2) / t)

theorem LiebThirring.cone_slice_eq_disk_high {t s : ℝ} (ht : 0 < t) (hst : t ≤ s) (hs1 : s < 1) : (fun (y : EuclideanSpace ℝ (Fin 2)) => sphereHeightSplit.symm (s, y)) ⁻¹' sphereCone t = Metric.ball 0 √(1 - s ^ 2)

theorem LiebThirring.cone_slice_empty {t s : ℝ} (ht : 0 ≤ t) (hs : s ≤ 0 ∨ 1 ≤ s) : (fun (y : EuclideanSpace ℝ (Fin 2)) => sphereHeightSplit.symm (s, y)) ⁻¹' sphereCone t = ∅

theorem LiebThirring.cone_slice_area {t : ℝ} (ht : 0 < t) (ht1 : t < 1) (s : ℝ) : MeasureTheory.volume ((fun (y : EuclideanSpace ℝ (Fin 2)) => sphereHeightSplit.symm (s, y)) ⁻¹' sphereCone t) = (Set.Ioo 0 t).indicator (fun (s : ℝ) => ENNReal.ofReal (Real.pi * ((1 - t ^ 2) / t ^ 2) * s ^ 2)) s + (Set.Ico t 1).indicator (fun (s : ℝ) => ENNReal.ofReal (Real.pi * (1 - s ^ 2))) s

theorem LiebThirring.lintegral_sq_Ioo (c a b : ℝ) (hab : a ≤ b) (hc : 0 ≤ c) : ∫⁻ (s : ℝ) in Set.Ioo a b, ENNReal.ofReal (c * s ^ 2) = ENNReal.ofReal (c * ((b ^ 3 - a ^ 3) / 3))

theorem LiebThirring.lintegral_one_sub_sq_Ico {t : ℝ} (ht : 0 ≤ t) (ht1 : t ≤ 1) : ∫⁻ (s : ℝ) in Set.Ico t 1, ENNReal.ofReal (Real.pi * (1 - s ^ 2)) = ENNReal.ofReal (Real.pi * (1 - t - (1 - t ^ 3) / 3))

theorem LiebThirring.volume_sphereCone {t : ℝ} (ht : 0 < t) (ht1 : t < 1) : MeasureTheory.volume (sphereCone t) = ENNReal.ofReal (2 * Real.pi / 3 * (1 - t))

theorem LiebThirring.unitSphereMeasure_cap {t : ℝ} (ht : 0 < t) (ht1 : t < 1) : unitSphereMeasure {ω : ↑(Metric.sphere 0 1) | t < (↑ω).ofLp 2} = ENNReal.ofReal ((1 - t) / 2)

theorem LiebThirring.measurable_sphereHeight : Measurable fun (ω : ↑(Metric.sphere 0 1)) => (↑ω).ofLp 2

theorem LiebThirring.sphereHeight_Ioi {t : ℝ} (ht : 0 < t) : (MeasureTheory.Measure.map (fun (ω : ↑(Metric.sphere 0 1)) => (↑ω).ofLp 2) unitSphereMeasure) (Set.Ioi t) = (ENNReal.ofReal 2)⁻¹ * ENNReal.ofReal (max (1 - t) 0)

theorem LiebThirring.sphereHeight_neg_invariant : MeasureTheory.Measure.map (fun (s : ℝ) => -s) (MeasureTheory.Measure.map (fun (ω : ↑(Metric.sphere 0 1)) => (↑ω).ofLp 2) unitSphereMeasure) = MeasureTheory.Measure.map (fun (ω : ↑(Metric.sphere 0 1)) => (↑ω).ofLp 2) unitSphereMeasure