Commit 2023-05-25 11:24 acca960b

View on Github →

feat: port Analysis.BoxIntegral.Partition.Filter (#4126)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

added def BoxIntegral.IntegrationParams.GP

added def BoxIntegral.IntegrationParams.Henstock

added def BoxIntegral.IntegrationParams.McShane

added theorem BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl

added theorem BoxIntegral.IntegrationParams.MemBaseSet.mono'

added theorem BoxIntegral.IntegrationParams.MemBaseSet.mono

added structure BoxIntegral.IntegrationParams.MemBaseSet

added theorem BoxIntegral.IntegrationParams.RCond.mono

added def BoxIntegral.IntegrationParams.RCond

added def BoxIntegral.IntegrationParams.Riemann

added theorem BoxIntegral.IntegrationParams.biUnionTagged_memBaseSet

added def BoxIntegral.IntegrationParams.equivProd

added theorem BoxIntegral.IntegrationParams.eventually_isPartition

added theorem BoxIntegral.IntegrationParams.exists_memBaseSet_isPartition

added theorem BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq

added theorem BoxIntegral.IntegrationParams.gp_le

added theorem BoxIntegral.IntegrationParams.hasBasis_toFilter

added theorem BoxIntegral.IntegrationParams.hasBasis_toFilterDistortion

added theorem BoxIntegral.IntegrationParams.hasBasis_toFilterDistortioniUnion

added theorem BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion

added theorem BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top

added theorem BoxIntegral.IntegrationParams.henstock_le_mcShane

added theorem BoxIntegral.IntegrationParams.henstock_le_riemann

added def BoxIntegral.IntegrationParams.isoProd

added theorem BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_false

added theorem BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top

added def BoxIntegral.IntegrationParams.toFilter

added def BoxIntegral.IntegrationParams.toFilterDistortion

added theorem BoxIntegral.IntegrationParams.toFilterDistortion_mono

added def BoxIntegral.IntegrationParams.toFilterDistortioniUnion

added theorem BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot

added theorem BoxIntegral.IntegrationParams.toFilter_inf_iUnion_eq

added theorem BoxIntegral.IntegrationParams.toFilter_mono

added def BoxIntegral.IntegrationParams.toFilteriUnion

added theorem BoxIntegral.IntegrationParams.toFilteriUnion_congr

added theorem BoxIntegral.IntegrationParams.toFilteriUnion_mono

added structure BoxIntegral.IntegrationParams