internlm/Lean-Github huggingface dataset:
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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 ∂μ
Proof 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)
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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)
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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 ∂μ
Proof 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)
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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)
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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]
Proof 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)
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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 ?_ ?_ ?_
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof state after:
no goals
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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]
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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]
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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]
Proof state after:
no goals
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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]
Proof 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 ∂μ
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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]
Proof 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 ∂μ
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof 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