LogTrigonometric

📁 Source: Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean

Statistics

Metric	Count
Definitions	0
Theorems integral_log_sin_zero_pi, integral_log_sin_zero_pi_div_two	2
Total	2

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_log_sin_zero_pi 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Real.sin Real.instZero Real.pi MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat integral_log_sin_zero_pi_div_two Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz
integral_log_sin_zero_pi_div_two 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.log Real.sin Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instMul Real.instNeg	—	Nat.instAtLeastTwoHAddOfNat intervalIntegral.integral_congr_codiscreteWithin Filter.codiscreteWithin.mono AnalyticOnNhd.preimage_zero_mem_codiscrete PathConnectedSpace.connectedSpace Real.instPathConnectedSpace Real.analyticOnNhd_sin Real.sin_pi_div_two NeZero.one Real.instNontrivial Real.analyticOnNhd_cos Real.cos_zero Filter.mp_mem Filter.univ_mem' Real.sin_two_mul Real.log_mul NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add intervalIntegral.integral_sub IntervalIntegrable.sub zero_div IntervalIntegrable.comp_mul_left PseudoEMetricSpace.pseudoMetrizableSpace intervalIntegrable_log_sin enorm_ne_top intervalIntegrable_const Real.locallyFinite_volume intervalIntegrable_log_cos intervalIntegral.integral_const Real.instCompleteSpace sub_zero intervalIntegral.integral_comp_sub_left sub_self intervalIntegral.integral_comp_mul_left two_ne_zero CharZero.NeZero.two MulZeroClass.mul_zero Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero CancelDenoms.sub_subst CancelDenoms.mul_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true inv_mul_cancel_left₀ sub_sub_cancel_left neg_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNat.to_raw_eq CancelDenoms.neg_subst

---

← Back to Index