theorem ae_le_of_forallOn_le {α : Type u_1} {g f : α → ℝ} {s : Set α} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (ms : MeasurableSet s) (h₁ : ∀ x ∈ s, g x ≤ f x) : g ≤ᵐ[μ.restrict s] f

theorem indicator_one_mul {X : Type u_1} {Y : Type u_2} {x : X} [MulZeroOneClass Y] (f : X → Y) [MeasurableSpace X] (E : Set X) : f x * E.indicator 1 x = E.indicator f x

theorem IntegrableFin {X : Type} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] {ℙᵤ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure ℙᵤ] {f : X → ℝ} : MeasureTheory.Integrable f ℙᵤ

theorem bounded_thingy_on_s {s : Set ℝ} {f g h : ℝ → ℝ} (ms : MeasurableSet s) (Ih : MeasureTheory.IntegrableOn h s MeasureTheory.volume) (Ig : MeasureTheory.IntegrableOn g s MeasureTheory.volume) (dh : ∀ x ∈ s, h x ≤ f x) (dg : ∀ x ∈ s, f x ≤ g x) (mf : Measurable f) : MeasureTheory.IntegrableOn f s MeasureTheory.volume

theorem integrableOn_one_div_two_mul_sqrt_plus (m c : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => 1 / (2 * √(x + c))) (Set.Icc (-c) m) MeasureTheory.volume

theorem continuousOn_add_const {c : ℝ} {s : Set ℝ} : ContinuousOn (fun (x : ℝ) => x + c) s

theorem intOn1 {m : ℝ} : MeasureTheory.IntegrableOn (fun (x : ℝ) => 1 / (2 * √(x + 1))) (Set.Ioc (-1) m) MeasureTheory.volume

theorem improper_integral_shift (c : ℝ) (f : ℝ → ℝ) (cf : ContinuousOn f (Set.Ioi 0)) (If : MeasureTheory.IntegrableOn f (Set.Ici 0) MeasureTheory.volume) (Iif : MeasureTheory.IntegrableOn (fun (x : ℝ) => f (x + c)) (Set.Ici (-c)) MeasureTheory.volume) : ∫ (x : ℝ) in Set.Ioi (-c), f (x + c) = ∫ (x : ℝ) in Set.Ioi 0, f x

theorem integrableOn_pow {m a c : ℝ} (mp : 0 < m) (ha : a < -1) (cp : 0 ≤ c) : MeasureTheory.IntegrableOn (fun (x : ℝ) => (x + c) ^ a) (Set.Ioi m) MeasureTheory.volume

theorem measEsqc {d c : ℝ} : Measurable fun (x : ℝ) => Real.exp (d * √(x + 1)) * (c * (1 / (2 * √(x + 1))))

theorem integrableOn_exp_neg_sqrt_plus {c : ℝ} (cn : 0 ≤ c) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-√(x + c)) * (1 / (2 * √(x + c)))) (Set.Ioi (-c)) MeasureTheory.volume

theorem intEsqc (c : ℝ) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-√(x + 1)) * (c * (1 / (2 * √(x + 1))))) (Set.Ioi (-1)) MeasureTheory.volume

theorem integrableOn_exp_neg_sqrt : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-√x) * (1 / (2 * √x))) (Set.Ioi 0) MeasureTheory.volume

theorem integral_exp_neg_sqrt : ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-√x) * (1 / (2 * √x)) = 1

theorem terriblel (c : ℝ) : ∫ (a : ℝ) in Set.Ioi (-1), Real.exp (-√(a + 1)) * (c * (1 / (2 * √(a + 1)))) = c

theorem terrible (c : ENNReal) (cnt : c ≠ ⊤) : ∫⁻ (a : ℝ) in Set.Ioi (-1), ENNReal.ofReal (Real.exp (-√(a + 1)) * (c.toReal * (1 / (2 * √(a + 1))))) = c

theorem lintegral_Ioc_eq_Ioi {X : Type u_1} (l : ℝ) (f : ℝ → ENNReal) (x : X) (b : X → ℝ) : ∫⁻ (a : ℝ) in Set.Ioc l (b x), f a = ∫⁻ (a : ℝ) in Set.Ioi l, f a * {y : X | a ≤ b y}.indicator 1 x