awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
hab : dist a ((algebraMap 𝕜 A : (a : 𝕜) → A) x) ≤ ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
hab₁ : dist ((algebraMap 𝕜 A : (a : 𝕜) → A) x) a ≤ ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
have hab₂ : ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ ≤
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
Tactic: grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x) (by simp [hx]), dist_comm,
            dist_eq_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖a - w‖ ≤ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
have hcd : ‖a - w‖ < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
Tactic: apply le_of_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖ ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
have grw : ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a + (a - w)‖ ≤
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
Tactic: grw [norm_sub_le_norm_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
have calc : infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
    infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
Tactic: calc infDist a (algebraMap 𝕜 A '' μ.support) / 2
      _ ≤ infDist a (algebraMap 𝕜 A '' μ.support)
        - infDist a (algebraMap 𝕜 A '' μ.support) / 2 := by grind
      _ ≤ ‖(algebraMap 𝕜 A) x - a‖ - ‖a - w‖ := by
        gcongr
        · grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x) (by simp [hx]), dist_comm,
            dist_eq_norm]
        · apply le_of_lt
          simpa [s, ← dist_eq_norm, dist_comm w a] using hw
      _ ≤ ‖(algebraMap 𝕜 A) x - w‖ := by grw [norm_sub_le_norm_add]; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
calc :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
      infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
have calc₁ : infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
    infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖
Tactic: calc infDist a (algebraMap 𝕜 A '' μ.support) / 2
      _ ≤ infDist a (algebraMap 𝕜 A '' μ.support)
        - infDist a (algebraMap 𝕜 A '' μ.support) / 2 := by grind
      _ ≤ ‖(algebraMap 𝕜 A) x - a‖ - ‖a - w‖ := by
        gcongr
        · grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x) (by simp [hx]), dist_comm,
            dist_eq_norm]
        · apply le_of_lt
          simpa [s, ← dist_eq_norm, dist_comm w a] using hw
      _ ≤ ‖(algebraMap 𝕜 A) x - w‖ := by grw [norm_sub_le_norm_add]; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
calc :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
      infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
calc₁ :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) -
      infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖
⊢ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
have calc₂ : ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖ ≤
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
Tactic: calc infDist a (algebraMap 𝕜 A '' μ.support) / 2
      _ ≤ infDist a (algebraMap 𝕜 A '' μ.support)
        - infDist a (algebraMap 𝕜 A '' μ.support) / 2 := by grind
      _ ≤ ‖(algebraMap 𝕜 A) x - a‖ - ‖a - w‖ := by
        gcongr
        · grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x) (by simp [hx]), dist_comm,
            dist_eq_norm]
        · apply le_of_lt
          simpa [s, ← dist_eq_norm, dist_comm w a] using hw
      _ ≤ ‖(algebraMap 𝕜 A) x - w‖ := by grw [norm_sub_le_norm_add]; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
⊢ HasDerivAt (F := A) (fun (a : A) ↦ ∫ (x : 𝕜), resolvent a x ∂μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
have resolvent'_bound : ∀ᵐ (x : 𝕜) ∂μ,
  ∀ w ∈ s,
    ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
      HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
Tactic: have resolvent'_bound : ∀ᵐ x ∂μ, ∀ w ∈ s,
      ‖(resolvent w x) ^ 2‖ ≤ ((infDist a (algebraMap 𝕜 A '' μ.support)) / 2)⁻¹ ^ 2 := by
    filter_upwards [support_mem_ae] with x hx w hw
    grw [resolvent, Ring.inverse_eq_inv, norm_pow, norm_inv]
    gcongr
    calc infDist a (algebraMap 𝕜 A '' μ.support) / 2
      _ ≤ infDist a (algebraMap 𝕜 A '' μ.support)
        - infDist a (algebraMap 𝕜 A '' μ.support) / 2 := by grind
      _ ≤ ‖(algebraMap 𝕜 A) x - a‖ - ‖a - w‖ := by
        gcongr
        · grw [infDist_le_dist_of_mem (y := (algebraMap 𝕜 A) x) (by simp [hx]), dist_comm,
            dist_eq_norm]
        · apply le_of_lt
          simpa [s, ← dist_eq_norm, dist_comm w a] using hw
      _ ≤ ‖(algebraMap 𝕜 A) x - w‖ := by grw [norm_sub_le_norm_add]; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
⊢ ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
have h₁ : ∀ (x : 𝕜) (hx : x ∈ μ.support) (w : A) (hw : w ∈ s),
  HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
Tactic: filter_upwards [support_mem_ae] with x hx w hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
have h₁ : x ∈ resolventSet 𝕜 w
Tactic: apply hasDerivAt_resolvent_const_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ x ∈ resolventSet 𝕜 w
have hw₁ : Membership.mem (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ w
Tactic: replace hw := hs_μ hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
x : 𝕜
hx : x ∈ μ.support
w : A
hw : Membership.mem (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ w
⊢ x ∈ resolventSet 𝕜 w
have h₁ : ∀ (hw : ¬x ∈ resolventSet 𝕜 w), w ∉ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
Tactic: contrapose! hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
x : 𝕜
hx : x ∈ μ.support
w : A
hw : ¬x ∈ resolventSet 𝕜 w
⊢ w ∉ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
have h₁ : Membership.mem (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) w
Tactic: rw [Set.notMem_compl_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
x : 𝕜
hx : x ∈ μ.support
w : A
hw : ¬x ∈ resolventSet 𝕜 w
⊢ Membership.mem (γ := Set A) ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) w
have right : (algebraMap 𝕜 A : (a : 𝕜) → A) x = w
Tactic: use x, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
⊢ HasDerivAt (F := A) (fun (a : A) ↦ ∫ (x : 𝕜), resolvent a x ∂μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
have h_deriv : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
Tactic: have h_deriv : ∀ᵐ x ∂μ, ∀ w ∈ s, HasDerivAt (fun w ↦ resolvent w x) (resolvent w x ^ 2) w := by
    filter_upwards [support_mem_ae] with x hx w hw
    apply hasDerivAt_resolvent_const_right
    replace hw := hs_μ hw
    contrapose! hw
    rw [Set.notMem_compl_iff]
    use x, hx
    simpa [resolventSet, sub_eq_zero] using hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : RCLike A
inst_6 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst_7 : IsFiniteMeasure μ
a : A
ha : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
s : Set A := ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
resolvent'_bound :
  ∀ᵐ (x : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
h_deriv : ∀ᵐ (x : 𝕜) ∂μ, ∀ w ∈ s, HasDerivAt (fun (w : A) ↦ resolvent w x) (HPow.hPow (β := ℕ) (resolvent w x) 2) w
⊢ Integrable (ε := ℝ)
    (fun (a_1 : 𝕜) ↦ HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2) μ
have funProp : ‖HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2‖ₑ ≠ ⊤
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
⊢ AnalyticOn ℂ (E := ℂ) (resolventTransform μ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ
have rw : DifferentiableOn ℂ (E := ℂ) (resolventTransform μ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ
Tactic: rw [analyticOn_iff_differentiableOn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
rw : DifferentiableOn ℂ (E := ℂ) (resolventTransform μ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ
⊢ AnalyticOn ℂ (E := ℂ) (resolventTransform μ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ
have rw₁ : IsOpen (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ
Tactic: rw [analyticOn_iff_differentiableOn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
⊢ IsOpen (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)ᶜ
have apply : IsClosed (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)
Tactic: apply isOpen_compl_iff.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : HereditarilyLindelofSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
inst_5 : NormedAlgebra 𝕜 ℂ
μ : Measure 𝕜
inst_6 : IsFiniteMeasure μ
⊢ IsClosed (X := ℂ) ((⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ) '' μ.support)
have refine : Topology.IsClosedEmbedding (X := 𝕜) (Y := ℂ) (⇑(algebraMap 𝕜 ℂ) : (a : 𝕜) → ℂ)
Tactic: refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed ?_).mp isClosed_support
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
δ : Type u_4
γ : Type u_5
ι : Type u_6
m0_1 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s'_1 t_1 : Set α
m0 : MeasurableSpace α
s : Set α
μ : Measure α
s' : Set α
hs' : MeasurableSet s'
t : Set α
⊢ (((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
        (a : Set α) → ℝ≥0∞)
      t =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t ∩ s') :
        ℝ≥0∞)
      ((((OuterMeasure.restrict s : (a : OuterMeasure α) → OuterMeasure α) μ.toOuterMeasure : OuterMeasure α) :
            (a : Set α) → ℝ≥0∞)
          (t \ s') :
        ℝ≥0∞)
have suffices : (μ : (a : Set α) → ℝ≥0∞) (s ∩ t) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∩ s') : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((s ∩ t) \ s') : ℝ≥0∞)
Tactic: suffices μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s') by
      simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_diff_assoc]