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 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

@[reducible, inline]

noncomputable abbrev ecsq (c y : ℝ) : ℝ

Equations

• ecsq c y = Real.exp (c * √(y + 1))

@[reducible, inline]

noncomputable abbrev ecsq' (c x : ℝ) : ℝ

Equations

• ecsq' c x = Real.exp (c * √(x + 1)) * (c * (1 / (2 * √(x + 1))))

@[reducible, inline]

abbrev oℝ (r : ℝ) : ENNReal

Equations

• oℝ = ENNReal.ofReal

theorem fundamental (c m : ℝ) (mp : -1 ≤ m) : ∫ (y : ℝ) in Set.Ioc (-1) m, ecsq' c y = ecsq c m - ecsq c (-1)

theorem integral_ecsq' (c m : ℝ) (mp : -1 ≤ m) (cpos : 0 < c) : oℝ (ecsq c m) = (∫⁻ (y : ℝ) in Set.Ioc (-1) m, oℝ (ecsq' c y)) + oℝ (ecsq c (-1))

theorem exp_indicator {X : Type u_1} (m : X × X → ℝ) (E : Set (X × X)) (mp : ∀ (x : X × X), m x < -1 → x ∉ E) (x : X × X) (c : ENNReal) (cpos : 0 < c) (cnt : c ≠ ⊤) : oℝ (ecsq c.toReal (m x)) * E.indicator 1 x = (∫⁻ (a : ℝ) in Set.Ioi (-1), oℝ (ecsq' c.toReal a) * (E ∩ {x : X × X | a ≤ m x}).indicator (fun (x : X × X) => 1) x) + E.indicator (fun (x : X × X) => 1) x

theorem integral_bound {V : Type} {X : Finset V} [MeasurableSpace { x : V // x ∈ X }] {ℙᵤ : MeasureTheory.Measure ({ x : V // x ∈ X } × { x : V // x ∈ X })} [dm : DiscreteMeasurableSpace ({ x : V // x ∈ X } × { x : V // x ∈ X })] {r : ℕ} {M : { x : V // x ∈ X } × { x : V // x ∈ X } → ℝ} {E : Set ({ x : V // x ∈ X } × { x : V // x ∈ X })} (mp : ∀ (x : { x : V // x ∈ X } × { x : V // x ∈ X }), M x < -1 → x ∉ E) (measInter : Measurable fun (a : ({ x : V // x ∈ X } × { x : V // x ∈ X }) × ℝ) => (E ∩ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | a.2 ≤ M x}).indicator (fun (x : { x : V // x ∈ X } × { x : V // x ∈ X }) => 1) a.1) {c C : ENNReal} (cpos : 0 < c) (cnt : c ≠ ⊤) (cleC : c.toReal ≤ C.toReal - 1) : have β := oℝ (3 ^ (-4 * ↑r)); ℙᵤ E < β → (∀ (y : ℝ), -1 ≤ y → ℙᵤ (E ∩ {x : { x : V // x ∈ X } × { x : V // x ∈ X } | y ≤ M x}) < oℝ (Real.exp (-C.toReal * √(y + 1))) * β * ↑r) → ∫⁻ (x : { x : V // x ∈ X } × { x : V // x ∈ X }) in E, oℝ (ecsq c.toReal (M x)) ∂ℙᵤ ≤ β * (↑r * c + 1)