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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst✝¹ : OpensMeasurableSpace E
inst✝ : BorelSpace F
L : E →L[ℝ] F
L' : StrongDual ℝ F
⊢ Measurable ⇑L

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst✝¹ : OpensMeasurableSpace E
inst✝ : BorelSpace F
L : E →L[ℝ] F
L' : StrongDual ℝ F
⊢ charFunDual (Measure.map (⇑L) μ) L' = charFunDual μ (L' ∘SL L)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
x : E
L : StrongDual ℝ E
⊢ charFunDual (Measure.dirac x) L = cexp (↑(L x) * I)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ AEMeasurable (fun x ↦ x + r) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun v ↦ cexp (↑(L v) * I)) (Measure.map (fun x ↦ x + r) μ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ charFunDual (Measure.map (fun x ↦ x + r) μ) L = charFunDual μ L * cexp (↑(L r) * I)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ charFunDual (Measure.map (fun x ↦ r + x) μ) L = charFunDual μ L * cexp (↑(L r) * I)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
⊢ IsInducing stoneCechUnit

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
x : X
⊢ 0 ≤ (∑ n, g n) x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst✝] K
hx✝ : x ∉ K
s : Set X
hs : s ∈ {s | IsClopen s}
hx : x ∈ s
hsK : s ⊆ Kᶜ
⊢ sᶜ.indicator 1 x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
x : X
K : Set X
hK : IsClosed[inst✝] K
hx : x ∉ K
⊢ ∃ f, Continuous[inst✝, _] f ∧ f x = 0 ∧ EqOn f 1 K

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
⊢ lift.{u, 0} #↑R < lift.{0, u} 𝔠

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : StrongDual ℝ (E × F)
⊢ charFunDual (μ.prod ν) L =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
h : ∀ (x : X), 0 ≤ (∑ n, g n) x
x : X
hx : x ∈ K
⊢ (∑ n, g n) x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
⊢ ∀ (x : X), f x ≠ r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
x : X
s : Set X
hxs : x ∈ s
hs : IsOpen[inst✝¹] s
f : X → ↑I
hfc : Continuous[inst✝¹, _] f
hf₀ : f x = 0
hf₁ : EqOn f 1 sᶜ
R : Set ↑I := range f
hR : #↑R < #↑I
r : ↑I
hr : r ∈ Rᶜ
hr' : ∀ (x : X), f x ≠ r
⊢ f ⁻¹' Iio r = f ⁻¹' Iic r

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
p : ℝ≥0∞
inst✝² : Fact (1 ≤ p)
inst✝¹ : SFinite μ
inst✝ : SFinite ν
L : StrongDual ℝ (WithLp p (E × F))
⊢ charFunDual (Measure.map (toLp p) (μ.prod ν)) L =
    charFunDual μ (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
      charFunDual ν (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
hX : #X < 𝔠
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
n : Fin N
⊢ (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous[inst✝¹, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ (fun x ↦ ↑(f x)) x ≠ (fun x ↦ ↑(f x)) y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
⊢ {f | Continuous[inst✝¹, _] f}.SeparatesPoints

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous[inst✝¹, _] f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ f x ≠ f y

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ ((i : ι) → E i)
⊢ charFunDual (Measure.pi μ) L = ∏ i, charFunDual (μ i) (L ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.CompletelyRegular

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T35Space X
⊢ Function.Injective stoneCechUnit

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst✝¹] K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous[inst✝¹, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
⊢ ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst✝¹] K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous[inst✝¹, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x ↦ (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
⊢ f x = 1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst✝¹] K
x : X
x_notin_K : x ∉ K
g : X → ↑unitInterval
g_cont : Continuous[inst✝¹, _] g
gx_zero : g x = 0
g_one_on_K : EqOn g 1 K
g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1
g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x ↦ (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd
f : X →ᵇ ℝ≥0 := 1 - g'
y : X
y_in_K : y ∈ K
⊢ f y = 0

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompletelyRegularSpace X
K : Set X
K_closed : IsClosed[inst✝¹] K
x : X
x_notin_K : x ∉ K
⊢ ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0

Tactic:
by

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

Goal state before:
pp: X : Type u_2
inst✝¹ : MeasurableSpace X
inst✝ : MeasurableSpace.SeparatesPoints X
⊢ Function.Injective fun x ↦ diracProba x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
⊢ Continuous[inst✝¹, ProbabilityMeasure.instTopologicalSpace] fun x ↦ diracProba x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
⊢ ∃ U ∈ 𝓝 x, ∃ᶠ (x : X) in L, x ∉ U

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
⊢ interior U ∈ 𝓝 x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
⊢ ?m.81 ∉ (interior ?m.77)ᶜ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
U : Set X
U_nhds : U ∈ 𝓝 x
hU : ∃ᶠ (x : X) in L, x ∉ U
Uint_nhds : interior U ∈ 𝓝 x
f : X →ᵇ ℝ≥0
fx_eq_one : f x = 1
f_vanishes_outside : ∀ y ∈ (interior U)ᶜ, f y = 0
⊢ 0 < ↑1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
h : ¬Tendsto id L (𝓝 x)
⊢ ¬Tendsto diracProba L (𝓝 (diracProba x))

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : CompletelyRegularSpace X
x : X
L : Filter X
⊢ Tendsto diracProba L (𝓝 (diracProba x)) ↔ Tendsto id L (𝓝 x)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
μ : ↑(range diracProba)
h : ↑μ = diracProba x
⊢ diracProbaInverse μ = x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
⊢ diracProba x ∈ range diracProba

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x : X
⊢ diracProbaInverse ((fun x ↦ ⟨diracProba x, ⋯⟩) x) = x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
μ : ↑(range diracProba)
⊢ ↑((fun x ↦ ⟨diracProba x, ⋯⟩) (diracProbaInverse μ)) = ↑μ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
⊢ diracProba ∘ ⇑diracProbaEquiv.symm = fun μ ↦ ↑μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: p : ℝ≥0∞
inst✝⁵ : Fact (1 ≤ p)
ι : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
E : ι → Type u_5
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
L : StrongDual ℝ (PiLp p E)
⊢ charFunDual (Measure.map (toLp p) (Measure.pi μ)) L =
    ∏ i, charFunDual (μ i) (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto diracProba (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto id (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Tactic:
← (diracProbaEquiv (X := X)).symm_comp_self,

Goal state after:
X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
key :
  Tendsto diracProba (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔
    Tendsto (⇑diracProbaEquiv.symm ∘ ⇑diracProbaEquiv) (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProbaEquiv.symm μ))
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
h : μ K = ∑ i, μ (E i)
⊢ ∑ i, μ.real (E i) = μ.real K

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : CompleteSpace E
μ ν : Measure E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : charFunDual μ = charFunDual ν
⊢ μ = ν

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
μ : ↑(range diracProba)
F : Filter ↑(range diracProba)
⊢ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h :
  ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)
⊢ ξ = μ.prod ν

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
ν : Measure F
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : BorelSpace F
inst✝⁵ : SecondCountableTopology F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
ξ : Measure (E × F)
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsFiniteMeasure ξ
h : ξ = μ.prod ν
⊢ ∀ (L : StrongDual ℝ (E × F)),
    charFunDual ξ L =
      charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : OpensMeasurableSpace X
inst✝¹ : T0Space X
inst✝ : CompletelyRegularSpace X
⊢ Continuous[instTopologicalSpaceSubtype, inst✝³] ⇑diracProbaEquiv.symm

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : μ B ≤ ν (thickening ε₁.toReal B) + ε₁
⊢ μ B ≤ ν (thickening ε₂.toReal B) + ε₂

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
⊢ μ B ≤ ν (thickening c.toReal B) + c

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
⊢ ν B ≤ μ (thickening c.toReal B) + c

Tactic:
by

Goal state after: