[Merged by Bors] - feat: add ContinuousSMul instances for ℚ≥0

[astrainfinita]

---

[astrainfinita]

!bench

[github-actions]

PR summary 766e19e781

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Instances.Rat	1195	1197	+2 (+0.17%)

Import changes for all files

Files	Import difference
81 files Mathlib.Analysis.LConvolution Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Normed.Order.Lattice Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Dynamics.Ergodic.Conservative Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.Convolution Mathlib.MeasureTheory.Group.LIntegral Mathlib.MeasureTheory.Group.Measure Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.Indicator Mathlib.MeasureTheory.Integral.Lebesgue.Add Mathlib.MeasureTheory.Integral.Lebesgue.Basic Mathlib.MeasureTheory.Integral.Lebesgue.Countable Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence Mathlib.MeasureTheory.Integral.Lebesgue.Map Mathlib.MeasureTheory.Integral.Lebesgue.Markov Mathlib.MeasureTheory.Integral.Lebesgue.MeasurePreserving Mathlib.MeasureTheory.Integral.Lebesgue.Norm Mathlib.MeasureTheory.Integral.Lebesgue.Sub Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.MeasureTheory.Measure.Support Mathlib.MeasureTheory.Measure.Tight Mathlib.MeasureTheory.Measure.WithDensity Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.Probability.Decision.Risk.Defs Mathlib.Probability.Kernel.Basic Mathlib.Probability.Kernel.Composition.CompMap Mathlib.Probability.Kernel.Composition.CompNotation Mathlib.Probability.Kernel.Composition.CompProd Mathlib.Probability.Kernel.Composition.Comp Mathlib.Probability.Kernel.Composition.KernelLemmas Mathlib.Probability.Kernel.Composition.MapComap Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Probability.Kernel.Composition.Prod Mathlib.Probability.Kernel.Defs Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Proper Mathlib.RingTheory.DividedPowers.Padic Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.Instances.RatLemmas Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.UniformSpace.Dini	1
Mathlib.Topology.Instances.Rat Mathlib.Topology.UniformSpace.CompareReals	2

---

Declarations diff

+ instance : ContinuousSMul ℚ ℝ
+ instance : ContinuousSMul ℚ≥0 NNReal
+ instance {R : Type*} [TopologicalSpace R] [MulAction ℚ R] [MulAction ℚ≥0 R] [IsScalarTower ℚ≥0 ℚ R]

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

[themathqueen]

Is the Algebra ℚ≥0 R hypothesis necessary? Why not show it within the proof for continuous_smul?

[astrainfinita]

The argument of ContinuousSMul ℚ≥0 R needs Algebra ℚ≥0 R. Obtaining it from Algebra ℚ R will cause a diamond.

[themathqueen]

ah, fair enough

[ocfnash]

I don't agree with the claim about the diamond (in fact I claim the opposite!) but it doesn't matter since I have another suggestion.

[astrainfinita]

I think the diamond already exists. Zulip

[ocfnash]

I don't agree with the claim about the diamond (in fact I claim the opposite!) but it doesn't matter since I have another suggestion.

[ocfnash]

Note that via NNRat.instDistribMulActionOfRat we already have an action of ℚ≥0 on R so there is no need to include a typeclass carrying this. Also the Algebra assumption is more than we need and can be weakened to just DistribMulAction. Here is what I suggest:

Suggested change

	instance {R} [Ring R] [TopologicalSpace R] [Algebra ℚ R] [Algebra ℚ≥0 R] [ContinuousSMul ℚ R] :
	ContinuousSMul ℚ≥0 R where
	continuous_smul := by
	convert continuous_induced_dom.fst'.smul (M := ℚ) (X := R) continuous_snd using 2
	rw [← cast_smul_eq_nnqsmul ℚ]
	rfl
	instance {R : Type*} [Ring R] [DistribMulAction ℚ R] [TopologicalSpace R] [ContinuousSMul ℚ R] :
	ContinuousSMul ℚ≥0 R where
	continuous_smul := continuous_induced_dom.fst'.smul continuous_snd

[leanprover-community-mathlib4-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit 94eb313.
The entire run failed.
Found no significant differences.

[ocfnash]

I've left some suggestions; feel free to revert to your original design if these give trouble.

Thanks!

bors d+

[mathlib-bors]

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

[astrainfinita]

bors r+

[mathlib-bors]

Build failed:

• Post-Build Step

[ocfnash]

I think this failed because of a silly disk space error so let's try again

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Post-Build Step
• Build