[Merged by Bors] - feat: add theorem about the norm of cross products by guptbot · Pull Request #20920 · leanprover-community/mathlib4

guptbot · 2025-01-21T17:17:33Z

Add and prove the equality between the norm of a cross-product of two vectors and the product of the norms of the individual vectors and the sine of the angle between them. See crossProduct_norm_eq_norm_mul_norm_mul_sin.

github-actions · 2025-01-21T17:18:26Z

PR summary 31a021f3f7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct` (new file)	1833

Declarations diff

+ norm_withLpEquiv_crossProduct
+ norm_withLpEquiv_symm_crossProduct
+ sin_angle_nonneg

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

jsm28 · 2025-01-22T01:53:41Z

I think you should put the result about cross product in a separate file, since cross products are irrelevant to most uses of angles (just as the results about conformal maps and angles go in a separate file to avoid introducing irrelevant dependencies on calculus for most users).

jsm28 · 2025-01-22T01:56:44Z

Also, the fact that you need a definition l2norm shows that using the existing cross product definition on EuclideanSpace ℝ (Fin 3) is a code smell, because it produces a result with the wrong type. Rather, you should probably have a separate definition of the cross product for Euclidean space, producing a result in Euclidean space (API for that definition can mostly be deduced from that for the existing cross product via defeq).

guptbot · 2025-01-25T05:28:03Z

@jsm28 I'll move the cross product result to a separate file. Regarding your second comment, could you help me understand what the right way to address this might be? I could make a separate definition for cross products using EuclideanSpace as inputs/outputs. But then porting over every cross product theorem to this new definition (even though the proof may be simple through defeq) doesn't feel right. It seems to me that a better cross product definition should simultaneously work for both input types, and just return the appropriate output type. However, I'm unsure about what the best way to implement this would be. Any help is greatly appreciated :)

jsm28 · 2025-01-25T12:04:46Z

I suggest asking on Zulip about how to avoid duplication of cross product API. My guess is that it might be possible to do something in meta code that controls the elaboration of ×₃ to prefer producing an output that is the same type as the inputs (rather than merely defeq), for example. Alternatively, you could redefine crossProduct to be more general, so that rather than working only on (Fin 3 → R) it works on an arbitrary module given a linear equivalence between that module and (Fin 3 → R), which avoids meta code though I don't know if it would make things more awkward to use in practice (e.g. cross_apply would involve a load of applications of that equivalence and its inverse).

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

jsm28 · 2025-01-27T02:44:18Z

Note that the new lemma and imports still need to move to a new file such as Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct to avoid import creep.

jsm28 · 2025-01-27T02:44:58Z

(sin_angle_nonneg makes sense in the existing file.)

Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean

eric-wieser · 2025-02-05T22:04:39Z

Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean

+
+assert_not_exists HasFDerivAt ConformalAt
+
+noncomputable section


I would guess you don't need this.

I meant the noncomputable section on the line I commented on, not the assert_not_exists that was in the context that github chose to show! Though getting rid of both also seems fine.

Gotcha, Ill remove both!

eric-wieser · 2025-02-05T22:05:08Z

Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean

+open Real
+
+open Matrix


nit:

Suggested change

open Real

open Matrix

open Real

open Matrix

eric-wieser

bors d+

Thanks!

mathlib-bors · 2025-02-05T22:05:31Z

✌️ Mr-vedant-gupta can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

guptbot · 2025-02-05T22:11:28Z

bors r+

Add and prove the equality between the norm of a cross-product of two vectors and the product of the norms of the individual vectors and the sine of the angle between them. See `crossProduct_norm_eq_norm_mul_norm_mul_sin`. Co-authored-by: Mr-vedant-gupta <91429389+Mr-vedant-gupta@users.noreply.github.com>

mathlib-bors · 2025-02-05T22:21:09Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: chore: update Mathlib dependencies 2025-02-06 (#21523) fix(MathlibTest/TransImports): stop inspecting the `Lean` package (#21492) style(Mathlib/Computability/Halting): `RePred` to `REPred` (#21216) feat(Data/Set/Card): add `ncard_le_encard` (#21467) feat(Order): lemmas for `Order.succ` and `Order.pred` in `Fin` (#21437) feat(LinearAlgebra/LinearIndependent): linear independence + subsingletons (#21511) feat: for continuous linear maps in a normed ring, `flip mul = mul` (#21507) chore(GroupTheory/Commutator): don't import `Ring` (#21296) chore(Data/Complex/Abs): add `protected` to results that already exists in root namespace (#21454) chore(*): `erw`s that can now become `rw`s (#21510) chore: allow create-adaptation-pr.sh to continue when bump branch already exists (#21486) feat(CategoryTheory): equivalence between `Ind C` and left exact functors from `C` to `Type` (#21430) chore: add test to TCSynth.lean (#21499) feat: the category of ind-objects satisfies the AB5 axiom (#21350) refactor(RepresentationTheory): `ConcreteCategory` instances for `Rep` (#21465) chore: split Mathlib.Order.Filter.Basic (#21403) chore: update Mathlib dependencies 2025-02-06 (#21487) chore(Cache): Add support for $MATHLIB_CACHE_DIR (#21480) feat(CategoryTheory): a closed monoidal category is an ordinary enriched category over itself (#21436) feat(AlgebraicTopology): notation X ^[n] for cosimplicial objects (#21485) chore: upgrade dependencies manually (#21484) refactor(Analysis/Normed): `ConcreteCategory` refactor for `SemiNormedGrp` (#21477) refactor(LinearAlgebra): `ConcreteCategory` instance for `QuadraticModuleCat` (#21471) refactor(MeasureTheory): `ConcreteCategory` instance for `MeasCat` (#21468) refactor(Topology/Category): clean up remaining uses of `HasForget` (#21458) refactor(CategoryTheory): `ConcreteCategory` instances for pointed types (#21470) feat(CategoryTheory/Action): `ConcreteCategory` instances for `Action` (#21462) feat(CategoryTheory): `ConcreteCategory` instance for `DifferentialObject` (#21464) feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk` (#18178) chore: rename `encard_le_card` to `encard_le_encard` (#21426) feat: add theorem about the norm of cross products (#20920) feat(Data/Matroid/Circuit): circuit elimination and finitary matroids (#21172) feat(LinearAlgebra/ExteriorPower): add iMulti_family definition for product of a family of vectors (#21397)

Add and prove the equality between the norm of a cross-product of two vectors and the product of the norms of the individual vectors and the sine of the angle between them. See `crossProduct_norm_eq_norm_mul_norm_mul_sin`. Co-authored-by: Mr-vedant-gupta <91429389+Mr-vedant-gupta@users.noreply.github.com>

Mr-vedant-gupta added 3 commits January 21, 2025 10:52

initial commit

b5f3107

clean up

916dd86

add docstring

55aba8c

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! large-import Automatically added label for PRs with a significant increase in transitive imports labels Jan 21, 2025

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 21, 2025

try moving changes to Angle directory to reduce additional imports

2f9e90b

tb65536 reviewed Jan 21, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean Outdated Show resolved Hide resolved

Play better golf

b407612

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

tb65536 reviewed Jan 21, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean Outdated Show resolved Hide resolved

fix lemma ordering

7d9e2a2

tb65536 reviewed Jan 21, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean Outdated Show resolved Hide resolved

fix trailing spaces and import ordering

03d71dd

eric-wieser reviewed Jan 26, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 26, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean Outdated Show resolved Hide resolved

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 26, 2025

explicit conversion of cross product output to euclidean space

6e02120

eric-wieser reviewed Jan 27, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean Outdated Show resolved Hide resolved

move results to new file

4874aff

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 27, 2025

fix docstring

88c8d63

eric-wieser reviewed Jan 27, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean Show resolved Hide resolved

eric-wieser reviewed Jan 27, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean Outdated Show resolved Hide resolved

add identical theorem for different input type

20d3c92

eric-wieser reviewed Feb 5, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 5, 2025

View reviewed changes

Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean Outdated Show resolved Hide resolved

Mr-vedant-gupta added 2 commits February 5, 2025 16:53

update docstrings

24004e3

fix docstring formatting

dcd298a

eric-wieser reviewed Feb 5, 2025

View reviewed changes

eric-wieser approved these changes Feb 5, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 5, 2025

Mr-vedant-gupta added 2 commits February 5, 2025 17:07

nits

6652d5d

nits

31a021f

mathlib-bors bot changed the title ~~feat: add theorem about the norm of cross products~~ [Merged by Bors] - feat: add theorem about the norm of cross products Feb 5, 2025

mathlib-bors bot closed this Feb 5, 2025

mathlib-bors bot deleted the cross-product-norm branch February 5, 2025 22:21


		assert_not_exists HasFDerivAt ConformalAt

		noncomputable section

Conversation

guptbot commented Jan 21, 2025 • edited by tb65536 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 31a021f3f7

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jsm28 commented Jan 22, 2025

Uh oh!

jsm28 commented Jan 22, 2025

Uh oh!

guptbot commented Jan 25, 2025

Uh oh!

jsm28 commented Jan 25, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jsm28 commented Jan 27, 2025

Uh oh!

jsm28 commented Jan 27, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser Feb 5, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Feb 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

guptbot Feb 5, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Feb 5, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Feb 5, 2025

Uh oh!

guptbot commented Feb 5, 2025

Uh oh!

mathlib-bors bot commented Feb 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

guptbot commented Jan 21, 2025 •

edited by tb65536

Loading

github-actions bot commented Jan 21, 2025 •

edited

Loading

eric-wieser Feb 5, 2025 •

edited

Loading