case intro.intro.intro
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ (∫⁻ (a : α), f a ∂μ) + ε * ↑↑μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
⊢ (∫⁻ (a : α), f a ∂μ) + ε * ↑↑μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
rcases exists_measurable_le_lintegral_eq μ f with ⟨φ, hφm, hφ_le, hφ_eq⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
⊢ φ x + indicator {x | φ x + ε ≤ g x} (fun x => ε) x ≤ g x
case intro.intro.intro
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ (∫⁻ (a : α), f a ∂μ) + ε * ↑↑μ {x | f x + ε ≤ g x} ≤ ∫⁻ (a : α), g a ∂μ
calc
  (∫⁻ x, f x ∂μ) + ε * μ { x | f x + ε ≤ g x } = (∫⁻ x, φ x ∂μ) + ε * μ { x | f x + ε ≤ g x } :=
    by rw [hφ_eq]
  _ ≤ (∫⁻ x, φ x ∂μ) + ε * μ { x | φ x + ε ≤ g x } := by
    gcongr
    exact measure_mono fun x => (add_le_add_right (hφ_le _) _).trans
  _ = ∫⁻ x, φ x + indicator { x | φ x + ε ≤ g x } (fun _ => ε) x ∂μ := by
    rw [lintegral_add_left hφm, lintegral_indicator₀, set_lintegral_const]
    exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable
  _ ≤ ∫⁻ x, g x ∂μ := lintegral_mono_ae (hle.mono fun x hx₁ => ?_)
case intro.intro.intro
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
⊢ (φ x + if x ∈ {x | φ x + ε ≤ g x} then ε else 0) ≤ g x
case intro.intro.intro
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
⊢ φ x + indicator {x | φ x + ε ≤ g x} (fun x => ε) x ≤ g x
simp only [indicator_apply]
case intro.intro.intro.inl
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : x ∈ {x | φ x + ε ≤ g x}
⊢ φ x + ε ≤ g x

case intro.intro.intro.inr
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : ¬x ∈ {x | φ x + ε ≤ g x}
⊢ φ x + 0 ≤ g x
case intro.intro.intro
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
⊢ (φ x + if x ∈ {x | φ x + ε ≤ g x} then ε else 0) ≤ g x
split_ifs with hx₂
no goals
case intro.intro.intro.inl
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : x ∈ {x | φ x + ε ≤ g x}
⊢ φ x + ε ≤ g x

case intro.intro.intro.inr
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
hx₂ : ¬x ∈ {x | φ x + ε ≤ g x}
⊢ φ x + 0 ≤ g x
exacts [hx₂, (add_zero _).trans_le <| (hφ_le x).trans hx₁]
no goals
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ (∫⁻ (x : α), f x ∂μ) + ε * ↑↑μ {x | f x + ε ≤ g x} = (∫⁻ (x : α), φ x ∂μ) + ε * ↑↑μ {x | f x + ε ≤ g x}
rw [hφ_eq]
case bc.bc
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ ↑↑μ {x | f x + ε ≤ g x} ≤ ↑↑μ {x | φ x + ε ≤ g x}
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ (∫⁻ (x : α), φ x ∂μ) + ε * ↑↑μ {x | f x + ε ≤ g x} ≤ (∫⁻ (x : α), φ x ∂μ) + ε * ↑↑μ {x | φ x + ε ≤ g x}
gcongr
no goals
case bc.bc
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ ↑↑μ {x | f x + ε ≤ g x} ≤ ↑↑μ {x | φ x + ε ≤ g x}
exact measure_mono fun x => (add_le_add_right (hφ_le _) _).trans
case hs
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ NullMeasurableSet {x | φ x + ε ≤ g x}
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ (∫⁻ (x : α), φ x ∂μ) + ε * ↑↑μ {x | φ x + ε ≤ g x} = ∫⁻ (x : α), φ x + indicator {x | φ x + ε ≤ g x} (fun x => ε) x ∂μ
rw [lintegral_add_left hφm, lintegral_indicator₀, set_lintegral_const]
no goals
case hs
α : Type u_1
β : Type ?u.953853
γ : Type ?u.953856
δ : Type ?u.953859
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᵐ[μ] g
hg : AEMeasurable g
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : (∫⁻ (a : α), f a ∂μ) = ∫⁻ (a : α), φ a ∂μ
⊢ NullMeasurableSet {x | φ x + ε ≤ g x}
exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable