feat(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map

[mans0954]

Three lemmas about Quadratic maps applied to:

• A finite sum
• A linearCombination
• The representation of an element wrt a basis

---

[github-actions]

PR summary 1b0044bc2f

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Sym.Sym2	481	485	+4 (+0.83%)
Mathlib.LinearAlgebra.QuadraticForm.Basis	1432	1434	+2 (+0.14%)

Import changes for all files

Files	Import difference
20 files Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.Density Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.SetTheory.Game.Birthday Mathlib.SetTheory.Game.Domineering Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Ordinal Mathlib.SetTheory.Game.Short Mathlib.SetTheory.Game.State Mathlib.SetTheory.Surreal.Basic	1
Mathlib.LinearAlgebra.QuadraticForm.Basis	2
6 files Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Sum	3
29 files Mathlib.Algebra.BigOperators.Sym Mathlib.Combinatorics.Digraph.Orientation Mathlib.Combinatorics.SimpleGraph.Basic Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Dart Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.LineGraph Mathlib.Combinatorics.SimpleGraph.Maps Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Path Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Subgraph Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Combinatorics.SimpleGraph.Turan Mathlib.Combinatorics.SimpleGraph.Walk Mathlib.Data.Finset.Sym Mathlib.Data.List.Sym Mathlib.Data.Multiset.Sym Mathlib.Data.Sym.Card Mathlib.Data.Sym.Sym2.Order Mathlib.Data.Sym.Sym2 Mathlib.Order.GameAdd Mathlib.SetTheory.Game.Basic Mathlib.SetTheory.Game.Impartial Mathlib.SetTheory.Game.PGame Mathlib.SetTheory.ZFC.Ordinal	4
Mathlib.LinearAlgebra.Finsupp.Sym2 (new file)	535

---

Declarations diff

+ CommMagmaMulZeroClass
+ Finsupp.coe_pointwise_module_smul
+ Finsupp.hMul
+ Sym2.mem_support_sym2_of_mul_ne_zero
+ Sym2.mul_finsupp
+ Sym2.mul_finsupp_support
+ apply_linearCombination
+ apply_linearCombination'
+ instance [CommSemiring R] : CommMagmaMulZeroClass R
+ map_finsuppSum
+ map_finsuppSum'
+ mul
+ mul_sym2Mk
+ polarSym2_map_hMul
+ polarSym2_map_mul
+ smul
+ sum_polar_sub_repr_sq
+ sum_repr_sq_add_sum_repr_mul_polar
+ support_mul_self

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).

[mans0954]

CC: @eric-wieser

[eric-wieser]

I think inheriting a * from a smul in this way is not an established pattern in mathlib. This would maybe be a little less objectionable if it used HSMul, but fundamentally the heterogenous classes create nasty diamond issues (which I touch on briefly in Section 4.8 of my thesis.

[mans0954]

Presumably I should make it a def instead? https://github.com/leanprover-community/mathlib4/pull/18578/files#diff-b2e63ded24baf2b6dbf29bf1c8d5ff01b0db9b4201ce0726503848038e25b241R30

[mans0954]

@eric-wieser @YaelDillies I think I've got as far as I can with this if you're able to take another look please?