MellinCalculus

📁 Source: PrimeNumberTheoremAnd/MellinCalculus.lean

Statistics

Metric	Count
Definitions `DeltaSpike`, `MellinConvolution`, `Smooth1`	3
Theorems `ofReal_rpow`, `DeltaSpikeContinuous`, `DeltaSpikeMass`, `DeltaSpikeNonNeg_of_NonNeg`, `DeltaSpikeOfRealContinuous`, `DeltaSpikeSupport`, `DeltaSpikeSupport'`, `DeltaSpikeSupport_aux`, `BigO_zero_atTop_of_support_in_Icc`, `BigO_zero_atZero_of_support_in_Icc`, `TendstoAtTop_of_support_in_Icc`, `TendstoAtZero_of_support_in_Icc`, `support_abs`, `support_deriv_subset_Icc`, `support_mul_subset_of_subset`, `support_ofReal`, `support_of_along_fiber_subset_subset`, `integral_eq_integral_of_support_subset_Icc`, `integral_comp_div_I0i_haar`, `integral_comp_inv_I0i_haar`, `integral_comp_mul_left_I0i_haar`, `integral_comp_mul_right_I0i_haar`, `integral_comp_mul_right_I0i_haar_real`, `integral_comp_rpow_I0i_haar_real`, `setIntegral_integral_swap`, `MellinConvNonNeg_of_NonNeg`, `MellinConvolutionSymmetric`, `MellinConvolutionTransform`, `MellinOf1`, `MellinOfDeltaSpike`, `MellinOfDeltaSpikeAt1`, `MellinOfDeltaSpikeAt1_asymp`, `MellinOfPsi`, `MellinOfPsi_aux`, `MellinOfSmooth1a`, `MellinOfSmooth1b`, `MellinOfSmooth1c`, `PartialIntegration`, `PartialIntegration_of_support_in_Icc`, `integral_eq_integral_inter_of_support_subset`, `integral_eq_integral_inter_of_support_subset_Icc`, `Smooth1ContinuousAt`, `Smooth1LeOne`, `Smooth1LeOne_aux`, `Smooth1MellinConvergent`, `Smooth1MellinDifferentiable`, `Smooth1Nonneg`, `Smooth1Properties_above`, `Smooth1Properties_above_aux`, `Smooth1Properties_above_aux2`, `Smooth1Properties_below`, `Smooth1Properties_below_aux`, `Smooth1Properties_estimate`, `Smooth1_def_ite`, `comp_ofReal'`, `ofReal_comp'`, `norm_integral_le_of_norm_le_const'`, `mem_within_strip`, `support_MellinConvolution`, `support_MellinConvolution_subsets`	60
Total	63

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofReal_rpow` 📖	—	—	—	—	—

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`BigO_zero_atTop_of_support_in_Icc` 📖	—	—	—	—	—
`BigO_zero_atZero_of_support_in_Icc` 📖	—	—	—	—	—
`TendstoAtTop_of_support_in_Icc` 📖	—	—	—	—	—
`TendstoAtZero_of_support_in_Icc` 📖	—	—	—	—	—

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`support_abs` 📖	—	—	—	—	—
`support_deriv_subset_Icc` 📖	—	—	—	—	—
`support_mul_subset_of_subset` 📖	—	—	—	—	—
`support_ofReal` 📖	—	—	—	—	—
`support_of_along_fiber_subset_subset` 📖	—	—	—	—	—

IntervalIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_eq_integral_of_support_subset_Icc` 📖	—	—	—	—	—

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_comp_div_I0i_haar` 📖	—	—	—	—	`integral_comp_inv_I0i_haar` `integral_comp_mul_left_I0i_haar`
`integral_comp_inv_I0i_haar` 📖	—	—	—	—	—
`integral_comp_mul_left_I0i_haar` 📖	—	—	—	—	`integral_comp_mul_right_I0i_haar`
`integral_comp_mul_right_I0i_haar` 📖	—	—	—	—	—
`integral_comp_mul_right_I0i_haar_real` 📖	—	—	—	—	`integral_comp_mul_right_I0i_haar`
`integral_comp_rpow_I0i_haar_real` 📖	—	—	—	—	—
`setIntegral_integral_swap` 📖	—	—	—	—	—

SetIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_eq_integral_inter_of_support_subset` 📖	—	—	—	—	—
`integral_eq_integral_inter_of_support_subset_Icc` 📖	—	—	—	—	`integral_eq_integral_inter_of_support_subset`

(root)

Definitions

Name	Category	Theorems
`DeltaSpike` 📖	CompOp	9 math math: `MellinOfDeltaSpikeAt1`, `DeltaSpikeContinuous`, `DeltaSpikeSupport_aux`, `MellinOfDeltaSpike`, `DeltaSpikeMass`, `DeltaSpikeSupport`, `Smooth1_def_ite`, `DeltaSpikeNonNeg_of_NonNeg`, `DeltaSpikeOfRealContinuous`
`MellinConvolution` 📖	CompOp	6 math math: `MellinConvolutionTransform`, `MellinConvNonNeg_of_NonNeg`, `MellinConvolutionSymmetric`, `support_MellinConvolution`, `Smooth1_def_ite`, `support_MellinConvolution_subsets`
`Smooth1` 📖	CompOp	17 math math: `Smooth1Properties_above`, `Smooth1LeOne`, `SmoothedChebyshevPull3`, `Smooth1Properties_below`, `Smooth1MellinDifferentiable`, `MellinOfSmooth1a`, `Smooth1MellinConvergent`, `MellinOfSmooth1b`, `MellinOfSmooth1c`, `Smooth1ContinuousAt`, `SmoothedChebyshevDirichlet_aux_integrable`, `Smooth1Nonneg`, `SmoothedChebyshevDirichlet`, `Smooth1_def_ite`, `SmoothedChebyshevDirichlet_aux_tsum_integral`, `MellinOfSmooth1cExplicit`, `SmoothedChebyshevPull1`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`DeltaSpikeContinuous` 📖	mathematical	—	`DeltaSpike`	—	—
`DeltaSpikeMass` 📖	mathematical	—	`DeltaSpike`	—	—
`DeltaSpikeNonNeg_of_NonNeg` 📖	mathematical	—	`DeltaSpike`	—	—
`DeltaSpikeOfRealContinuous` 📖	mathematical	—	`DeltaSpike`	—	`DeltaSpikeContinuous`
`DeltaSpikeSupport` 📖	mathematical	—	`DeltaSpike`	—	`DeltaSpikeSupport'`
`DeltaSpikeSupport'` 📖	—	—	—	—	`DeltaSpikeSupport_aux`
`DeltaSpikeSupport_aux` 📖	mathematical	—	`DeltaSpike`	—	—
`MellinConvNonNeg_of_NonNeg` 📖	mathematical	—	`MellinConvolution`	—	—
`MellinConvolutionSymmetric` 📖	mathematical	—	`MellinConvolution`	—	`MeasureTheory.integral_comp_mul_right_I0i_haar` `MeasureTheory.integral_comp_inv_I0i_haar`
`MellinConvolutionTransform` 📖	mathematical	—	`MellinConvolution`	—	`MeasureTheory.setIntegral_integral_swap`
`MellinOf1` 📖	—	—	—	—	—
`MellinOfDeltaSpike` 📖	mathematical	—	`DeltaSpike`	—	—
`MellinOfDeltaSpikeAt1` 📖	mathematical	—	`DeltaSpike`	—	`MellinOfDeltaSpike`
`MellinOfDeltaSpikeAt1_asymp` 📖	—	—	—	—	`DifferentiableAt.comp_ofReal` `Filter.BigO_zero_atTop_of_support_in_Icc` `Function.support_ofReal` `Filter.BigO_zero_atZero_of_support_in_Icc`
`MellinOfPsi` 📖	—	—	—	—	`MellinOfPsi_aux` `SetIntegral.integral_eq_integral_inter_of_support_subset_Icc` `Function.support_abs` `Function.support_ofReal` `Function.support_deriv_subset_Icc` `intervalIntegral.norm_integral_le_of_norm_le_const'`
`MellinOfPsi_aux` 📖	—	—	—	—	`deriv.comp_ofReal` `PartialIntegration_of_support_in_Icc` `Differentiable.ofReal_comp_iff` `DifferentiableAt.comp_ofReal` `deriv.ofReal_comp'`
`MellinOfSmooth1a` 📖	mathematical	—	`Smooth1`	—	`DeltaSpikeOfRealContinuous` `DeltaSpikeSupport` `MellinConvolutionTransform` `MellinConvolutionSymmetric` `MellinOf1` `MellinOfDeltaSpike`
`MellinOfSmooth1b` 📖	mathematical	—	`Smooth1`	—	`MellinOfPsi` `MellinOfSmooth1a`
`MellinOfSmooth1c` 📖	mathematical	—	`Smooth1`	—	`MellinOfDeltaSpikeAt1_asymp` `MellinOfSmooth1a`
`PartialIntegration` 📖	—	—	—	—	—
`PartialIntegration_of_support_in_Icc` 📖	—	—	—	—	`Function.support_deriv_subset_Icc` `Function.support_mul_subset_of_subset` `Filter.TendstoAtZero_of_support_in_Icc` `Filter.TendstoAtTop_of_support_in_Icc` `PartialIntegration`
`Smooth1ContinuousAt` 📖	mathematical	—	`Smooth1`	—	`DeltaSpikeContinuous` `DeltaSpikeSupport'` `DeltaSpikeNonNeg_of_NonNeg` `MellinConvolutionSymmetric`
`Smooth1LeOne` 📖	mathematical	—	`Smooth1`	—	`Smooth1LeOne_aux`
`Smooth1LeOne_aux` 📖	—	—	—	—	`MeasureTheory.integral_comp_div_I0i_haar` `MeasureTheory.integral_comp_rpow_I0i_haar_real`
`Smooth1MellinConvergent` 📖	mathematical	—	`Smooth1`	—	`Smooth1ContinuousAt` `Smooth1Properties_above` `Smooth1Nonneg` `Smooth1LeOne`
`Smooth1MellinDifferentiable` 📖	mathematical	—	`Smooth1`	—	`Smooth1ContinuousAt` `Smooth1Properties_above` `Smooth1Nonneg` `Smooth1LeOne`
`Smooth1Nonneg` 📖	mathematical	—	`Smooth1`	—	`MellinConvNonNeg_of_NonNeg` `DeltaSpikeNonNeg_of_NonNeg`
`Smooth1Properties_above` 📖	mathematical	—	`Smooth1`	—	`Smooth1Properties_above_aux` `DeltaSpikeSupport` `Smooth1Properties_above_aux2`
`Smooth1Properties_above_aux` 📖	—	—	—	—	`Smooth1Properties_estimate`
`Smooth1Properties_above_aux2` 📖	—	—	—	—	—
`Smooth1Properties_below` 📖	mathematical	—	`Smooth1`	—	`Smooth1Properties_below_aux` `DeltaSpikeMass` `DeltaSpikeSupport` `MeasureTheory.integral_comp_div_I0i_haar`
`Smooth1Properties_below_aux` 📖	—	—	—	—	`Smooth1Properties_estimate`
`Smooth1Properties_estimate` 📖	—	—	—	—	—
`Smooth1_def_ite` 📖	mathematical	—	`Smooth1` `MellinConvolution` `DeltaSpike`	—	`MellinConvolutionSymmetric`
`mem_within_strip` 📖	—	—	—	—	—
`support_MellinConvolution` 📖	mathematical	—	`MellinConvolution`	—	`support_MellinConvolution_subsets`
`support_MellinConvolution_subsets` 📖	mathematical	—	`MellinConvolution`	—	—

deriv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_ofReal'` 📖	—	—	—	—	`comp_ofReal`
`ofReal_comp'` 📖	—	—	—	—	`ofReal_comp`

intervalIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_integral_le_of_norm_le_const'` 📖	—	—	—	—	—

---

← Back to Index