internlm/Lean-Github huggingface dataset:
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMapL
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((fderiv 𝕜 (fun y => compContinuousLinearMap m y) f) df) x = (((q f) df) m) x
Tactic:
rw [← fderiv_continuousMultilinear_apply_const_apply]
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ (fderiv 𝕜 (fun y => (compContinuousLinearMap m y) x) f) df = (((q f) df) m) x

case hc
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ DifferentiableAt 𝕜 (fun y => compContinuousLinearMap m y) f
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMapL
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ (fderiv 𝕜 (fun y => (compContinuousLinearMap m y) x) f) df = (((q f) df) m) x
Tactic:
rw [fderiv_continuousMultilinear_apply_const]
Proof state after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((ContinuousLinearMap.flipMultilinear (fderiv 𝕜 (fun y => compContinuousLinearMap m y) f)) x) df = (((q f) df) m) x

case hc
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ DifferentiableAt 𝕜 (fun y => compContinuousLinearMap m y) f
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMapL
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ ((ContinuousLinearMap.flipMultilinear (fderiv 𝕜 (fun y => compContinuousLinearMap m y) f)) x) df = (((q f) df) m) x
Tactic:
sorry
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMapL
Proof state before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
⊢ DifferentiableAt 𝕜 (fun f => compContinuousLinearMapL f) f
Tactic:
sorry
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMapL
Proof state before:
case hc
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : (i : ι) → E i →L[𝕜] E₁ i
q :
  ((i : ι) → E i →L[𝕜] E₁ i) →
    ((i : ι) → E i →L[𝕜] E₁ i) →L[𝕜] ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G
df : (i : ι) → E i →L[𝕜] E₁ i
m : ContinuousMultilinearMap 𝕜 (fun i => E₁ i) G
x : (i : ι) → E i
⊢ DifferentiableAt 𝕜 (fun y => compContinuousLinearMap m y) f
Tactic:
sorry
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ENNReal.toReal (↑↑q s) ∈ Set.Icc (f m) (f M)
Tactic:
rw [ENNReal.toReal]
Proof state after:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑(ENNReal.toNNReal (↑↑q s)) ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑(ENNReal.toNNReal (↑↑q s)) ∈ Set.Icc (f m) (f M)
Tactic:
generalize hz : ENNReal.toNNReal (q s) = z
Proof state after:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
rcases hq_fin with ⟨hq_fin⟩
Proof state after:
case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑(Measure.restrict q s) Set.univ < ⊤
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑(Measure.restrict q s) Set.univ < ⊤
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
simp at hq_fin
Proof state after:
case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have hz' : q s = z
Proof state after:
case hz'
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
⊢ ↑↑q s = ↑z

case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hz'
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
⊢ ↑↑q s = ↑z

case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
. rw [← hz]
  rw [ENNReal.coe_toNNReal hq_fin.ne]
Proof state after:
case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
cases eq_or_gt_of_le (zero_le z) with
| inl hz_zero =>
  exfalso
  rw [hz_zero] at hz
  rw [ENNReal.toNNReal_eq_zero_iff] at hz
  cases hz with
  | inl _ => contradiction
  | inr h => exact ne_of_lt hq_fin h
| inr hz_pos =>
  generalize hp : (z : ENNReal)⁻¹ • q = p
  have hp_one : IsProbabilityMeasure (p.restrict s)
  . constructor
    rw [← hp]
    simp
    rw [hz']
    rw [← ENNReal.div_eq_inv_mul]
    rw [ENNReal.div_eq_one_iff]
    . simp; exact hz_pos.ne'
    . simp
  have hp_eq : ∫ x in s, f x ∂p = (∫ x in s, f x ∂q) / (z : ℝ)
  . rw [← hp]
    simp
    simp [ENNReal.toReal_inv]
    rw [inv_mul_eq_div]
  have hp_int : Integrable f (p.restrict s)
  . rw [← hp]
    simp  apply Integrable.smul_measure h_int
    simp
    apply hz_pos.ne'
  have hp_meas_compl : p.restrict s sᶜ = 0
  . rw [Measure.restrict_apply (MeasurableSet.compl hs_meas)]
    simp
  have h_lb := @exists_not_mem_null_le_integral _ _ _ _ _ hp_one hp_int hp_meas_compl
  have h_ub := @exists_not_mem_null_integral_le _ _ _ _ _ hp_one hp_int hp_meas_compl
  simp at h_lb
  simp at h_ub
  rcases h_lb with ⟨m, ⟨hm_mem, hm⟩⟩
  rcases h_ub with ⟨M, ⟨hM_mem, hM⟩⟩
  exists m
  exists M
  apply And.intro ⟨hm_mem, hM_mem⟩
  simp
  apply And.intro
  . rw [hp_eq] at hm
    exact hm
  . rw [hp_eq] at hM
    exact hM
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hz'
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
⊢ ↑↑q s = ↑z
Tactic:
rw [← hz]
Proof state after:
case hz'
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
⊢ ↑↑q s = ↑(ENNReal.toNNReal (↑↑q s))
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hz'
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
⊢ ↑↑q s = ↑(ENNReal.toNNReal (↑↑q s))
Tactic:
rw [ENNReal.coe_toNNReal hq_fin.ne]
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
exfalso
Proof state after:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
Tactic:
rw [hz_zero] at hz
Proof state after:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = 0
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = 0
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
Tactic:
rw [ENNReal.toNNReal_eq_zero_iff] at hz
Proof state after:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ↑↑q s = 0 ∨ ↑↑q s = ⊤
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ↑↑q s = 0 ∨ ↑↑q s = ⊤
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
Tactic:
cases hz with
| inl _ => contradiction
| inr h => exact ne_of_lt hq_fin h
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inl.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
h✝ : ↑↑q s = 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inl.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
h : ↑↑q s = ⊤
⊢ False
Tactic:
exact ne_of_lt hq_fin h
Proof state after:
no goals
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
generalize hp : (z : ENNReal)⁻¹ • q = p
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have hp_one : IsProbabilityMeasure (p.restrict s)
Proof state after:
case hp_one
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
⊢ IsProbabilityMeasure (Measure.restrict p s)

case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case hp_one
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
⊢ IsProbabilityMeasure (Measure.restrict p s)

case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
. constructor
  rw [← hp]
  simp
  rw [hz']
  rw [← ENNReal.div_eq_inv_mul]
  rw [ENNReal.div_eq_one_iff]
  . simp; exact hz_pos.ne'
  . simp
Proof state after:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Theorem: existsBoundsOn_integral_measure
Proof state before:
case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
Tactic:
have hp_eq : ∫ x in s, f x ∂p = (∫ x in s, f x ∂q) / (z : ℝ)
Proof state after:
case hp_eq
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
⊢ ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z

case mk.inr
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_pos : 0 < z
p : Measure ℝ
hp : (↑z)⁻¹ • q = p
hp_one : IsProbabilityMeasure (Measure.restrict p s)
hp_eq : ∫ (x : ℝ) in s, f x ∂p = (∫ (x : ℝ) in s, f x ∂q) / ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)