Grace/Cumulus/Geometry/Euclid/Cones.g17

Open in Workbench Download source

Imports

Ball · Real.Sqrt · Algebra.Group.Paradox

Declarations

Source

1-- Cones over pieces of the sphere lift a decomposition of the sphere to2-- one of the punctured ball3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Euclid.Cones9import Ball10import Real.Sqrt11import Algebra.Group.Paradox1213-- Scaling twice is scaling by the product.14theorem vectorScale.mul (c d v : Set)15  requires scalarC : c ∈ ℝ16  requires scalarD : d ∈ ℝ17  requires vector : v : 3 → ℝ18  shows vectorScale(c, vectorScale(d, v)) = vectorScale((c:R) * (d:R), v)19proof20  have inner := vectorScale.vector with scalarD, vector21  have left := vectorScale.vector with scalarC, inner22  have productReal : (c:R) * (d:R) ∈ ℝ by typecheck23  have right := vectorScale.vector with productReal, vector24  apply FunctionBetween.ext with left, right25  intros i hi26  have vi := vector.component_real at v, i with vector, hi27  have e1 :=28      vectorScale.entry at c, vectorScale(d, v), i with scalarC, inner, hi29  have e2 := vectorScale.entry at d, v, i with scalarD, vector, hi30  have e3 :=31      vectorScale.entry at (c:R) * (d:R), v, i with productReal, vector, hi32  rw [e1, e2, e3]33  ring3435-- A vector of squared norm zero is the zero vector.36theorem normSq.eq_zero (v : Set)37  requires vector : v : 3 → ℝ38  requires zero : normSq(v) = (0:R)39  shows v = zeroVector40proof41  have v0 := vector.component_real at v, 0 with vector, index.zero_mem42  have v1 := vector.component_real at v, 1 with vector, index.one_mem43  have v2 := vector.component_real at v, 2 with vector, index.two_mem44  have sq0 := realMulValue.square_nonnegative at (v(0):R)45  have sq1 := realMulValue.square_nonnegative at (v(1):R)46  have sq2 := realMulValue.square_nonnegative at (v(2):R)47  rw normSq.value at zero48  have z0 : (v(0):R) * (v(0):R) = 0 by linarith49  have z1 : (v(1):R) * (v(1):R) = 0 by linarith50  have z2 : (v(2):R) * (v(2):R) = 0 by linarith51  have c0 := realMulValue.square_eq_zero_iff.forward with z052  have c1 := realMulValue.square_eq_zero_iff.forward with z153  have c2 := realMulValue.square_eq_zero_iff.forward with z254  apply FunctionBetween.ext with vector, zeroVector.vector55  intros i hi56  have zi := zeroVector.entry at i with hi57  rw zi58  have alternatives := index.cases with hi59  rcases alternatives with at0 | at1 | at260  . rw at061    exact c062  . rw at163    exact c164  . rw at265    exact c26667-- Positive multiples of unit vectors determine the scalar and the vector.68theorem vectorScale.sphere_injective (r s u v : Set)69  requires scalarR : r ∈ ℝ70  requires scalarS : s ∈ ℝ71  requires positiveR : (0:R) < r72  requires positiveS : (0:R) < s73  requires hu : u ∈ S²74  requires hv : v ∈ S²75  requires same : vectorScale(r, u) = vectorScale(s, v)76  shows r = s ∧ u = v77proof78  obtain ⟨uSpace, uUnit⟩ := S².membership.forward with hu79  obtain ⟨vSpace, vUnit⟩ := S².membership.forward with hv80  have vectorU := ℝ³.function with uSpace81  have vectorV := ℝ³.function with vSpace82  have normU := vectorScale.normSq with scalarR, vectorU83  have normV := vectorScale.normSq with scalarS, vectorV84  rw [same, normV, vUnit, uUnit] at normU85  have unitS : (s:R) * (s:R) * 1 = (s:R) * (s:R)86    ring87  have unitR : (r:R) * (r:R) * 1 = (r:R) * (r:R)88    ring89  rw [unitS, unitR] at normU90  have squares : (r:R) * (r:R) = (s:R) * (s:R)91    symm92    exact normU93  have nonnegR : (0:R) ≤ r by linarith94  have nonnegS : (0:R) ≤ s by linarith95  have equalScalar :=96      realMulValue.eq_of_square_eq with nonnegR, nonnegS, squares97  refine ⟨equalScalar, ?_⟩98  rw equalScalar at same99  have nonzero : (s:R) ≠ 0100    intro equal101    rw equal at positiveS102    linarith103  apply FunctionBetween.ext with vectorU, vectorV104  intros i hi105  have ui := vector.component_real at u, i with vectorU, hi106  have vi := vector.component_real at v, i with vectorV, hi107  have e1 := vectorScale.entry at s, u, i with scalarS, vectorU, hi108  have e2 := vectorScale.entry at s, v, i with scalarS, vectorV, hi109  have entries : (s:R) * (u(i):R) = (s:R) * (v(i):R)110    rw [← e1, ← e2, same]111    rfl112  have cancel := realInvValue.mul_left with nonzero113  have invReal : realInvValue(s) ∈ ℝ by typecheck114  have expandU : realInvValue(s) * ((s:R) * (u(i):R)) = (u(i):R)115    have regroup : realInvValue(s) * ((s:R) * (u(i):R)) =116      (realInvValue(s) * (s:R)) * (u(i):R)117      ring118    rw [regroup, cancel]119    ring120  have expandV : realInvValue(s) * ((s:R) * (v(i):R)) = (v(i):R)121    have regroup : realInvValue(s) * ((s:R) * (v(i):R)) =122      (realInvValue(s) * (s:R)) * (v(i):R)123      ring124    rw [regroup, cancel]125    ring126  rw [← expandU, ← expandV, entries]127  rfl128129-- The cone over a set of directions: the multiples r u with 0 < r ≤ 1.130def cone (A : Set) : Set :=131  { v ∈ ℝ³ | ∃ u ∈ A, ∃ r ∈ ℝ,132    (0:R) < r ∧ r ≤ (1:R) ∧ v = vectorScale(r, u) }133134theorem cone.subset (A : Set)135  shows cone(A) ⊆ ℝ³136proof137  intros v hv138  have parts := cone.membership.forward with hv139  exact parts.left140141theorem cone.contains (A u r : Set)142  requires hu : u ∈ A143  requires uSpace : u ∈ ℝ³144  requires scalar : r ∈ ℝ145  requires positive : (0:R) < r146  requires bounded : r ≤ (1:R)147  shows vectorScale(r, u) ∈ cone(A)148proof149  have inSpace := vectorScale.space with scalar, uSpace150  exact cone.membership.backward151      with ⟨inSpace, u, hu, r, scalar, positive, bounded, rfl⟩152153theorem cone.monotone (A B : Set)154  requires subset : A ⊆ B155  shows cone(A) ⊆ cone(B)156proof157  intros v hv158  obtain ⟨inSpace, u, hu, r, scalar, positive, bounded, shape⟩ :=159    cone.membership.forward with hv160  have uIn := subset with u, hu161  exact cone.membership.backward162      with ⟨inSpace, u, uIn, r, scalar, positive, bounded, shape⟩163164-- The cone over directions on the sphere lies in the punctured ball.165theorem cone.subset_punctured (A : Set)166  requires subset : A ⊆ S²167  shows cone(A) ⊆ puncturedBall168proof169  intros v hv170  obtain ⟨inSpace, u, hu, r, scalar, positive, bounded, shape⟩ :=171    cone.membership.forward with hv172  obtain ⟨uSpace, uUnit⟩ := S².membership.forward with (subset with u, hu)173  have vectorU := ℝ³.function with uSpace174  have norm := vectorScale.normSq with scalar, vectorU175  rw uUnit at norm176  have unitR : (r:R) * (r:R) * 1 = (r:R) * (r:R)177    ring178  rw unitR at norm179  have nonneg : (0:R) ≤ r by linarith180  have squareBound := realMulValue.square_le_of_le with nonneg, bounded181  have oneOne : (1:R) * (1:R) = (1:R)182    ring183  rw oneOne at squareBound184  have squarePositive :=185      realLess.mul_left_of_positive at (0:R), r, r with positive, positive186  have zeroMul : (r:R) * 0 = 0187    ring188  rw zeroMul at squarePositive189  have scaledSpace := vectorScale.space with scalar, uSpace190  have vBound : normSq(vectorScale(r, u)) ≤ (1:R)191    rw norm192    exact squareBound193  have inBall : vectorScale(r, u) ∈ unitBall :=194    unitBall.membership.backward with ⟨scaledSpace, vBound⟩195  have notZero : vectorScale(r, u) ≠ zeroVector196    intro equal197    rw [equal, zeroVector.normSq] at norm198    linarith199  rw shape200  exact puncturedBall.membership.backward with ⟨inBall, notZero⟩201202-- Disjoint sets of directions have disjoint cones.203theorem cone.disjoint (A B : Set)204  requires boundedA : A ⊆ S²205  requires boundedB : B ⊆ S²206  requires disjoint : Disjoint(A, B)207  shows Disjoint(cone(A), cone(B))208proof209  have apart := Disjoint.iff.forward with disjoint210  apply Disjoint.iff.backward211  intros v hvA hvB212  obtain ⟨inSpace, u, hu, r, scalarR, positiveR, boundedR, shapeU⟩ :=213    cone.membership.forward with hvA214  obtain ⟨inSpace2, w, hw, s, scalarS, positiveS, boundedS, shapeW⟩ :=215    cone.membership.forward with hvB216  have same : vectorScale(r, u) = vectorScale(s, w) by cc217  have uSphere := boundedA with u, hu218  have wSphere := boundedB with w, hw219  have both := vectorScale.sphere_injective with220    scalarR, scalarS, positiveR, positiveS, uSphere, wSphere, same221  rw both.right at hu222  exact apart with w, hu, hw223224-- A rotation carries the cone over S to the cone over the rotated S.225theorem cone.rotate (M : realRing ^ 3 × 3) (S : Set)226  requires hM : M ∈ so3Matrices227  requires subset : S ⊆ S²228  shows translate(spaceAction, ℝ³, M, cone(S)) = cone(translate(sphereAction,229      S², M, S))230proof231  obtain ⟨sphereSubset, closed⟩ := Invariant.sphere232  ext y233  constructor234  . intro hy235    obtain ⟨yIn, x, hx, equal⟩ := translate.membership.forward with hy236    obtain ⟨xIn, u, hu, r, scalar, positive, bounded, shape⟩ :=237      cone.membership.forward with hx238    have uSphere := subset with u, hu239    obtain ⟨uSpace, uUnit⟩ := S².membership.forward with uSphere240    have vectorU := ℝ³.function with uSpace241    have space := spaceAction.apply with hM, xIn242    have sphere := sphereAction.apply with hM, uSphere243    have scaled := matrixVector.scale at M, r, u with scalar, vectorU244    have imageIn := closed with M, hM, u, uSphere245    have shapeBack : M · u = sphereAction(M, u)246      symm247      exact sphere248    have movedIn : M · u ∈ translate(sphereAction, S², M, S) :=249      translate.membership.backward with ⟨imageIn, u, hu, shapeBack⟩250    have imageSpace := S².subset with M · u, imageIn251    rw [equal, space, shape, scaled]252    exact cone.contains with movedIn, imageSpace, scalar, positive, bounded253  . intro hy254    obtain ⟨yIn, w, hw, r, scalar, positive, bounded, shape⟩ :=255      cone.membership.forward with hy256    obtain ⟨wIn, u, hu, wShape⟩ := translate.membership.forward with hw257    have uSphere := subset with u, hu258    obtain ⟨uSpace, uUnit⟩ := S².membership.forward with uSphere259    have vectorU := ℝ³.function with uSpace260    have sphere := sphereAction.apply with hM, uSphere261    rw sphere at wShape262    have scaledIn := cone.contains with hu, uSpace, scalar, positive, bounded263    have scaledSpace := vectorScale.space with scalar, uSpace264    have space := spaceAction.apply with hM, scaledSpace265    have scaled := matrixVector.scale at M, r, u with scalar, vectorU266    have yShape : y = spaceAction(M, vectorScale(r, u))267      rw [space, scaled, ← wShape]268      exact shape269    exact translate.membership.backward270        with ⟨yIn, vectorScale(r, u), scaledIn, yShape⟩271272-- The cone over the sphere is the punctured ball: v = ‖v‖ · (v / ‖v‖).273theorem cone.sphere274  shows cone(S²) = puncturedBall275proof276  apply Subset.antisymmetric277  . exact cone.subset_punctured with (Subset.reflexive at S²)278  . intros v hv279    obtain ⟨inBall, notZero⟩ := puncturedBall.membership.forward with hv280    obtain ⟨inSpace, bound⟩ := unitBall.membership.forward with inBall281    have vector := ℝ³.function with inSpace282    have v0 := vector.component_real at v, 0 with vector, index.zero_mem283    have v1 := vector.component_real at v, 1 with vector, index.one_mem284    have v2 := vector.component_real at v, 2 with vector, index.two_mem285    have sq0 := realMulValue.square_nonnegative at (v(0):R)286    have sq1 := realMulValue.square_nonnegative at (v(1):R)287    have sq2 := realMulValue.square_nonnegative at (v(2):R)288    have normReal : normSq(v) ∈ ℝ by typecheck289    have expand := normSq.value at v290    have normNonneg : (0:R) ≤ normSq(v)291      rw expand292      linarith293    have normNonzero : normSq(v) ≠ (0:R)294      intro zero295      exact notZero with (normSq.eq_zero with vector, zero)296    have nonnegative := NonnegativeReal.of_le with normNonneg297    have rReal := sqrt.real at normSq(v)298    have rIn : sqrt(normSq(v)) ∈ ℝ by typecheck299    have rPositive := sqrt.positive with normNonzero300    have rSquare := sqrt.square at normSq(v)301    have zeroLeOne : (0:R) ≤ (1:R) by linarith302    have oneNonneg := NonnegativeReal.of_le with zeroLeOne303    have rLe := sqrt.le_of_le with nonnegative, oneNonneg, bound304    have oneSquare : (1:R) * (1:R) = (1:R)305      ring306    have sqrtOne := sqrt.of_square at (1:R) with zeroLeOne307    rw oneSquare at sqrtOne308    rw sqrtOne at rLe309    have rNonzero : sqrt(normSq(v)) ≠ 0310      intro equal311      rw equal at rPositive312      linarith313    have invReal : realInvValue(sqrt(normSq(v))) ∈ ℝ by typecheck314    have cancel := realInvValue.mul_left with rNonzero315    have cancel2 := realInvValue.mul_right with rNonzero316    have uSpace := vectorScale.space with invReal, inSpace317    have uNorm := vectorScale.normSq with invReal, vector318    have uUnit : normSq(vectorScale(realInvValue(sqrt(normSq(v))), v)) = (1:R)319      rw uNorm320      calc321        realInvValue(sqrt(normSq(v))) * realInvValue(sqrt(normSq(v))) *322            normSq(v) =323            realInvValue(sqrt(normSq(v))) * realInvValue(sqrt(normSq(v))) *324            (sqrt(normSq(v)) * sqrt(normSq(v))) := by rw rSquare325        _ = (realInvValue(sqrt(normSq(v))) * sqrt(normSq(v))) *326            (realInvValue(sqrt(normSq(v))) * sqrt(normSq(v))) := by ring327        _ = (1:R) * (1:R) := by rw cancel328        _ = (1:R) := by ring329    have uSphere : vectorScale(realInvValue(sqrt(normSq(v))), v) ∈ S² :=330      S².membership.backward with ⟨uSpace, uUnit⟩331    have combine := vectorScale.mul at sqrt(normSq(v)),332        realInvValue(sqrt(normSq(v))), v with rIn, invReal, vector333    have unit := vectorScale.one at v with vector334    have vShape : v = vectorScale(sqrt(normSq(v)),335        vectorScale(realInvValue(sqrt(normSq(v))), v))336      rw [combine, cancel2, unit]337      rfl338    rw vShape339    exact cone.contains with uSphere, uSpace, rIn, rPositive, rLe340341-- Lifting a decomposition of the sphere: each piece and its element are342-- sent to the cone over the piece with the same element.343defgraph conePair (p ∈ 𝒫(S²) × SO3.carrier) : 𝒫(ℝ³) × SO3.carrier :=344  (cone(fst(p)), snd(p))345proof346  obtain ⟨bound, S, hS, g, hg, shape⟩ :=347    product.membership.forward with member348  have coneIn := powerset.membership_iff.backward with (cone.subset at S)349  have firstP := fst.pair at S, g350  have secondP := snd.pair at S, g351  rw [shape, firstP, secondP]352  exact product.pair with coneIn, hg353354theorem conePair.apply (S g : Set)355  requires hS : S ∈ 𝒫(S²)356  requires hg : g ∈ Group.carrier(SO3)357  shows conePair((S, g)) = (cone(S), g)358proof359  have pair := product.pair at S, g, 𝒫(S²), Group.carrier(SO3) with hS, hg360  have value := conePair.value at (S, g) with pair361  have firstP := fst.pair at S, g362  have secondP := snd.pair at S, g363  rw [value, firstP, secondP]364  rfl365366theorem conePair.first (p : Set)367  requires hp : p ∈ 𝒫(S²) × Group.carrier(SO3)368  shows fst(conePair(p)) = cone(fst(p))369proof370  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with hp371  have value := conePair.apply with hS, hg372  have firstP := fst.pair at S, g373  have firstC := fst.pair at cone(S), g374  rw [shape, value, firstP, firstC]375  rfl376377theorem conePair.moved (p : Set)378  requires hp : p ∈ 𝒫(S²) × Group.carrier(SO3)379  shows moved(spaceAction, ℝ³, conePair(p)) =380    cone(moved(sphereAction, S², p))381proof382  obtain ⟨bound, S, hS, g, hg, shape⟩ := product.membership.forward with hp383  have subset := powerset.membership_iff.forward with hS384  have gIn := hg385  rw SO3.carrierOf at gIn386  have matrixG := so3Matrices.matrix with gIn387  have value := conePair.apply with hS, hg388  have rotate := cone.rotate with gIn, subset389  have movedC := moved.value at spaceAction, ℝ³, cone(S), g390  have movedS := moved.value at sphereAction, S², S, g391  rw [shape, value, movedC, movedS]392  exact rotate393394theorem cone.equidecomposable (A B : Set)395  requires boundedA : A ⊆ S²396  requires boundedB : B ⊆ S²397  requires equidecomposable : Equidecomposable(sphereAction, SO3, S², A, B)398  shows Equidecomposable(spaceAction, SO3, ℝ³, cone(A), cone(B))399proof400  obtain ⟨F, finite, bounded, pieces, movedPieces⟩ := equidecomposable401  obtain ⟨piecesBounded, piecesCover, piecesDisjoint⟩ := pieces402  obtain ⟨movedBounded, movedCover, movedDisjoint⟩ := movedPieces403  have function := conePair.function404  have sphereSubset : ∀ p ∈ F, fst(p) ⊆ S²405    intros p hp406    obtain ⟨bound, S, hS, g, hg, shape⟩ :=407        product.membership.forward with (bounded with p, hp)408    rw [shape, fst.pair]409    exact powerset.membership_iff.forward with hS410  have movedSubset : ∀ p ∈ F, moved(sphereAction, S², p) ⊆ S²411    intros p hp412    rw moved.unfold413    exact translate.subset at sphereAction, S², snd(p), fst(p)414  apply Equidecomposable.of_reindex with function, finite, bounded415  . intros p hp416    have first := conePair.first with (bounded with p, hp)417    rw first418    exact cone.monotone with (piecesBounded with p, hp)419  . intros x hx420    obtain ⟨inSpace, u, hu, r, scalar, positive, boundedR, shape⟩ :=421      cone.membership.forward with hx422    obtain ⟨p, hp, member⟩ := piecesCover with u, hu423    have first := conePair.first with (bounded with p, hp)424    have uSpace := S².subset with u, (boundedA with u, hu)425    have scaledIn :=426        cone.contains with member, uSpace, scalar, positive, boundedR427    witness p428    rw [first, shape]429    exact ⟨hp, scaledIn⟩430  . intros p hp q hq different431    have firstP := conePair.first with (bounded with p, hp)432    have firstQ := conePair.first with (bounded with q, hq)433    have apart := piecesDisjoint with p, hp, q, hq, different434    rw [firstP, firstQ]435    exact cone.disjoint with (sphereSubset with p, hp), (sphereSubset with q,436        hq), apart437  . intros p hp438    have move := conePair.moved with (bounded with p, hp)439    rw move440    exact cone.monotone with (movedBounded with p, hp)441  . intros y hy442    obtain ⟨inSpace, w, hw, r, scalar, positive, boundedR, shape⟩ :=443      cone.membership.forward with hy444    obtain ⟨p, hp, member⟩ := movedCover with w, hw445    have move := conePair.moved with (bounded with p, hp)446    have wSpace := S².subset with w, (boundedB with w, hw)447    have scaledIn :=448        cone.contains with member, wSpace, scalar, positive, boundedR449    witness p450    rw [move, shape]451    exact ⟨hp, scaledIn⟩452  . intros p hp q hq different453    have moveP := conePair.moved with (bounded with p, hp)454    have moveQ := conePair.moved with (bounded with q, hq)455    have apart := movedDisjoint with p, hp, q, hq, different456    rw [moveP, moveQ]457    exact cone.disjoint with (movedSubset with p, hp), (movedSubset with q,458        hq), apart459