HardSphereClosePair

Graph, coordinate, and measure constructions for the hard-sphere NBC volume identity.

@[reducible, inline]

abbrev HsVirial.HS3 : Type

Three-dimensional Euclidean position space.

Equations

• HsVirial.HS3 = HsVirial.HSPosition 3

@[reducible, inline]

abbrev HsVirial.HS2 : Type

Two-dimensional Euclidean position space used for planar sections.

Equations

• HsVirial.HS2 = HsVirial.HSPosition 2

def HsVirial.testSplit3 : HS3 ≃ᵐ ℝ × HS2

The measurable separation of the axial coordinate from the two transverse coordinates.

Equations

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

theorem HsVirial.testMeasurePreserving_split3 : MeasureTheory.MeasurePreserving (⇑testSplit3) MeasureTheory.volume MeasureTheory.volume

def HsVirial.testAxis3 (s : ℝ) (y : HS2) : HS3

Reassemble a position from one axial and two transverse coordinates.

Equations

• HsVirial.testAxis3 s y = HsVirial.testSplit3.symm (s, y)

theorem HsVirial.testAxis3_apply (s : ℝ) (y : HS2) : testAxis3 s y = (MeasurableEquiv.toLp 2 (Fin 3 → ℝ)) fun (i : Fin 3) => if i = 0 then s else (MeasurableEquiv.toLp 2 (Fin 2 → ℝ)).symm y (Fin.predAbove 0 i)

theorem HsVirial.testToLp_apply (z : Fin 3 → ℝ) (i : Fin 3) : ((MeasurableEquiv.toLp 2 (Fin 3 → ℝ)) z).ofLp i = z i

theorem HsVirial.testNorm_axis3_sq (s : ℝ) (y : HS2) : ‖testAxis3 s y‖ ^ 2 = s ^ 2 + ‖y‖ ^ 2

theorem HsVirial.testNorm_axis3 (s : ℝ) (y : HS2) (_hs : 0 ≤ s) : ‖testAxis3 s y‖ ^ 2 = s ^ 2 + ‖y‖ ^ 2

theorem HsVirial.testAxis3_sub_axis (t s : ℝ) (y : HS2) : testAxis3 t y - testAxis3 s 0 = testAxis3 (t - s) y

def HsVirial.testAxisIntersection (s : ℝ) : Set (ℝ × HS2)

Two unit balls, separated along the axis, expressed in axial coordinates.

Equations

• HsVirial.testAxisIntersection s = {p : ℝ × HsVirial.HS2 | p.1 ^ 2 + ‖p.2‖ ^ 2 < 1 ∧ (p.1 - s) ^ 2 + ‖p.2‖ ^ 2 < 1}

theorem HsVirial.measurableSet_testAxisIntersection (s : ℝ) : MeasurableSet (testAxisIntersection s)

noncomputable def HsVirial.testSectionRadius (s t : ℝ) : ℝ

The smaller radius of the two ball sections at the specified axial coordinate.

Equations

• HsVirial.testSectionRadius s t = min √(max 0 (1 - t ^ 2)) √(max 0 (1 - (t - s) ^ 2))

theorem HsVirial.testSectionRadius_sq (s t : ℝ) : testSectionRadius s t ^ 2 = min (max 0 (1 - t ^ 2)) (max 0 (1 - (t - s) ^ 2))

theorem HsVirial.testSectionRadius_sq_eq_right (s t : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (hlo : s - 1 < t) (hmid : t ≤ s / 2) : testSectionRadius s t ^ 2 = 1 - (t - s) ^ 2

theorem HsVirial.testSectionRadius_sq_eq_left (s t : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) (hmid : s / 2 < t) (htop : t ≤ 1) : testSectionRadius s t ^ 2 = 1 - t ^ 2

theorem HsVirial.testSectionRadius_sq_eq_zero_of_le (s t : ℝ) (h : t ≤ s - 1) : testSectionRadius s t ^ 2 = 0

theorem HsVirial.testSectionRadius_sq_eq_zero_of_gt (s t : ℝ) (h : 1 < t) : testSectionRadius s t ^ 2 = 0

theorem HsVirial.testSectionRadius_sq_eq_piecewise (s t : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : testSectionRadius s t ^ 2 = (Set.Ioc (s - 1) (s / 2)).indicator (fun (u : ℝ) => 1 - (u - s) ^ 2) t + (Set.Ioc (s / 2) 1).indicator (fun (u : ℝ) => 1 - u ^ 2) t

theorem HsVirial.testSectionRadius_sq_integral (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : ∫ (t : ℝ), testSectionRadius s t ^ 2 = (∫ (t : ℝ) in s - 1..s / 2, 1 - (t - s) ^ 2) + ∫ (t : ℝ) in s / 2..1, 1 - t ^ 2

theorem HsVirial.testAxisIntersection_section_integral_eq_lens (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : ∫ (t : ℝ), Real.pi * testSectionRadius s t ^ 2 = hardSphereLens s

theorem HsVirial.testMem_ball_sqrt_max_iff (t : ℝ) (z : HS2) : z ∈ Metric.ball 0 √(max 0 (1 - t ^ 2)) ↔ t ^ 2 + ‖z‖ ^ 2 < 1

theorem HsVirial.testAxisIntersection_section (s t : ℝ) : Prod.mk t ⁻¹' testAxisIntersection s = Metric.ball 0 (testSectionRadius s t)

theorem HsVirial.testAxisIntersection_section_volume (s t : ℝ) : MeasureTheory.volume (Prod.mk t ⁻¹' testAxisIntersection s) = ENNReal.ofReal (testSectionRadius s t) ^ 2 * ENNReal.ofReal Real.pi

theorem HsVirial.testAxis3_split_apply (s : ℝ) (y : HS2) : testSplit3 (testAxis3 s y) = (s, y)

theorem HsVirial.testAxisIntersection_image (s : ℝ) (_hs : 0 ≤ s) : ⇑testSplit3 '' (Metric.ball 0 1 ∩ Metric.ball (testAxis3 s 0) 1) = testAxisIntersection s

theorem HsVirial.testAxisIntersection_volume_as_lintegral (s : ℝ) (hs : 0 ≤ s) : MeasureTheory.volume (Metric.ball 0 1 ∩ Metric.ball (testAxis3 s 0) 1) = ∫⁻ (t : ℝ), MeasureTheory.volume (Prod.mk t ⁻¹' testAxisIntersection s)

theorem HsVirial.testAxisIntersection_section_volume_real (s t : ℝ) : MeasureTheory.volume.real (Prod.mk t ⁻¹' testAxisIntersection s) = Real.pi * testSectionRadius s t ^ 2

theorem HsVirial.testAxisIntersection_volume_real_as_integral (s : ℝ) (hs : 0 ≤ s) : MeasureTheory.volume.real (Metric.ball 0 1 ∩ Metric.ball (testAxis3 s 0) 1) = ∫ (t : ℝ), MeasureTheory.volume.real (Prod.mk t ⁻¹' testAxisIntersection s)

theorem HsVirial.testAxisIntersection_volume_real_eq_lens (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : MeasureTheory.volume.real (Metric.ball 0 1 ∩ Metric.ball (testAxis3 s 0) 1) = hardSphereLens s

theorem HsVirial.testAxis3_norm (s : ℝ) (hs : 0 ≤ s) : ‖testAxis3 s 0‖ = s

theorem HsVirial.testBallIntersection_image_linearIsometry (R : HS3 ≃ₗᵢ[ℝ] HS3) (d : HS3) : ⇑R '' (Metric.ball 0 1 ∩ Metric.ball d 1) = Metric.ball (R 0) 1 ∩ Metric.ball (R d) 1

theorem HsVirial.testBallIntersection_real_volume_eq_lens_norm (d : HS3) (hd : ‖d‖ ≤ 1) : MeasureTheory.volume.real (Metric.ball 0 1 ∩ Metric.ball d 1) = hardSphereLens ‖d‖

def HsVirial.testPairBlock (x : Fin 2 × Fin 3 → ℝ) (i : Fin 2) : HS3

Read one three-dimensional position from flattened two-particle coordinates.

Equations

• HsVirial.testPairBlock x i = (MeasurableEquiv.toLp 2 (Fin 3 → ℝ)) fun (a : Fin 3) => x (i, a)

def HsVirial.testPairDifferencePositionMap (p : HS3 × HS3) : HS3 × HS3

The difference-coordinate transformation used to integrate pairs of positions.

Equations

• HsVirial.testPairDifferencePositionMap p = (HsVirial.hardSpherePairCoordinateEquiv.symm (HsVirial.hardSpherePairDifferenceLinearMap (HsVirial.hardSpherePairCoordinateEquiv p))).swap

theorem HsVirial.testMeasurePreserving_pairDifferencePositionMap : MeasureTheory.MeasurePreserving testPairDifferencePositionMap MeasureTheory.volume MeasureTheory.volume

theorem HsVirial.testPairDifferencePositionMap_apply (p : HS3 × HS3) : testPairDifferencePositionMap p = (p.2 - p.1, p.1)

def HsVirial.testClosePairDifferenceRegion : Set (HS3 × HS3)

Pairs in the unit ball whose sum is also in the unit ball.

Equations

• HsVirial.testClosePairDifferenceRegion = {p : HsVirial.HS3 × HsVirial.HS3 | p.1 ∈ Metric.ball 0 1 ∧ p.2 ∈ Metric.ball 0 1 ∧ p.1 + p.2 ∈ Metric.ball 0 1}

theorem HsVirial.measurableSet_testClosePairDifferenceRegion : MeasurableSet testClosePairDifferenceRegion

theorem HsVirial.testPairDifferencePositionMap_preimage_close : testPairDifferencePositionMap ⁻¹' testClosePairDifferenceRegion = hardSphereClosePairRegion

theorem HsVirial.testClosePairDifferenceRegion_real_volume : MeasureTheory.volume.real testClosePairDifferenceRegion = ∫ (d : HS3), (Metric.ball 0 1).indicator (fun (d : HS3) => hardSphereLens ‖d‖) d

theorem HsVirial.testClosePairRegion_real_volume_eq_difference : MeasureTheory.volume.real hardSphereClosePairRegion = MeasureTheory.volume.real testClosePairDifferenceRegion

theorem HsVirial.testClosePairDifferenceRegion_radial_volume : MeasureTheory.volume.real testClosePairDifferenceRegion = 3 * hardSphereKappa * ∫ (s : ℝ) in 0..1, hardSphereLens s * s ^ 2

theorem HsVirial.testClosePairRegion_real_volume : MeasureTheory.volume.real hardSphereClosePairRegion = 5 * Real.pi ^ 2 / 6

theorem HsVirial.testSeparatedPairRegion_real_volume : MeasureTheory.volume.real hardSphereSeparatedPairRegion = 17 * Real.pi ^ 2 / 18

theorem HsVirial.hardSphereClosePairRegion_real_volume : MeasureTheory.volume.real hardSphereClosePairRegion = 5 * Real.pi ^ 2 / 6

theorem HsVirial.hardSphereSeparatedPairRegion_real_volume : MeasureTheory.volume.real hardSphereSeparatedPairRegion = 17 * Real.pi ^ 2 / 18

theorem HsVirial.hardSphereSeparatedPairRegion_real_volume_ratio : MeasureTheory.volume.real hardSphereSeparatedPairRegion = 17 / 32 * hardSphereKappa ^ 2