Theorem: integrable_bump_sub_const_mul_diracSeq (ForML/Dirac.lean)

State before:
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Integrable fun x => (φ x - y) * DiracSeq b x
Tactic:
refine Integrable.bdd_mul ?_ ?_ ?_
State after:
case refine_1
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Integrable fun x => DiracSeq b x

case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume

case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C

State before:
case refine_1
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Integrable fun x => DiracSeq b x

case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume

case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Tactic:
. exact DiracSeq.integrable hb
State after:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume

case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C

State before:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume

case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Tactic:
. refine Continuous.aestronglyMeasurable ?_
  exact Continuous.sub hφ.continuous continuous_const
State after:
case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C

State before:
case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Tactic:
. exact bounded_bump_sub_const hφ y
State after:
no goals

State before:
case refine_1
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Integrable fun x => DiracSeq b x
Tactic:
exact DiracSeq.integrable hb
State after:
no goals

State before:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ AEStronglyMeasurable (fun x => φ x - y) volume
Tactic:
refine Continuous.aestronglyMeasurable ?_
State after:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Continuous fun x => φ x - y

State before:
case refine_2
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ Continuous fun x => φ x - y
Tactic:
exact Continuous.sub hφ.continuous continuous_const
State after:
no goals

State before:
case refine_3
φ : ℝ → ℝ
hφ : IsBump φ
y b : ℝ
hb : 0 < b
⊢ ∃ C, ∀ (x : ℝ), ‖φ x - y‖ ≤ C
Tactic:
exact bounded_bump_sub_const hφ y
State after:
no goals