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 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this_1 : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
this :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
grw :
  ‖Ring.inverse (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)‖ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
⊢ ‖resolvent a x‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
have grw₁ : ‖(HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)⁻¹‖ ≤
  (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
Tactic: grw [resolvent, Ring.inverse_eq_inv', norm_inv, inv_le_inv₀ (by linarith) (by positivity), this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this_1 : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
this :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
grw :
  ‖Ring.inverse (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)‖ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
grw₁ :
  ‖(HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)⁻¹‖ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
⊢ ‖resolvent a x‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
have grw₂ : ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖⁻¹ ≤
  (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
Tactic: grw [resolvent, Ring.inverse_eq_inv', norm_inv, inv_le_inv₀ (by linarith) (by positivity), this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
μ : Measure 𝕜
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
x : 𝕜
hx : x ∈ μ.support
this_1 : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
this :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
grw :
  ‖Ring.inverse (HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)‖ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
grw₁ :
  ‖(HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a)⁻¹‖ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
grw₂ :
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖⁻¹ ≤
    (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
grw₃ :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
⊢ ‖resolvent a x‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
have grw₄ : ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ ≤
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
Tactic: grw [resolvent, Ring.inverse_eq_inv', norm_inv, inv_le_inv₀ (by linarith) (by positivity), this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : HereditarilyLindelofSpace 𝕜
inst_6 : OpensMeasurableSpace 𝕜
inst_7 : CompleteSpace A
inst_8 : SecondCountableTopology A
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μ : Measure 𝕜
inst_11 : IsFiniteMeasure μ
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
⊢ Integrable (resolvent a) μ
have refine : HasFiniteIntegral (resolvent a) μ
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : HereditarilyLindelofSpace 𝕜
inst_6 : OpensMeasurableSpace 𝕜
inst_7 : CompleteSpace A
inst_8 : SecondCountableTopology A
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μ : Measure 𝕜
inst_11 : IsFiniteMeasure μ
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
⊢ HasFiniteIntegral (resolvent a) μ
have hC : ∀ᵐ (a_1 : 𝕜) ∂μ, ‖resolvent a a_1‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
Tactic: apply HasFiniteIntegral.of_bounded
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : MeasurableSpace 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : NormedDivisionRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : HereditarilyLindelofSpace 𝕜
inst_6 : OpensMeasurableSpace 𝕜
inst_7 : CompleteSpace A
inst_8 : SecondCountableTopology A
inst_9 : MeasurableSpace A
inst_10 : BorelSpace A
μ : Measure 𝕜
inst_11 : IsFiniteMeasure μ
a : A
hz : a ∉ (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support
hC : ∀ᵐ (a_1 : 𝕜) ∂μ, ‖resolvent a a_1‖ ≤ (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support))⁻¹
⊢ HasFiniteIntegral (resolvent a) μ
have C : ℝ
Tactic: apply HasFiniteIntegral.of_bounded
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ResolventTransform (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra ℝ A
inst_3 : NormedAlgebra 𝕜 A
m𝕜 : MeasurableSpace 𝕜
⊢ Eq.{u_2 + 1} (α := (a : A) → A) (resolventTransform.{u_1, u_2} (𝕜 := 𝕜) (m𝕜 := m𝕜) 0) 0
have h : ∀ (x : A), resolventTransform.{u_1, u_2} (𝕜 := 𝕜) (m𝕜 := m𝕜) 0 x = 0 x
Tactic: ext
-- 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
⊢ HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
have pos : ∀ (h : μ.support.Nonempty), HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
Tactic: by_cases! h : μ.support.Nonempty
-- 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
pos :
  ∀ (h : μ.support.Nonempty), HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
⊢ HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
have neg : ∀ (h : μ.support = ∅), HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
Tactic: by_cases! h : μ.support.Nonempty
-- 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
⊢ 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
have refine : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
Tactic: refine (IsClosed.notMem_iff_infDist_pos ?_ (h.image _)).mp ha
-- 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
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
have refine : Topology.IsClosedEmbedding.{u_1, u_2} (X := 𝕜) (Y := A) (⇑(algebraMap 𝕜 A) : (a : 𝕜) → A)
Tactic: refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed ?_).mp isClosed_support
-- 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
⊢ HasDerivAt (F := A) (fun (a : A) ↦ ∫ (x : 𝕜), resolvent a x ∂μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
have this : 0 < infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
Tactic: have : 0 < infDist a (algebraMap 𝕜 A '' μ.support) := by
    refine (IsClosed.notMem_iff_infDist_pos ?_ (h.image _)).mp ha
    refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed ?_).mp isClosed_support
    exact (algebraMap_isometry 𝕜 A).isClosedEmbedding
-- 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)
⊢ HasDerivAt (F := A) (fun (a : A) ↦ ∫ (x : 𝕜), resolvent a x ∂μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
have hs_z : s ∈ 𝓝 a
Tactic: have hs_z : s ∈ 𝓝 a := ball_mem_nhds _ (by positivity)
-- 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
⊢ ball a (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2) ⊆
    ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
have grw : infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)
Tactic: grw [ball_subset_ball, ball_infDist_subset_compl]
-- 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
⊢ HasDerivAt (F := A) (fun (a : A) ↦ ∫ (x : 𝕜), resolvent a x ∂μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
have hs_μ : s ⊆ ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support)ᶜ
Tactic: have hs_μ : s ⊆ (algebraMap 𝕜 A '' μ.support)ᶜ := by
    unfold s
    grw [ball_subset_ball, ball_infDist_subset_compl]
    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)ᶜ
⊢ ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
have h₁ : ∀ (a : A), Membership.mem (γ := Set A) {x : A | (fun (w : A) ↦ AEStronglyMeasurable (resolvent w) μ) x} a
Tactic: filter_upwards with _ using by fun_prop
-- 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)ᶜ
h₁ : ∀ (a : A), Membership.mem (γ := Set A) {x : A | (fun (w : A) ↦ AEStronglyMeasurable (resolvent w) μ) x} a
⊢ ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
have h₂ : ∀ (a : A), AEStronglyMeasurable (resolvent a) μ
Tactic: filter_upwards with _ using by fun_prop
-- 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)ᶜ
⊢ HasDerivAt (F := A) (fun (a : A) ↦ ∫ (x : 𝕜), resolvent a x ∂μ) (∫ (x : 𝕜), HPow.hPow (β := ℕ) (resolvent a x) 2 ∂μ) a
have resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
Tactic: have resolvent_meas : ∀ᶠ w in nhds a, AEStronglyMeasurable (resolvent w) μ := by
    filter_upwards with _ using by fun_prop
-- 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 : 𝕜) ∂μ,
    ∀ w ∈ s,
      ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
        HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
have h₁ : ∀ (x : 𝕜) (hx : x ∈ μ.support) (w : A) (hw : w ∈ s),
  ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
    HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
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) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖HPow.hPow (β := ℕ) (resolvent w x) 2‖ ≤
    HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
have h₁ : HPow.hPow (β := ℕ) ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖⁻¹ 2 ≤
  HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
Tactic: grw [resolvent, Ring.inverse_eq_inv, norm_pow, norm_inv]
-- 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
⊢ HPow.hPow (β := ℕ) ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖⁻¹ 2 ≤
    HPow.hPow (β := ℕ) (infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2)⁻¹ 2
have h₁ : infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) w‖
Tactic: gcongr
-- 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) -
      infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2 ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖ - ‖a - w‖
have hab : infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
  ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
Tactic: gcongr
-- 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 :
  infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
⊢ 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‖
have hcd : ‖a - w‖ ≤ infDist a ((⇑(algebraMap 𝕜 A) : (a : 𝕜) → A) '' μ.support) / 2
Tactic: gcongr
-- 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) ≤
    ‖HSub.hSub (α := A) ((algebraMap 𝕜 A : (a : 𝕜) → A) x : A) a‖
have hab : dist a ((algebraMap 𝕜 A : (a : 𝕜) → A) x) ≤ ‖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
hab : dist a ((algebraMap 𝕜 A : (a : 𝕜) → A) x) ≤ ‖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₁ : dist ((algebraMap 𝕜 A : (a : 𝕜) → A) x) 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]