Theorems · Definition · real analysis
BoxIntegral.Box.distortion
{ι : Type u_1} → [Fintype ι] → BoxIntegral.Box ι → NNRealThe distortion of a box I is the maximum of the ratios of the lengths of its edges.
It is defined as the maximum of the ratios
nndist I.lower I.upper / nndist (I.lower i) (I.upper i).
- Defined in
- Mathlib.Analysis.BoxIntegral.Box.Basic
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- NNRealstatement · cited by 4,310
- Finset.univproof · cited by 3,473
- Finset.supproof · cited by 530
- BoxIntegral.Boxstatement and proof · cited by 464
- NNDist.nndistproof · cited by 235
- BoxIntegral.Box.upperproof · cited by 70
- BoxIntegral.Box.lowerproof · cited by 65
Cited by22
Results whose statement or proof uses this declaration.
- BoxIntegral.Prepartition.distortionproof · cited by 23
- BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleOstatement and proof · cited by 2
- BoxIntegral.Box.nndist_le_distortion_mulstatement · cited by 1
- BoxIntegral.Box.diam_Icc_le_of_distortion_lestatement and proof · cited by 1
- BoxIntegral.Box.dist_le_distortion_mulstatement and proof · cited by 1
- BoxIntegral.Box.distortion_eq_of_sub_eq_divstatement · cited by 1
- BoxIntegral.IntegrationParams.exists_memBaseSet_isPartitionstatement and proof · cited by 1
- BoxIntegral.hasIntegral_GP_pderivproof · cited by 1
- BoxIntegral.Box.exists_taggedPartition_isHenstock_isSubordinate_homotheticstatement and proof · cited by 1
- BoxIntegral.Prepartition.distortion_topstatement · cited by 1