Commit 2024-08-09 00:58 86d8be68

View on Github →

chore: backports for leanprover/lean4#4814 (part 34) (#15607)

Estimated changes

Modified Mathlib/Algebra/Lie/Derivation/Killing.lean

modified theorem LieDerivation.IsKilling.killingForm_restrict_range_ad

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

deleted theorem LieAlgebra.IsKilling.restrict_killingForm

added theorem LieAlgebra.restrict_killingForm

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

modified theorem LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add

modified theorem LieAlgebra.IsKilling.chainBotCoeff_zero_right

modified theorem LieAlgebra.IsKilling.chainLength_zero_right

modified theorem LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add

modified theorem LieAlgebra.IsKilling.chainTopCoeff_zero_right

modified theorem LieAlgebra.IsKilling.eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul

modified theorem LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top

modified theorem LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt

modified theorem LieAlgebra.IsKilling.rootSpace_one_div_two_smul

modified theorem LieAlgebra.IsKilling.rootSpace_two_smul

modified theorem LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff

modified theorem LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem

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

modified theorem BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl

Modified Mathlib/Analysis/Calculus/BumpFunction/Normed.lean

modified theorem ContDiffBump.normed_le_div_measure_closedBall_rIn

Modified Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean

Modified Mathlib/Analysis/Convolution.lean

modified theorem MeasureTheory.integral_posConvolution

Modified Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

modified theorem ae_eq_zero_of_integral_smooth_smul_eq_zero

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

modified theorem ContMDiffOn.contMDiffOn_tangentMapWithin

modified theorem TangentBundle.tangentMap_tangentBundle_pure

Modified Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

modified theorem UniqueMDiffOn.uniqueDiffOn_inter_preimage

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

modified structure SmoothBumpCovering

Modified Mathlib/Geometry/Manifold/PoincareConjecture.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/Hom.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

modified theorem MeasureTheory.average_pair

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

modified theorem MeasureTheory.tendsto_integral_norm_approxOn_sub

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

modified theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae

modified theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge'

modified theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le'

Modified Mathlib/MeasureTheory/Integral/IntervalAverage.lean

Modified Mathlib/MeasureTheory/Measure/DiracProba.lean

modified theorem MeasureTheory.diracProba_diracProbaInverse

modified theorem MeasureTheory.embedding_diracProba

Modified Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean

modified theorem MeasureTheory.integral_comp

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

modified theorem MeasureTheory.ProbabilityMeasure.continuous_toLevyProkhorov

modified theorem MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le

modified def MeasureTheory.homeomorph_probabilityMeasure_levyProkhorov

modified theorem MeasureTheory.levyProkhorov_eq_convergenceInDistribution

Modified Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean

modified theorem MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq

modified theorem MeasureTheory.Integrable.withDensityᵥ_eq_iff

Modified Mathlib/Probability/Density.lean

modified theorem MeasureTheory.pdf.integral_pdf_smul

Modified Mathlib/Probability/Independence/ZeroOne.lean

modified theorem ProbabilityTheory.indep_biSup_compl

modified theorem ProbabilityTheory.indep_biSup_limsup

modified theorem ProbabilityTheory.indep_iSup_directed_limsup

modified theorem ProbabilityTheory.indep_iSup_limsup

modified theorem ProbabilityTheory.indep_limsup_atBot_self

modified theorem ProbabilityTheory.indep_limsup_atTop_self

modified theorem ProbabilityTheory.indep_limsup_self

modified theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup

modified theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot

modified theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop

Modified Mathlib/Probability/Kernel/CondDistrib.lean

Modified Mathlib/Probability/Kernel/Condexp.lean

modified theorem ProbabilityTheory.condexpKernel_ae_eq_condexp'

modified theorem ProbabilityTheory.condexpKernel_ae_eq_condexp

modified theorem ProbabilityTheory.condexpKernel_ae_eq_trim_condexp

Modified Mathlib/Probability/Kernel/Disintegration/Basic.lean

Modified Mathlib/Probability/Kernel/IntegralCompProd.lean