mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
⊢ 0 ≤ 2 * r⁻¹

Tactic:
;

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
⊢ 0 ≤ 2 * r⁻¹
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: case inl
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : ↑ε' ≤ preVariationFun f s
this✝ : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - ↑ε'
⊢ ∃ P, preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ↑ε

Tactic:
have ha : a < preVariationFun f s := ENNReal.sub_lt_self h hw (by positivity)

Goal state after:
case inl
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : ↑ε' ≤ preVariationFun f s
this✝ : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - ↑ε'
ha : a < preVariationFun f s
⊢ ∃ P, preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ↑ε
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: case inl
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : ↑ε' ≤ preVariationFun f s
this : ε' ≤ ε
hw : preVariationFun f s ≠ 0
⊢ ∃ P, preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ↑ε

pp: case inr
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : ↑ε' ≤ preVariationFun f s
this : ε' ≤ ε
hw : preVariationFun f s = 0
⊢ ∃ P, preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ↑ε

Tactic:
· have : 0 < ε' := by
      simp only [lt_inf_iff, ε']
      exact ⟨hε, toNNReal_pos hw h⟩
    let a := preVariationFun f s - ε'
    have ha : a < preVariationFun f s := ENNReal.sub_lt_self h hw (by positivity)
    obtain ⟨P, hP⟩ := exists_Finpartition_sum_gt f hs ha
    use P
    calc preVariationFun f s
      _ = a + ε' := (tsub_add_cancel_of_le hε').symm
      _ ≤ ∑ p ∈ P.parts, f p + ε' := by
        exact (ENNReal.add_le_add_iff_right coe_ne_top).mpr (le_of_lt hP)
      _ ≤ ∑ p ∈ P.parts, f p + ε := by gcongr

Goal state after:
case inr
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : ↑ε' ≤ preVariationFun f s
this : ε' ≤ ε
hw : preVariationFun f s = 0
⊢ ∃ P, preVariationFun f s ≤ ∑ p ∈ P.parts, f ↑p + ↑ε
Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁹ : (i : ι) → TopologicalSpace (X i)
inst✝⁸ : ∀ (i : ι), BorelSpace (X i)
inst✝⁷ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁶ : (j : κ) → TopologicalSpace (Y j)
inst✝⁵ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁴ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝³ : Finite ι
inst✝² : Finite κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : ((i : ι) → X i) →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂ν
this : Fintype ι
⊢ μ = ν

Tactic:
;

Goal state after:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst✝⁹ : (i : ι) → TopologicalSpace (X i)
inst✝⁸ : ∀ (i : ι), BorelSpace (X i)
inst✝⁷ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁶ : (j : κ) → TopologicalSpace (Y j)
inst✝⁵ : ∀ (j : κ), BorelSpace (Y j)
inst✝⁴ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝³ : Finite ι
inst✝² : Finite κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h :
  ∀ (f : ((i : ι) → X i) →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂μ =
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)), f p.1 * g p.2 ∂ν
this : Fintype ι
⊢ μ = ν
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ε' / ↑n
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f ↑p + ↑ε
⊢ ∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f ↑p + ∑ x ∈ Finset.range n, ↑ε =
    ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p + ↑ε'

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ε' / ↑n
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f ↑p + ↑ε
⊢ ∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f ↑p + ∑ x ∈ Finset.range n, ↑ε =
    ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p + ↑ε'
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: case h₁
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ⋯
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f ↑p + ↑ε
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p ≤ preVariationFun f (⋃ i, s i)

Tactic:
;

Goal state after:
case h₁
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ⋯
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f ↑p + ↑ε
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p ≤ preVariationFun f (⋃ i, s i)
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ i, s i) < ∞
ε : ℝ≥0 := ε' / ↑n
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition ⟨s i, ⋯⟩
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f ↑p + ↑ε
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f ↑p + ↑ε' ≤ preVariationFun f (⋃ i, s i) + ↑ε'

Tactic:
gcongr; exact sum_le_preVariationFun_iUnion' f hs hs' P n

Goal state after:
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
s✝ : ℕ → { t // MeasurableSet t }
⊢ Pairwise (Disjoint on Subtype.val ∘ s✝) → 0 (⋃ i, ↑(s✝ i)) ≤ ∑' (i : ℕ), 0 ↑(s✝ i)

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
s✝ : ℕ → { t // MeasurableSet t }
⊢ Pairwise (Disjoint on Subtype.val ∘ s✝) → 0 (⋃ i, ↑(s✝ i)) ≤ ∑' (i : ℕ), 0 ↑(s✝ i)
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
q : Subtype MeasurableSet
hq : q ∈ Q.parts
⊢ ↑q = ↑q ∩ ⋃ i, s i

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
q : Subtype MeasurableSet
hq : q ∈ Q.parts
⊢ ↑q = ↑q ∩ ⋃ i, s i
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: case e_f
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
⊢ (fun i ↦ ∑ q ∈ Q.parts, f (↑q ⊓ ↑(s' i))) = fun i ↦ ∑ p ∈ (P i).parts, f ↑p

Tactic:
;

Goal state after:
case e_f
X : Type u_1
inst✝ : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition ⟨⋃ i, s i, ⋯⟩
hQ : b < ∑ p ∈ Q.parts, f ↑p
s' : ℕ → Subtype MeasurableSet := fun i ↦ ⟨s i, ⋯⟩
P : (i : ℕ) → Finpartition (s' i) := fun i ↦ Q.restrict ⋯
⊢ (fun i ↦ ∑ q ∈ Q.parts, f (↑q ⊓ ↑(s' i))) = fun i ↦ ∑ p ∈ (P i).parts, f ↑p
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
i✝ : Set X
a✝ : MeasurableSet i✝
⊢ (ennrealPreVariation 0 ⋯ ⋯) i✝ = 0 i✝

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
i✝ : Set X
a✝ : MeasurableSet i✝
⊢ (ennrealPreVariation 0 ⋯ ⋯) i✝ = 0 i✝
Module: Mathlib.MeasureTheory.Measure.PreVariation

Goal state before:
pp: X : Type u_1
inst✝ : MeasurableSpace X
s✝ : Set X
a✝ : MeasurableSet s✝
⊢ (preVariation 0 ⋯ ⋯) s✝ = 0 s✝

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : MeasurableSpace X
s✝ : Set X
a✝ : MeasurableSet s✝
⊢ (preVariation 0 ⋯ ⋯) s✝ = 0 s✝
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ ν : Measure X
x✝ : X
⊢ x✝ ∈ (μ + ν).support ↔ x✝ ∈ μ.support ∪ ν.support

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
μ ν : Measure X
x✝ : X
⊢ x✝ ∈ (μ + ν).support ↔ x✝ ∈ μ.support ∪ ν.support
Module: Mathlib.MeasureTheory.Measure.Support

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
⊢ closure[inst✝²] s ∈ ae (μ.restrict s)

Tactic:
rw [mem_ae_iff, μ.restrict_apply isClosed_closure.isOpen_compl.measurableSet]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : OpensMeasurableSpace X
s : Set X
⊢ μ ((closure[inst✝²] s)ᶜ ∩ s) = 0
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: case pos
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
⊢ HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), resolvent a x ^ 2 ∂μ) a

pp: case neg
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support = ∅
⊢ HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), resolvent a x ^ 2 ∂μ) a

Tactic:
;

Goal state after:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
⊢ HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), resolvent a x ^ 2 ∂μ) a

case neg
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support = ∅
⊢ HasDerivAt (resolventTransform μ) (∫ (x : 𝕜), resolvent a x ^ 2 ∂μ) a
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
c : E
hc : c ≠ 0
p_pos : 0 < p
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
hε : ε > 0
aux : 0 < (ε / ‖c‖) ^ p.toReal
t : Set X
ht : t ∈ 𝒜
hμt : μ t ≠ ∞
hμst : μ (s ∆ t) < ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)
⊢ ‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal)

Tactic:
by
          have := toReal_pos p_pos.ne.symm p_ne_top.elim
          rw [measureReal_def]
          gcongr
          exact ofReal_ne_top

Goal state after:
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * ((2 * r⁻¹ + 2 * r⁻¹) * ε / 4) = ε / 2

Tactic:
;

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : ℕ → Measure E
inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun n ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 : ∀ (n : ℕ) (r : ℝ), 0 < r → 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖ ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ),
    0 < r → (μ n).real {x | r < |⟪z, x⟫|} ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖
h_limsup_le :
  ∀ (r : ℝ),
    0 < r →
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop ≤ 2⁻¹ * r * ‖∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * ((2 * r⁻¹ + 2 * r⁻¹) * ε / 4) = ε / 2
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this✝ : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
h_compact : IsCompact (closure[instTopologicalSpace] {x | ∃ n, μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U) (𝓝 μ')
this : ↑μ' = ↑μ₀
⊢ μ₀ = μ'

Tactic:
;

Goal state after:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this✝ : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
h_compact : IsCompact (closure[instTopologicalSpace] {x | ∃ n, μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U) (𝓝 μ')
this : ↑μ' = ↑μ₀
⊢ μ₀ = μ'
Module: Mathlib.MeasureTheory.Measure.LevyConvergence

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this✝ : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
h_compact : IsCompact (closure[instTopologicalSpace] {x | ∃ n, μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U) (𝓝 μ')
this : ↑μ' = ↑μ₀
s✝ : Set E
a✝ : MeasurableSet s✝
⊢ ↑μ₀ s✝ = ↑μ' s✝

Tactic:
;

Goal state after:
𝕜 : Type u_2
inst✝⁴ : RCLike 𝕜
E : Type u_3
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : PolishSpace E
inst✝ : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet {x | ∃ n, ↑(μ n) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA : (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A).SeparatesPoints
hμ : ∀ g ∈ A, Tendsto (fun n ↦ ∫ (x : E), g x ∂↑(μ n)) 𝓕 (𝓝 (∫ (x : E), g x ∂↑μ₀))
this✝ : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h✝ : 𝓕.NeBot
U : Ultrafilter ι
hU : ↑U ≤ 𝓕
h_compact : IsCompact (closure[instTopologicalSpace] {x | ∃ n, μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U) (𝓝 μ')
this : ↑μ' = ↑μ₀
s✝ : Set E
a✝ : MeasurableSet s✝
⊢ ↑μ₀ s✝ = ↑μ' s✝
Module: Mathlib.MeasureTheory.Measure.ResolventTransform

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖(algebraMap 𝕜 A) x - a + (a - w)‖ ≤ ‖(algebraMap 𝕜 A) x - w‖

Tactic:
;

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : HereditarilyLindelofSpace 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : MeasurableSpace 𝕜
inst✝³ : BorelSpace 𝕜
inst✝² : RCLike A
inst✝¹ : NormedAlgebra 𝕜 A
μ : Measure 𝕜
inst✝ : IsFiniteMeasure μ
a : A
ha : a ∉ ⇑(algebraMap 𝕜 A) '' μ.support
h : μ.support.Nonempty
this : 0 < infDist a (⇑(algebraMap 𝕜 A) '' μ.support)
s : Set A := ball a (infDist a (⇑(algebraMap 𝕜 A) '' μ.support) / 2)
hs_z : s ∈ 𝓝 a
hs_μ : s ⊆ (⇑(algebraMap 𝕜 A) '' μ.support)ᶜ
resolvent_meas : ∀ᶠ (w : A) in 𝓝 a, AEStronglyMeasurable (resolvent w) μ
x : 𝕜
hx : x ∈ μ.support
w : A
hw : w ∈ s
⊢ ‖(algebraMap 𝕜 A) x - a + (a - w)‖ ≤ ‖(algebraMap 𝕜 A) x - w‖
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
x✝ : FiniteMeasure E
⊢ x✝ ∈ {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ↔
    x✝ ∈ {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C}

Tactic:
;

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
x✝ : FiniteMeasure E
⊢ x✝ ∈ {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ↔
    x✝ ∈ {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C}
Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
⊢ IsCompact {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}

Tactic:
by
  have : {μ : FiniteMeasure E | μ.mass = C ∧ ∀ n, μ (K n)ᶜ ≤ u n} =
    {μ | μ.mass ≤ C ∧ ∀ n, μ (K n)ᶜ ≤ u n} ∩ {μ | μ.mass = C} := by ext; grind
  rw [this]
  apply IsCompact.inter_right
    (isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le C hu hK h)
  exact isClosed_eq (by fun_prop) (by fun_prop)

Goal state after: