Sinc

📁 Source: Mathlib/MeasureTheory/Function/SpecialFunctions/Sinc.lean

Statistics

Metric	Count
Definitions	0
Theorems sinc, sinc, sinc, sinc, integrable_sinc, measurable_sinc, stronglyMeasurable_sinc	7
Total	7

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sinc 📖	mathematical	AEMeasurable Real Real.measurableSpace	Real.sinc	—	Measurable.comp_aemeasurable Real.measurable_sinc

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sinc 📖	mathematical	Measurable Real Real.measurableSpace	Real.sinc	—	comp Real.measurable_sinc

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sinc 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.sinc	—	aestronglyMeasurable_iff_aemeasurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace instSecondCountableTopologyReal AEMeasurable.sinc

MeasureTheory.StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sinc 📖	mathematical	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.sinc	—	comp_measurable Real.stronglyMeasurable_sinc measurable PseudoEMetricSpace.pseudoMetrizableSpace Real.borelSpace

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable_sinc 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing measurableSpace sinc	—	MeasureTheory.Integrable.mono' MeasureTheory.integrable_const MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_sinc MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass norm_eq_abs abs_sinc_le_one
measurable_sinc 📖	mathematical	—	Measurable Real measurableSpace sinc	—	Continuous.measurable BorelSpace.opensMeasurable borelSpace continuous_sinc
stronglyMeasurable_sinc 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace measurableSpace sinc	—	Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable borelSpace measurable_sinc

---

← Back to Index