internlm/Lean-Github huggingface dataset:
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
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun a => ‖g a‖) x = (fun a => g a) x
Tactic:
simp
Proof state after:
no goals
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 ∂μ
Tactic:
rw [← hq]
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 ∂Measure.withDensity μ fun x => ↑‖g x‖₊) = ∫ (x : ℝ) in s, f x * g x ∂μ
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 ∂Measure.withDensity μ fun x => ↑‖g x‖₊) = ∫ (x : ℝ) in s, f x * g x ∂μ
Tactic:
rw [set_integral_withDensity_eq_set_integral_smul₀ _ _ hs_meas]
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 ∂μ
⊢ ∫ (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‖₊
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 ∂μ
⊢ ∫ (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
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 ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
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 ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
. apply AEMeasurable.nnnorm
  exact hg_int.aemeasurable
Proof state after:
no goals
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 ∂μ
⊢ ∫ (a : ℝ) in s, ‖g a‖₊ • f a ∂μ = ∫ (x : ℝ) in s, f x * g x ∂μ
Tactic:
exact integral_congr_ae h_ae_eq.symm
Proof state after:
no goals
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 ∂μ
⊢ AEMeasurable fun x => ‖g x‖₊
Tactic:
apply AEMeasurable.nnnorm
Proof 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
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof state after:
no goals
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)
Tactic:
constructor
Proof 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 < ⊤
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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]
Proof 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‖₊ ∂μ < ⊤
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof state after:
no goals
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
Tactic:
intro h
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 ∂μ
h : ↑↑q s = 0
⊢ False
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 ∂μ
h : ↑↑q s = 0
⊢ False
Tactic:
revert hq_g
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_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
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_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]
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_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ ¬0 = ∫ (x : ℝ) in s, g x ∂μ
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_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]
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_fg : ∫ (x : ℝ) in s, f x ∂q = ∫ (x : ℝ) in s, f x * g x ∂μ
h : ↑↑q s = 0
⊢ ¬∫ (x : ℝ) in s, g x ∂μ = 0
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_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
Proof state after:
no goals
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:
rw [IntegrableOn]
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 ∂μ
⊢ Integrable fun x => f x
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 ∂μ
⊢ Integrable fun x => f x
Tactic:
rw [integrable_withDensity_iff_integrable_smul₀]
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 ∂μ
⊢ 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‖₊
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 ∂μ
⊢ 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
Proof 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‖₊
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof state after:
no goals
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 ∂μ
⊢ Integrable fun x => ‖g x‖₊ • f x
Tactic:
exact IntegrableOn.congr_fun_ae h_int h_ae_eq
Proof state after:
no goals
Theorem: existsBoundsOn_integral_mul_nonneg
Proof 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
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
have hz' : ∫ x in s, g x ∂μ = ENNReal.toReal (∫⁻ x in s, ↑‖g x‖₊ ∂μ)
Proof state after:
case hz'
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
⊢ ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)

f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
hz' : ∫ (x : ℝ) in s, g x ∂μ = ENNReal.toReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ