Documentation Verification Report

JapaneseBracket

📁 Source: Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

Statistics

Metric	Count
Definitions	0
Theorems `closedBall_rpow_sub_one_eq_empty_aux`, `finite_integral_one_add_norm`, `finite_integral_rpow_sub_one_pow_aux`, `integrable_one_add_norm`, `integrable_rpow_neg_one_add_norm_sq`, `le_rpow_one_add_norm_iff_norm_le`, `one_add_norm_le_sqrt_two_mul_sqrt`, `rpow_neg_one_add_norm_sq_le`, `sqrt_one_add_norm_sq_le`	9
Total	9

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedBall_rpow_sub_one_eq_empty_aux` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne`	`Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instSub` `Real.instPow` `Real.instNeg` `Real.instInv` `Set` `Set.instEmptyCollection`	—	`Metric.closedBall_eq_empty` `sub_neg` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.rpow_lt_one_of_one_lt_of_neg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`finite_integral_one_add_norm` 📖	mathematical	`Real` `Real.instLT` `Real.instNatCast` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.lintegral` `ENNReal.ofReal` `Real.instPow` `Real.instAdd` `Real.instOne` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instNeg` `Top.top` `instTopENNReal`	—	`lt_of_le_of_lt` `Nat.cast_nonneg` `Real.instIsOrderedRing` `Measurable.pow_const` `Real.hasMeasurablePow` `Measurable.const_add` `ContinuousAdd.measurableAdd` `Real.borelSpace` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Measurable.norm` `BorelSpace.opensMeasurable` `measurable_id'` `le_of_lt` `Real.rpow_pos_of_pos` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `norm_nonneg` `MeasureTheory.lintegral_eq_lintegral_meas_le` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `Measurable.aemeasurable` `Set.ext` `le_rpow_one_add_norm_iff_norm_le` `Set.mem_Ioi` `MeasureTheory.setLIntegral_congr_fun` `measurableSet_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `MeasureTheory.lintegral_mono_set` `Set.Ioi_subset_Ioc_union_Ioi` `MeasureTheory.lintegral_union_le` `ENNReal.add_lt_top` `MeasureTheory.Measure.addHaar_closedBall` `sub_nonneg` `covariant_swap_add_of_covariant_add` `Real.one_le_rpow_of_pos_of_le_one_of_nonpos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.le` `measurableSet_Ioc` `MeasureTheory.lintegral_mul_const'` `LT.lt.ne` `MeasureTheory.measure_ball_lt_top` `FiniteDimensional.proper_real` `MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts` `ENNReal.mul_lt_top` `finite_integral_rpow_sub_one_pow_aux` `closedBall_rpow_sub_one_eq_empty_aux` `MeasureTheory.measure_empty` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul` `WithTop.top_pos`
`finite_integral_rpow_sub_one_pow_aux` 📖	mathematical	`Real` `Real.instLT` `Real.instNatCast`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.lintegral` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioc` `Real.instPreorder` `Real.instZero` `Real.instOne` `ENNReal.ofReal` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `Real.instPow` `Real.instNeg` `Real.instInv` `Top.top` `instTopENNReal`	—	`lt_of_le_of_lt` `Nat.cast_nonneg` `Real.instIsOrderedRing` `ENNReal.ofReal_le_ofReal` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.one_le_rpow_of_pos_of_le_one_of_nonpos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.le` `sub_le_sub_left` `Real.instZeroLEOneClass` `sub_zero` `Real.rpow_mul` `Real.rpow_natCast` `MeasureTheory.setLIntegral_mono'` `measurableSet_Ioc` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `MeasureTheory.IntegrableOn.setLIntegral_lt_top` `intervalIntegrable_iff_integrableOn_Ioc_of_le` `PseudoEMetricSpace.pseudoMetrizableSpace` `zero_le_one` `intervalIntegral.intervalIntegrable_rpow'` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `inv_mul_lt_iff₀'` `one_mul`
`integrable_one_add_norm` 📖	mathematical	`Real` `Real.instLT` `Real.instNatCast` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`MeasureTheory.Integrable` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instPow` `Real.instAdd` `Real.instOne` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instNeg`	—	`Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Measurable.pow_const` `Real.hasMeasurablePow` `Measurable.const_add` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Measurable.norm` `measurable_id'` `MeasureTheory.lintegral_enorm_of_nonneg` `Real.rpow_nonneg` `le_of_lt` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `norm_nonneg` `MeasureTheory.hasFiniteIntegral_iff_enorm` `finite_integral_one_add_norm`
`integrable_rpow_neg_one_add_norm_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instNatCast` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`MeasureTheory.Integrable` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instPow` `Real.instAdd` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`lt_of_le_of_lt` `Nat.cast_nonneg` `Real.instIsOrderedRing` `MeasureTheory.Integrable.mono'` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Integrable.const_mul` `integrable_one_add_norm` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `Measurable.pow_const` `Real.hasMeasurablePow` `Measurable.const_add` `ContinuousAdd.measurableAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Monoid.measurablePow` `ContinuousMul.measurableMul₂` `IsTopologicalSemiring.toContinuousMul` `Measurable.norm` `measurable_id'` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `Eq.trans_le` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.rpow_pos_of_pos` `add_pos_of_pos_of_nonneg` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `rpow_neg_one_add_norm_sq_le`
`le_rpow_one_add_norm_iff_norm_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Real.instPow` `Real.instAdd` `Real.instOne` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instNeg` `Real.instSub` `Real.instInv`	—	`le_sub_iff_add_le'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `neg_inv` `Real.le_rpow_inv_iff_of_neg` `add_pos_of_pos_of_nonneg` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `norm_nonneg` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`one_add_norm_le_sqrt_two_mul_sqrt` 📖	mathematical	—	`Real` `Real.instLE` `Real.instAdd` `Real.instOne` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instMul` `Real.sqrt` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.sqrt_mul` `zero_le_two` `Real.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Real.le_sqrt_of_sq_le` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt`
`rpow_neg_one_add_norm_sq_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Real.instPow` `Real.instAdd` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNeg` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.rpow_div_two_eq_sqrt` `le_of_lt` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.mul_rpow` `Real.sqrt_pos_of_pos` `mul_inv` `Real.rpow_neg` `mul_inv_cancel_left₀` `ne_of_gt` `Real.rpow_pos_of_pos` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `inv_anti₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `norm_nonneg` `Real.rpow_le_rpow` `one_add_norm_le_sqrt_two_mul_sqrt`
`sqrt_one_add_norm_sq_le` 📖	mathematical	—	`Real` `Real.instLE` `Real.sqrt` `Real.instAdd` `Real.instOne` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Real.sqrt_le_left` `le_of_lt` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `norm_nonneg` `Nat.instAtLeastTwoHAddOfNat` `add_sq` `one_pow` `mul_one` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`

---

← Back to Index