feat: Nesbitt's inequality

[vihdzp]

We prove Nesbitt's inequality 3 / 2 ≤ a / (b + c) + b / (c + a) + c / (b + a) for a linearly ordered semifield, by reduction to Sedrakyan's lemma.

---

• depends on: chore: move results on Σ i : Fin n, f i earlier #19415

[github-actions]

PR summary 0cfd0a78d4

Import changes exceeding 2%

%	File
+4.41%	Mathlib.Algebra.Order.BigOperators.Ring.Finset

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.BigOperators.Ring.Finset	657	686	+29 (+4.41%)

Import changes for all files

Files	Import difference
21 files Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Polynomial.CauchyBound Mathlib.NumberTheory.Primorial Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Field.Basic Mathlib.Data.Real.IsNonarchimedean Mathlib.Algebra.Squarefree.Basic Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Topology.MetricSpace.Algebra Mathlib.Analysis.Normed.MulAction Mathlib.RingTheory.ChainOfDivisors Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Combinatorics.Enumerative.Bell Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Analysis.Normed.Field.Ultra Mathlib.Data.Nat.Choose.Multinomial Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Ring.Ultra Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.NullSubmodule	1
34 files Mathlib.Analysis.Subadditive Mathlib.Topology.Instances.CantorSet Mathlib.Data.Real.Sqrt Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Topology.UniformSpace.CompareReals Mathlib.Topology.Order.Bounded Mathlib.Data.Complex.Exponential Mathlib.Topology.Homotopy.Basic Mathlib.Topology.Instances.Real Mathlib.AlgebraicTopology.SingularSet Mathlib.Topology.Instances.Rat Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Algebra.Star.CHSH Mathlib.Order.Filter.ENNReal Mathlib.Topology.UnitInterval Mathlib.Data.Real.StarOrdered Mathlib.Topology.Connected.PathConnected Mathlib.Topology.Instances.EReal Mathlib.Data.Complex.Order Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.Data.Complex.Abs Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Instances.NNReal Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Topology.Semicontinuous Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Topology.Instances.ENNReal Mathlib.MeasureTheory.OuterMeasure.BorelCantelli	3
53 files Mathlib.Topology.Instances.Nat Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Algebra.Order.Hom.Ultra Mathlib.Topology.Instances.PNat Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.Instances.Int Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Topology.MetricSpace.Sequences Mathlib.NumberTheory.MulChar.Basic Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.Oscillation Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Lipschitz Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Dilation Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.SetTheory.Nimber.Field Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Analysis.NormedSpace.MStructure Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.Topology.EMetricSpace.Basic Mathlib.Analysis.Normed.Group.Bounded Mathlib.Topology.Metrizable.Basic Mathlib.Analysis.Normed.Group.Int Mathlib.Algebra.Order.Hom.Normed Mathlib.Data.ZMod.Factorial Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.MetricSpace.Gluing Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.InformationTheory.Hamming Mathlib.Analysis.Normed.Group.Submodule Mathlib.Algebra.CharP.Two Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.Normed.Group.Constructions Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.Normed.Group.Basic Mathlib.Topology.MetricSpace.Bounded	4
5 files Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.MetricSpace.Pseudo.Constructions	8
11 files Mathlib.Data.NNReal.Basic Mathlib.Data.ENNReal.Inv Mathlib.Data.Real.ConjExponents Mathlib.Topology.EMetricSpace.Defs Mathlib.Algebra.Order.BigOperators.Expect Mathlib.Topology.MetricSpace.Defs Mathlib.Data.ENNReal.Real Mathlib.Data.ENNReal.Operations Mathlib.Data.Real.EReal Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Topology.MetricSpace.MetricSeparated	10
Mathlib.Combinatorics.SetFamily.KruskalKatona	15
Mathlib.Combinatorics.Additive.Energy	18
Mathlib.NumberTheory.Multiplicity Mathlib.NumberTheory.Basic	19
5 files Mathlib.NumberTheory.Padics.PadicNorm Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.NumberTheory.FactorisationProperties Mathlib.Algebra.Order.CauSeq.BigOperators Mathlib.Algebra.CharP.Reduced	23
4 files Mathlib.Data.Nat.Multiplicity Mathlib.Algebra.CharP.ExpChar Mathlib.RingTheory.Nilpotent.Basic Mathlib.Algebra.CharP.Lemmas	24
Mathlib.Combinatorics.Colex Mathlib.Algebra.GeomSum	25
3 files Mathlib.Data.NNRat.BigOperators Mathlib.Algebra.Order.BigOperators.Ring.Finset Mathlib.Data.Nat.Factorial.BigOperators	29

---

Declarations diff

+ three_div_two_le_sum_div_add

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

[YaelDillies]

Given that Algebra.Order.BigOperators.Ring.Finset is the entry point of the API of big operators on ordered rings, can you please keep their imports at a minimum by moving this to a new file/doing a preliminary split?

[vihdzp]

I'm not exactly sure what causes the import spike, Mathlib.Tactic.FinCases and Mathlib.Data.Fin.VecNotation should both be very lightweight files.

Is Mathlib.Algebra.BigOperators.Fin the issue? All I'm using from it is Fin.sum_univ_three, which can surely be moved much earlier.

[YaelDillies]

As indicated by its name, Algebra.BigOperators.Fin hasn't been split into Group-/GroupWithZero-/Ring-specific files, so you should generally consider it heavy.

It is not very hard to split it if you would like to

[vihdzp]

Yeah, I'll split it in a dependent PR. Seems a bit ridiculous that a lemma like Σ i : Fin 3, f i = f 0 + f 1 + f 2 is what's causing my import spike.

To clarify, what would the new files be named? Would it be Algebra.BigOperators.(Group/GroupWithZero/Ring).Fin?

[YaelDillies]

Hopefully, you don't need a new file at all, and Algebra.BigOperators.Group.Finset will do

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• chore: move results on Σ i : Fin n, f i earlier #19415
  By Dependent Issues (🤖). Happy coding!

[vihdzp]

On a more mathematical note, I just realized that the specific application of Sedrakyan used in this proof is the exact one used to prove AM-HM, so I'll rework this PR to do that first.