Theorems · Definition · real analysis
BoxIntegral.IntegrationParams.bDistortion
BoxIntegral.IntegrationParams → Bool
true if r can depend on the maximal ratio of sides of the
same box of a partition. Presence of this case makes quite a few proofs harder but we can prove
the divergence theorem only for the filter BoxIntegral.IntegrationParams.GP = ⊥ =
{bRiemann := false, bHenstock := true, bDistortion := true}.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- BoxIntegral.IntegrationParamsstatement and proof · cited by 101
Cited by20
Results whose statement or proof uses this declaration.
- BoxIntegral.IntegrationParams.MemBaseSet.distortion_lestatement · cited by 6
- BoxIntegral.IntegrationParams.MemBaseSet.exists_complstatement · cited by 3
- BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eqproof · cited by 2
- BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleOstatement and proof · cited by 2
- BoxIntegral.IntegrationParams.MemBaseSet.mono'proof · cited by 2
- BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSetproof · cited by 2
- tendsto_tsum_div_pow_atTop_integralproof · cited by 1
- BoxIntegral.IntegrationParams.biUnionTagged_memBaseSetstatement and proof · cited by 1
- BoxIntegral.IntegrationParams.extstatement and proof · cited by 1
- BoxIntegral.hasIntegral_GP_pderivproof · cited by 1
- BoxIntegral.IntegrationParams.MemBaseSet.exists_common_complstatement and proof · cited by 1