internlm/Lean-Github huggingface dataset:
Theorem: exists_mul_eq_setInterval
Proof state before:
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 ∂μ
Tactic:
. rw [← integral_norm_eq_lintegral_nnnorm hg_int.aestronglyMeasurable]
  rw [integral_congr_ae]
  apply Filter.Eventually.mp hg_nonneg
  simp
  apply Filter.eventually_of_forall
  intro x hx
  symm
  rw [abs_eq_self]
  exact hx
Proof state after:
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 ∂μ
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
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 ∂μ
Tactic:
rw [ENNReal.toReal] at hz'
Proof state after:
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.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ))
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑(ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ))
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
generalize hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
Proof state after:
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.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ))
z : NNReal
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
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
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑(ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ))
z : NNReal
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
rw [hz] at hz'
Proof state after:
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
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
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
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
cases eq_or_gt_of_le (zero_le z) with
| inl hz_zero =>
  simp [hz_zero] at hz'
  simp [hz']
  refine And.intro hs_ne ?_
  apply integral_eq_zero_of_ae
  rw [integral_eq_zero_iff_of_nonneg_ae hg_nonneg hg_int] at hz'
  apply Filter.Eventually.mp hz'
  simp
  apply Filter.eventually_of_forall
  intro x hx
  exact Or.inr hx
| inr hz_pos =>
  have hmM := existsBoundsOn_integral_mul_nonneg hs_meas hg_int hg_nonneg ?_ h_int
  swap
  . intro h_zero
    simp [h_zero] at hz'
    rw [eq_comm] at hz'
    rw [NNReal.coe_eq_zero] at hz'
    simp [hz'] at hz_pos
  rw [hz']
  rw [hz'] at hmM
  have hz_ne_zero : (z : ℝ) ≠ 0 := ne_of_gt hz_pos
  conv => arg 1; intro c; rhs; rw [← div_eq_iff hz_ne_zero]
  rcases hmM with ⟨m, hmM⟩
  rcases hmM with ⟨M, hmM⟩
  rcases hmM with ⟨⟨hm_mem, hM_mem⟩, ⟨hm, hM⟩⟩
  cases eq_or_gt_of_le hm with
  | inl hm => exists m
  | inr hm_lt =>
    cases eq_or_lt_of_le hM with
    | inl hM_eq => exists M
    | inr hM_lt =>
      simp_rw [eq_comm]
      rw [← Set.mem_image]
      refine @Set.mem_of_mem_of_subset _ _ (Set.Ioo (f m) (f M)) _ ?_ ?_
      . exact And.intro hm_lt hM_lt
      . 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 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‖₊ ∂μ)
Tactic:
rw [← integral_norm_eq_lintegral_nnnorm hg_int.aestronglyMeasurable]
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 ∂μ = ∫ (x : ℝ) in s, ‖g x‖ ∂μ
Theorem: exists_mul_eq_setInterval
Proof state before:
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 ∂μ = ∫ (x : ℝ) in s, ‖g x‖ ∂μ
Tactic:
rw [integral_congr_ae]
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
⊢ (fun x => g x) =ᵐ[Measure.restrict μ s] fun a => ‖g a‖
Theorem: exists_mul_eq_setInterval
Proof state before:
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
⊢ (fun x => g x) =ᵐ[Measure.restrict μ s] fun a => ‖g a‖
Tactic:
apply Filter.Eventually.mp hg_nonneg
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 : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun x => g x) x = (fun a => ‖g a‖) x
Theorem: exists_mul_eq_setInterval
Proof state before:
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 : ℝ) ∂Measure.restrict μ s, 0 x ≤ g x → (fun x => g x) x = (fun a => ‖g a‖) x
Tactic:
simp
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 : ℝ) ∂Measure.restrict μ s, 0 ≤ g x → g x = |g x|
Theorem: exists_mul_eq_setInterval
Proof state before:
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 : ℝ) ∂Measure.restrict μ s, 0 ≤ g x → g x = |g x|
Tactic:
apply Filter.eventually_of_forall
Proof state after:
case hz'.hp
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 : ℝ), 0 ≤ g x → g x = |g x|
Theorem: exists_mul_eq_setInterval
Proof state before:
case hz'.hp
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 : ℝ), 0 ≤ g x → g x = |g x|
Tactic:
intro x hx
Proof state after:
case hz'.hp
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 : ℝ
hx : 0 ≤ g x
⊢ g x = |g x|
Theorem: exists_mul_eq_setInterval
Proof state before:
case hz'.hp
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 : ℝ
hx : 0 ≤ g x
⊢ g x = |g x|
Tactic:
symm
Proof state after:
case hz'.hp
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 : ℝ
hx : 0 ≤ g x
⊢ |g x| = g x
Theorem: exists_mul_eq_setInterval
Proof state before:
case hz'.hp
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 : ℝ
hx : 0 ≤ g x
⊢ |g x| = g x
Tactic:
rw [abs_eq_self]
Proof state after:
case hz'.hp
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 : ℝ
hx : 0 ≤ g x
⊢ 0 ≤ g x
Theorem: exists_mul_eq_setInterval
Proof state before:
case hz'.hp
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 : ℝ
hx : 0 ≤ g x
⊢ 0 ≤ g x
Tactic:
exact hx
Proof state after:
no goals
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl
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_zero : z = 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
simp [hz_zero] at hz'
Proof state after:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
Tactic:
simp [hz']
Proof state after:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ (∃ x, x ∈ s) ∧ ∫ (x : ℝ) in s, f x * g x ∂μ = 0
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ (∃ x, x ∈ s) ∧ ∫ (x : ℝ) in s, f x * g x ∂μ = 0
Tactic:
refine And.intro hs_ne ?_
Proof state after:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ ∫ (x : ℝ) in s, f x * g x ∂μ = 0
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ ∫ (x : ℝ) in s, f x * g x ∂μ = 0
Tactic:
apply integral_eq_zero_of_ae
Proof state after:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ (fun a => f a * g a) =ᵐ[Measure.restrict μ s] 0
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : ∫ (x : ℝ) in s, g x ∂μ = 0
⊢ (fun a => f a * g a) =ᵐ[Measure.restrict μ s] 0
Tactic:
rw [integral_eq_zero_iff_of_nonneg_ae hg_nonneg hg_int] at hz'
Proof state after:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ (fun a => f a * g a) =ᵐ[Measure.restrict μ s] 0
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ (fun a => f a * g a) =ᵐ[Measure.restrict μ s] 0
Tactic:
apply Filter.Eventually.mp hz'
Proof state after:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, g x = 0 x → (fun a => f a * g a) x = 0 x
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, g x = 0 x → (fun a => f a * g a) x = 0 x
Tactic:
simp
Proof state after:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, g x = 0 → f x = 0 ∨ g x = 0
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl.hf
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict μ s, g x = 0 → f x = 0 ∨ g x = 0
Tactic:
apply Filter.eventually_of_forall
Proof state after:
case inl.hf.hp
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ (x : ℝ), g x = 0 → f x = 0 ∨ g x = 0
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl.hf.hp
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
⊢ ∀ (x : ℝ), g x = 0 → f x = 0 ∨ g x = 0
Tactic:
intro x hx
Proof state after:
case inl.hf.hp
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
x : ℝ
hx : g x = 0
⊢ f x = 0 ∨ g x = 0
Theorem: exists_mul_eq_setInterval
Proof state before:
case inl.hf.hp
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 : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_zero : z = 0
hz' : g =ᵐ[Measure.restrict μ s] 0
x : ℝ
hx : g x = 0
⊢ f x = 0 ∨ g x = 0
Tactic:
exact Or.inr hx
Proof state after:
no goals