Theorem: existsBoundsOn_integral_mul_nonneg (ForML/IntegralMeanValue.lean)

State before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
have h_ae_eq : (fun x => f x * g x) =ᵐ[μ.restrict s] (fun x => ‖g x‖₊ • f x)
State after:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)

State before:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
. simp [NNReal.smul_def]
  apply Filter.Eventually.mp hg_nonneg
  simp
  apply Filter.eventually_of_forall
  intro x hx
  rw [mul_comm]
  rw [abs_eq_self.mpr hx]
State after:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)

State before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
generalize hq : μ.withDensity (fun x => ‖g x‖₊) = q
State after:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)

State before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
have hq_g : ENNReal.toReal (q s) = ∫ (x : ℝ) in s, g x ∂μ
State after:
case hq_g
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)

State before:
case hq_g
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
. simp [← hq, hs_meas]
  rw [← integral_norm_eq_lintegral_nnnorm hg_int.aestronglyMeasurable]
  apply integral_congr_ae
  apply Filter.Eventually.mp hg_nonneg
  simp
State after:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)

State before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
have hq_fg : ∫ x in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
State after:
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)

State before:
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
. rw [← hq]
  rw [set_integral_withDensity_eq_set_integral_smul₀ _ _ hs_meas]
  . exact integral_congr_ae h_ae_eq.symm
  . apply AEMeasurable.nnnorm
    exact hg_int.aemeasurable
State after:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)

State before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ∫ (x : ℝ) in s, g x ∂μ ∈ Set.Icc (f m) (f M)
Tactic:
rw [← hq_g, ← hq_fg]
State after:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ENNReal.toReal (↑↑q s) ∈ Set.Icc (f m) (f M)

State before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ENNReal.toReal (↑↑q s) ∈ Set.Icc (f m) (f M)
Tactic:
refine existsBoundsOn_integral_measure hs_meas ?_ ?_ ?_
State after:
case refine_1
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IsFiniteMeasure (Measure.restrict q s)

case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ↑↑q s ≠ 0

case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IntegrableOn (fun x => f x) s

State before:
case refine_1
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IsFiniteMeasure (Measure.restrict q s)

case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ↑↑q s ≠ 0

case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IntegrableOn (fun x => f x) s
Tactic:
. constructor
  simp [← hq, hs_meas]
  exact hg_int.right
State after:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ↑↑q s ≠ 0

case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IntegrableOn (fun x => f x) s

State before:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ↑↑q s ≠ 0

case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IntegrableOn (fun x => f x) s
Tactic:
. intro h
  revert hq_g
  simp [h]
  rw [eq_comm]
  exact hg_nonzero
State after:
case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IntegrableOn (fun x => f x) s

State before:
case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IntegrableOn (fun x => f x) s
Tactic:
. simp [← hq]
  rw [IntegrableOn]
  rw [restrict_withDensity hs_meas]
  rw [integrable_withDensity_iff_integrable_smul₀]
  . exact IntegrableOn.congr_fun_ae h_int h_ae_eq
  . exact AEMeasurable.nnnorm hg_int.aemeasurable
State after:
no goals

State before:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
Tactic:
simp [NNReal.smul_def]
State after:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => |g x| * f x

State before:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => |g x| * f x
Tactic:
apply Filter.Eventually.mp hg_nonneg
State after:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun x => f x * g x) x = (fun x => |g x| * f x) x

State before:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun x => f x * g x) x = (fun x => |g x| * f x) x
Tactic:
simp
State after:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 ≤ g x → f x * g x = |g x| * f x

State before:
case h_ae_eq
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 ≤ g x → f x * g x = |g x| * f x
Tactic:
apply Filter.eventually_of_forall
State after:
case h_ae_eq.hp
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∀ (x : ℝ), 0 ≤ g x → f x * g x = |g x| * f x

State before:
case h_ae_eq.hp
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∀ (x : ℝ), 0 ≤ g x → f x * g x = |g x| * f x
Tactic:
intro x hx
State after:
case h_ae_eq.hp
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
x : ℝ
hx : 0 ≤ g x
⊢ f x * g x = |g x| * f x

State before:
case h_ae_eq.hp
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
x : ℝ
hx : 0 ≤ g x
⊢ f x * g x = |g x| * f x
Tactic:
rw [mul_comm]
State after:
case h_ae_eq.hp
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
x : ℝ
hx : 0 ≤ g x
⊢ g x * f x = |g x| * f x

State before:
case h_ae_eq.hp
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
x : ℝ
hx : 0 ≤ g x
⊢ g x * f x = |g x| * f x
Tactic:
rw [abs_eq_self.mpr hx]
State after:
no goals

State before:
case hq_g
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
Tactic:
simp [← hq, hs_meas]
State after:
case hq_g
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = ∫ (x : ℝ) in s, g x ∂μ

State before:
case hq_g
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = ∫ (x : ℝ) in s, g x ∂μ
Tactic:
rw [← integral_norm_eq_lintegral_nnnorm hg_int.aestronglyMeasurable]
State after:
case hq_g
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ∫ (x : ℝ) in s, ‖g x‖ ∂μ = ∫ (x : ℝ) in s, g x ∂μ

State before:
case hq_g
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ∫ (x : ℝ) in s, ‖g x‖ ∂μ = ∫ (x : ℝ) in s, g x ∂μ
Tactic:
apply integral_congr_ae
State after:
case hq_g.h
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ (fun a => ‖g a‖) =ᵐ[Measure.restrict μ s] fun a => g a

State before:
case hq_g.h
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ (fun a => ‖g a‖) =ᵐ[Measure.restrict μ s] fun a => g a
Tactic:
apply Filter.Eventually.mp hg_nonneg
State after:
case hq_g.h
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun a => ‖g a‖) x = (fun a => g a) x

State before:
case hq_g.h
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun a => ‖g a‖) x = (fun a => g a) x
Tactic:
simp
State after:
no goals

State before:
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
Tactic:
rw [← hq]
State after:
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ (∫ (x : ℝ) in s, f x ∂Measure.withDensity μ fun x => ↑‖g x‖₊) = ∫ (x : ℝ) in s, f x * g x ∂μ

State before:
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ (∫ (x : ℝ) in s, f x ∂Measure.withDensity μ fun x => ↑‖g x‖₊) = ∫ (x : ℝ) in s, f x * g x ∂μ
Tactic:
rw [set_integral_withDensity_eq_set_integral_smul₀ _ _ hs_meas]
State after:
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (a : ℝ) in s, ‖g a‖₊ • f a ∂μ = ∫ (x : ℝ) in s, f x * g x ∂μ

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊

State before:
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (a : ℝ) in s, ‖g a‖₊ • f a ∂μ = ∫ (x : ℝ) in s, f x * g x ∂μ

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
. exact integral_congr_ae h_ae_eq.symm
State after:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊

State before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
. apply AEMeasurable.nnnorm
  exact hg_int.aemeasurable
State after:
no goals

State before:
case hq_fg
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ ∫ (a : ℝ) in s, ‖g a‖₊ • f a ∂μ = ∫ (x : ℝ) in s, f x * g x ∂μ
Tactic:
exact integral_congr_ae h_ae_eq.symm
State after:
no goals

State before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
apply AEMeasurable.nnnorm
State after:
case hf
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ AEMeasurable fun a => g a

State before:
case hf
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
⊢ AEMeasurable fun a => g a
Tactic:
exact hg_int.aemeasurable
State after:
no goals

State before:
case refine_1
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IsFiniteMeasure (Measure.restrict q s)
Tactic:
constructor
State after:
case refine_1.measure_univ_lt_top
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ↑↑(Measure.restrict q s) Set.univ < ⊤

State before:
case refine_1.measure_univ_lt_top
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ↑↑(Measure.restrict q s) Set.univ < ⊤
Tactic:
simp [← hq, hs_meas]
State after:
case refine_1.measure_univ_lt_top
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ < ⊤

State before:
case refine_1.measure_univ_lt_top
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ < ⊤
Tactic:
exact hg_int.right
State after:
no goals

State before:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ ↑↑q s ≠ 0
Tactic:
intro h
State after:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ False

State before:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ False
Tactic:
revert hq_g
State after:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ → False

State before:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ → False
Tactic:
simp [h]
State after:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ ¬0 = ∫ (x : ℝ) in s, g x ∂μ

State before:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ ¬0 = ∫ (x : ℝ) in s, g x ∂μ
Tactic:
rw [eq_comm]
State after:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ ¬∫ (x : ℝ) in s, g x ∂μ = 0

State before:
case refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ ¬∫ (x : ℝ) in s, g x ∂μ = 0
Tactic:
exact hg_nonzero
State after:
no goals

State before:
case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ IntegrableOn (fun x => f x) s
Tactic:
rw [IntegrableOn]
State after:
case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ Integrable fun x => f x

State before:
case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ Integrable fun x => f x
Tactic:
rw [integrable_withDensity_iff_integrable_smul₀]
State after:
case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ Integrable fun x => ‖g x‖₊ • f x

case refine_3.hf
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊

State before:
case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ Integrable fun x => ‖g x‖₊ • f x

case refine_3.hf
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
. exact IntegrableOn.congr_fun_ae h_int h_ae_eq
State after:
case refine_3.hf
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊

State before:
case refine_3.hf
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
. exact AEMeasurable.nnnorm hg_int.aemeasurable
State after:
no goals

State before:
case refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ Integrable fun x => ‖g x‖₊ • f x
Tactic:
exact IntegrableOn.congr_fun_ae h_int h_ae_eq
State after:
no goals

State before:
case refine_3.hf
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_meas : MeasurableSet s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
hg_nonzero : ∫ (x : ℝ) in s, g x ∂μ ≠ 0
h_int : IntegrableOn (fun x => f x * g x) s
h_ae_eq : (fun x => f x * g x) =ᵐ[Measure.restrict μ s] fun x => ‖g x‖₊ • f x
q : Measure ℝ
hq : (Measure.withDensity μ fun x => ↑‖g x‖₊) = q
hq_g : ENNReal.toReal (↑↑q s) = ∫ (x : ℝ) in s, g x ∂μ
hq_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
exact AEMeasurable.nnnorm hg_int.aemeasurable
State after:
no goals