Commit 2023-06-06 15:53 49f3a15a

View on Github →

feat: port Analysis.BoxIntegral.Basic (#4695)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/BoxIntegral/Basic.lean

added theorem BoxIntegral.HasIntegral.integrable

added theorem BoxIntegral.HasIntegral.integral_eq

added theorem BoxIntegral.HasIntegral.mcShane_of_forall_isLittleO

added theorem BoxIntegral.HasIntegral.mono

added theorem BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO

added theorem BoxIntegral.HasIntegral.of_le_Henstock_of_forall_isLittleO

added theorem BoxIntegral.HasIntegral.of_mul

added theorem BoxIntegral.HasIntegral.smul

added theorem BoxIntegral.HasIntegral.sub

added theorem BoxIntegral.HasIntegral.sum

added theorem BoxIntegral.HasIntegral.tendsto

added theorem BoxIntegral.HasIntegral.unique

added def BoxIntegral.HasIntegral

added theorem BoxIntegral.Integrable.add

added theorem BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion

added def BoxIntegral.Integrable.convergenceR

added theorem BoxIntegral.Integrable.convergenceR_cond

added theorem BoxIntegral.Integrable.dist_integralSum_integral_le_of_memBaseSet

added theorem BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet

added theorem BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet

added theorem BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq

added theorem BoxIntegral.Integrable.mono

added theorem BoxIntegral.Integrable.neg

added theorem BoxIntegral.Integrable.of_neg

added theorem BoxIntegral.Integrable.of_smul

added theorem BoxIntegral.Integrable.smul

added theorem BoxIntegral.Integrable.sub

added theorem BoxIntegral.Integrable.sum_integral_congr

added theorem BoxIntegral.Integrable.tendsto_integralSum_sum_integral

added theorem BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity

added theorem BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single

added def BoxIntegral.Integrable.toBoxAdditive

added theorem BoxIntegral.Integrable.to_subbox

added theorem BoxIntegral.Integrable.to_subbox_aux

added def BoxIntegral.Integrable

added theorem BoxIntegral.hasIntegral_const

added theorem BoxIntegral.hasIntegral_iff

added theorem BoxIntegral.hasIntegral_zero

added theorem BoxIntegral.integrable_const

added theorem BoxIntegral.integrable_iff_cauchy

added theorem BoxIntegral.integrable_iff_cauchy_basis

added theorem BoxIntegral.integrable_neg

added theorem BoxIntegral.integrable_of_continuousOn

added theorem BoxIntegral.integrable_zero

added def BoxIntegral.integral

added def BoxIntegral.integralSum

added theorem BoxIntegral.integralSum_add

added theorem BoxIntegral.integralSum_biUnionTagged

added theorem BoxIntegral.integralSum_biUnion_partition

added theorem BoxIntegral.integralSum_disjUnion

added theorem BoxIntegral.integralSum_fiberwise

added theorem BoxIntegral.integralSum_inf_partition

added theorem BoxIntegral.integralSum_neg

added theorem BoxIntegral.integralSum_smul

added theorem BoxIntegral.integralSum_sub_partitions

added theorem BoxIntegral.integral_add

added theorem BoxIntegral.integral_const

added theorem BoxIntegral.integral_neg

added theorem BoxIntegral.integral_nonneg

added theorem BoxIntegral.integral_smul

added theorem BoxIntegral.integral_sub

added theorem BoxIntegral.integral_zero

added theorem BoxIntegral.norm_integral_le_of_le_const

added theorem BoxIntegral.norm_integral_le_of_norm_le

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

modified theorem BoxIntegral.BoxAdditiveMap.coe_inj

modified theorem BoxIntegral.BoxAdditiveMap.coe_injective

Modified Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

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

Modified Mathlib/Analysis/BoxIntegral/Partition/Measure.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean