feat(Geometry/Convex/Cone): linear span of conic span of set equals linear span of set

[bjornsolheim]

• Prove that the linear span of the conic span of a subset equals the linear span of the subset.
• This is a specialization of Submodule.span_span_of_tower to pointed cones.

---

[github-actions]

PR summary e43846c17c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ span_span_eq_span

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

[ocfnash]

Both of these exist as instances. You can check this by writing:

#synth SMul R≥0 R
#synth IsScalarTower R≥0 R E

just above the lemma and Lean will provide clickable link to the instance or you can just delete them and observe as follows:

Suggested change

	Submodule.span R (PointedCone.span R s : Set E) = Submodule.span R s := by
	letI : SMul R≥0 R := ⟨fun ⟨c, _⟩ r => c * r⟩
	letI : IsScalarTower R≥0 R E := ⟨fun ⟨c, _⟩ r m => mul_smul c r m⟩
	exact Submodule.span_span_of_tower R≥0 R s
	Submodule.span R (PointedCone.span R s : Set E) = Submodule.span R s :=
	Submodule.span_span_of_tower R≥0 R s

Given the above, as well as the fact that PointedCone.span is already an abbrev I don't think we should introduce this lemma, since it is just an alias for Submodule.span_span_of_tower.

[ocfnash]

Thanks for your work. Unfortunately I'm going to close this PR since the proposed lemmas ends up just being an alias for Submodule.span_span_of_tower.

[bjornsolheim]

Of course. This was on me. Thank you for explaining the reasoning and relevant techniques.