internlm/Lean-Github huggingface dataset:
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
Tactic:
simp_rw [eq_comm]
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ ∃ c ∈ s, f c = (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ ∃ c ∈ s, f c = (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
Tactic:
rw [← Set.mem_image]
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ (fun c => f c) '' s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ (fun c => f c) '' s
Tactic:
refine @Set.mem_of_mem_of_subset _ _ (Set.Ioo (f m) (f M)) _ ?_ ?_
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_1
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Ioo (f m) (f M)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_1
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Ioo (f m) (f M)

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s
Tactic:
. exact And.intro hm_lt hM_lt
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Set.Ioo (f m) (f M) ⊆ (fun c => f c) '' s
Tactic:
. refine @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _
    hs_conn (nhdsWithin m s) (nhdsWithin M s) ?_ ?_ ?_ ?_ _
    hf_cont _ _ ?_ ?_
  . rw [← mem_closure_iff_nhdsWithin_neBot]
    rw [IsClosed.closure_eq hs_closed]
    exact hm_mem
  . rw [← mem_closure_iff_nhdsWithin_neBot]
    rw [IsClosed.closure_eq hs_closed]
    exact hM_mem
  . simp; exact self_mem_nhdsWithin
  . simp; exact self_mem_nhdsWithin
  . exact hf_cont m hm_mem
  . exact hf_cont M hM_mem
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_1
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Ioo (f m) (f M)
Tactic:
exact And.intro hm_lt hM_lt
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_5
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin m s) (nhds (f m))

case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_6
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin M s) (nhds (f M))
Tactic:
. exact hf_cont m hm_mem
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_6
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin M s) (nhds (f M))
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_6
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.Tendsto f (nhdsWithin M s) (nhds (f M))
Tactic:
. exact hf_cont M hM_mem
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.NeBot (nhdsWithin m s)
Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot]
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ m ∈ closure s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ m ∈ closure s
Tactic:
rw [IsClosed.closure_eq hs_closed]
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ m ∈ s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_1
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ m ∈ s
Tactic:
exact hm_mem
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ Filter.NeBot (nhdsWithin M s)
Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot]
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ M ∈ closure s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ M ∈ closure s
Tactic:
rw [IsClosed.closure_eq hs_closed]
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ M ∈ s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_2
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ M ∈ s
Tactic:
exact hM_mem
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ nhdsWithin m s ≤ Filter.principal s
Tactic:
simp
Proof state after:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ s ∈ nhdsWithin m s
Theorem: exists_mul_eq_setInterval
Proof state before:
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ s ∈ nhdsWithin m s
Tactic:
exact self_mem_nhdsWithin
Proof state after:
no goals