Theorems · Theorem · measure theory
IntervalIntegrable.iff_comp_neg
∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {f : ℝ → E},
autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.iff_comp_neg._auto_1 →
(IntervalIntegrable f MeasureTheory.volume a b ↔
IntervalIntegrable (fun x => f (-x)) MeasureTheory.volume (-a) (-b))- Cited by
- 6 results in Mathlib
- Foundations
- Depth 251 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedAddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- ENNRealstatement · cited by 9,879
- Top.topstatement and proof · cited by 9,680
- one_mulproof · cited by 2,841
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- one_ne_zeroproof · cited by 885
- ENorm.enormstatement and proof · cited by 715
- neg_mulproof · cited by 654
- div_oneproof · cited by 629
- IntervalIntegrablestatement and proof · cited by 316
- neg_ne_zeroproof · cited by 70
Cited by6
Results whose statement or proof uses this declaration.
- intervalIntegral.intervalIntegrable_cpow'proof · cited by 7
- intervalIntegral.intervalIntegrable_rpow'proof · cited by 6
- IntervalIntegrable.comp_sub_leftproof · cited by 2
- Complex.betaIntegral_convergentproof · cited by 2
- intervalIntegrable_of_odd₀proof · cited by 1
- intervalIntegrable_of_even₀proof · cited by 1