mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
⊢ MeasurableSet {ω | τ ω ≤ ↑t}

Tactic:
have : (𝓝[>] t).NeBot := ⟨ht⟩

Goal state after:
case neg
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
⊢ MeasurableSet {ω | τ ω ≤ ↑t}
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞

Tactic:
rw [mul_comm, ← ENNReal.le_div_iff_mul_le] at this

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
⊢ ∫⁻ (x : Ω), upcrossings a b f x ∂μ ≠ ∞

case h0
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ 0 ∨ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ 0

case ht
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : (∫⁻ (ω : Ω), upcrossings a b f ω ∂μ) * ENNReal.ofReal (b - a) ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
⊢ ENNReal.ofReal (b - a) ≠ ∞ ∨ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ ≠ ∞
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0

Tactic:
Set.indicator_of_notMem

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ 0 = 0

case h
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ k ∉ {n | upperCrossingTime a b f N n ω < N}
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ mgf X μ = mgf Y μ'

Tactic:
← mgf_id_map h.aemeasurable_fst,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ mgf id (Measure.map X μ) = mgf Y μ'
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝³ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
ω : Ω
⊢ τ ω ∈ WithTop.some '' ↑(Finset.Iic N)

Tactic:
simp only [Finset.coe_Iic, Set.mem_image]

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝³ : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : AddCommMonoid E
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
ω : Ω
⊢ ∃ x ∈ Set.Iic N, ↑x = τ ω
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr.h₀
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
b : ι
a✝ : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
⊢ {ω | τ ω = ↑b}.indicator (u b) ω = 0

Tactic:
Set.indicator_of_notMem

Goal state after:
case inr.h₀
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
b : ι
a✝ : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
⊢ 0 = 0

case inr.h₀.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
b : ι
a✝ : b ∈ {i ∈ s | i < n}
hneq : b ≠ i
⊢ ω ∉ {ω | τ ω = ↑b}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp ({a | ↑n ≤ τ a}.indicator (u n)) p μ

pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp (∑ i ∈ s with i < n, {ω | τ ω = ↑i}.indicator (u i)) p μ

Tactic:
· exact MemLp.indicator (ℱ.le n {a : Ω | n ≤ τ a} (hτ.measurableSet_ge n)) (hu n)

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
⊢ MemLp (∑ i ∈ s with i < n, {ω | τ ω = ↑i}.indicator (u i)) p μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:

Tactic:
l < v := hv.1
    _ ≤ v + ((v - l) ⊓ (u - v)) / 2 := le_add_of_nonneg_right (by positivity)

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}

Tactic:
refine AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq hX hY
    (convex_integrableExpSet.interior.linear_preimage reLm).isPreconnected
    (z₀ := (t : ℂ)) (by simp [ht]) ?_

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')}
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] ↑t, complexMGF X μ z = complexMGF Y μ' z
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun x ↦ x / c) (gaussianReal μ v) = gaussianReal (μ / c) (v / NNReal.mk (c ^ 2) ⋯)

Tactic:
by
  simp_rw [div_eq_mul_inv]
  convert! gaussianReal_map_mul_const c⁻¹ using 2 <;> rw [mul_comm]
  ext; simp

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (gaussianReal μ v)

Tactic:
lift p to ℝ≥0 using hp

Goal state after:
μ : ℝ
v p : ℝ≥0
⊢ MemLp id (↑p) (gaussianReal μ v)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
by
  calc charFunDual μ L
  _ = charFun (μ.map L) 1 := by rw [charFunDual_eq_charFun_map_one]
  _ = charFun (gaussianReal (μ[L]) (Var[L; μ]).toNNReal) 1 := by
    rw [IsGaussian.map_eq_gaussianReal L]
  _ = exp (μ[L] * I - Var[L; μ] / 2) := by
    rw [charFun_gaussianReal]
    simp only [ofReal_one, one_mul, Real.coe_toNNReal', one_pow, mul_one]
    congr
    · rw [integral_complex_ofReal]
    · simp only [sup_eq_left]
      exact variance_nonneg _ _

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
t : E
⊢ charFunDual μ ((toDualMap ℝ E) t) = cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)

Tactic:
IsGaussian.charFunDual_eq

Goal state after:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
t : E
⊢ cexp ((∫ (x : E), ↑(((toDualMap ℝ E) t) x) ∂μ) * I - ↑Var[⇑((toDualMap ℝ E) t); μ] / 2) =
    cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
μ✝ : Measure E
inst✝³ : IsGaussian μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
⊢ Measure.map (⇑L) (μ ∗ ν) = gaussianReal (∫ (x : E), L x ∂μ ∗ ν) Var[⇑L; μ ∗ ν].toNNReal

Tactic:
have : (μ ∗ ν)[L] = ∫ x, x ∂((μ.map L).conv (ν.map L)) := by
      rw [← Measure.map_conv_continuousLinearMap L,
        integral_map (φ := L) (by fun_prop) (by fun_prop)]

Goal state after:
E : Type u_1
F : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
μ✝ : Measure E
inst✝³ : IsGaussian μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
this : ∫ (x : E), L x ∂μ ∗ ν = ∫ (x : ℝ), x ∂Measure.map (⇑L) μ ∗ Measure.map (⇑L) ν
⊢ Measure.map (⇑L) (μ ∗ ν) = gaussianReal (∫ (x : E), L x ∂μ ∗ ν) Var[⇑L; μ ∗ ν].toNNReal
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
θ : ℝ
x y : E × E
⊢ (Real.cos θ • (x + y).1 + Real.sin θ • (x + y).2, -Real.sin θ • (x + y).1 + Real.cos θ • (x + y).2) =
    (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2) +
      (Real.cos θ • y.1 + Real.sin θ • y.2, -Real.sin θ • y.1 + Real.cos θ • y.2)

Tactic:
simp only [Prod.fst_add, smul_add, Prod.snd_add, neg_smul, Prod.mk_add_mk]

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
θ : ℝ
x y : E × E
⊢ (Real.cos θ • x.1 + Real.cos θ • y.1 + (Real.sin θ • x.2 + Real.sin θ • y.2),
      -(Real.sin θ • x.1) + -(Real.sin θ • y.1) + (Real.cos θ • x.2 + Real.cos θ • y.2)) =
    (Real.cos θ • x.1 + Real.sin θ • x.2 + (Real.cos θ • y.1 + Real.sin θ • y.2),
      -(Real.sin θ • x.1) + Real.cos θ • x.2 + (-(Real.sin θ • y.1) + Real.cos θ • y.2))
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < logRatio c

Tactic:
by
  refine div_pos (Real.log_pos ?_) (by positivity)
  rw [one_lt_div_iff]
  refine Or.inl ⟨?_, ?_⟩
  · simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]
    finiteness
  · refine (ENNReal.toReal_lt_toReal (by finiteness) (by finiteness)).mpr ?_
    refine ENNReal.sub_lt_of_lt_add hc_lt.le ?_
    rw [← two_mul]
    rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp (fun x ↦ ‖x‖ ^ 2) (p / 2) μ

Tactic:
lift p to ℝ≥0 using hp

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
⊢ MemLp (fun x ↦ ‖x‖ ^ 2) (↑p / 2) μ
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
⊢ ∃ L, Var[⇑L; μ] ≠ 0

Tactic:
contrapose! h
      exact ⟨_, eq_dirac_of_variance_eq_zero h⟩

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilin μ

Tactic:
let g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
    f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
      (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
  have : ∀ L : StrongDual ℝ E, charFunDual μ L = exp (L m * I - g L L / 2) := by
    simp [← charFun_toDual_symm_eq_charFunDual, h, g]
  have hg : g.toBilinForm.IsPosSemidef :=
    ⟨⟨fun x y ↦ by simpa [g] using hf.eq ..⟩, ⟨fun x ↦ by simpa [g] using hf.nonneg _⟩⟩
  have := gaussian_charFunDual_congr hg this
  refine ⟨this.1, ?_⟩
  ext
  simp [covarianceBilin, ← this.2, g, ← InnerProductSpace.toDual_apply_eq_toDualMap_apply,
    -InnerProductSpace.toContinuousLinearMap_toDualMap]

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ 2 * min ↑s ↑t ≤ ↑s + ↑t

Tactic:
nth_grw 1 [two_mul, min_le_left, min_le_right]

Goal state after:
Module: Mathlib.Probability.Process.FiniteDimensionalLaws

Goal state before:
pp: case refine_4
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : ∀ (I : Finset T), IdentDistrib (fun ω ↦ I.restrict fun x ↦ X x ω) (fun ω ↦ I.restrict fun x ↦ Y x ω) P P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
· exact (map_eq_iff_forall_finset_map_restrict_eq hX hY).mpr (fun I ↦ (h I).map_eq)

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case insert.hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s✝ : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
⊢ (∑ x ∈ s, X x) ⟂ᵢ[P] X i

Tactic:
convert!
      iIndepFun.indepFun_finsetSum_of_notMem₀ (i := ⟨i, mem_insert_self i s⟩) (f :=
        fun (x : (insert i s : Finset ι)) ↦ X x.1) (s := {x | x.1 ∈ s}) hX (fun i ↦ (mX i.1 i.2))
        (by simpa)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s✝ : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
⊢ ∑ x ∈ s, X x = ∑ j with ↑j ∈ s, X ↑j
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
⊢ iIndepFun (fun i ω j ↦ X' i j ω) κ P

Tactic:
by
  intro s f hf
  choose! g mg hg using hf
  have h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i := (biInf_congr hg).symm
  have h3' a : ∏ i ∈ s, κ a (f i) = ∏ i ∈ s, κ a ((fun i ω j ↦ X' i j ω) i ⁻¹' g i) := by
    refine Finset.prod_congr rfl fun i hi ↦ ?_
    rw [hg i hi]
  simp_rw [h3, h3']
  choose! I u hI hu using fun i hi ↦ (mg i hi).eq_preimage_restrict_countable
  have h4 (f : (i : S) → (j : T i) → Ω → 𝓧 i j) : ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' g i =
      ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i :=
      (biInf_congr (fun i hi ↦ by rw [hu i hi])).symm
  have h4' a (f : (i : S) → (j : T i) → Ω → 𝓧 i j) :
      ∏ i ∈ s, κ a ((fun i ω j ↦ f i j ω) i ⁻¹' g i) =
      ∏ i ∈ s, κ a ((fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i) := by
    refine Finset.prod_congr rfl fun i hi ↦ ?_
    rw [hu i hi]
  have h5 := h1 s (fun i hi ↦ ⟨g i, mg i hi, rfl⟩)
  simp_rw [h4, h4'] at h5 ⊢
  have h6 i (f : (j : T i) → Ω → 𝓧 i j) : (fun ω j ↦ f j ω) ⁻¹' (I i).domRestrict ⁻¹' (u i) =
      (fun ω (j : I i) ↦ f j ω) ⁻¹' (u i) := rfl
  simp_rw [h6] at h5 ⊢
  have h :
      ∀ᵐ a ∂P, ∀ i ∈ s, (fun ω (j : I i) ↦ X i j ω) =ᵐ[κ a] (fun ω (j : I i) ↦ X' i j ω) := by
    refine (ae_ball_iff s.countable_toSet).2 fun i hi ↦ ?_
    have := (hI i hi).to_subtype
    filter_upwards [ae_all_iff.2 fun (j : I i) ↦ h2 i j] with
      a (ha : ∀ (j : I i), ∀ᵐ ω ∂κ a, X i j ω = X' i j ω)
    filter_upwards [ae_all_iff.2 ha] with ω hω using by simp [hω]
  filter_upwards [h5, h] with a ha1 ha2
  refine .trans (measure_congr (ae_eq_set_biInter s.countable_toSet
    (fun i hi ↦ ((ha2 i hi).preimage _).symm))) (ha1.trans ?_)
  refine Finset.prod_congr rfl fun i hi ↦ ?_
  rw [measure_congr ((ha2 i hi).preimage _)]

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: case inr
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
⊢ iIndepFun (fun i ω j ↦ X i j ω) κ P

Tactic:
apply iIndepFun.congr (Filter.EventuallyEq.symm η_eq)

Goal state after:
case inr
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
⊢ iIndepFun (fun i ω j ↦ X i j ω) η P
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: ⊢ Monotone fun q ↦ if q < 0 then 0 else 1

Tactic:
intro x y hxy

Goal state after:
x y : ℚ
hxy : x ≤ y
⊢ (fun q ↦ if q < 0 then 0 else 1) x ≤ (fun q ↦ if q < 0 then 0 else 1) y
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ Monotone (stieltjesFunctionAux f a)

Tactic:
intro x y hxy

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
⊢ stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case e_f.hfin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬(ν a).restrict s = 0
b : β
⊢ ∃ i, (stieltjesOfMeasurableRat f ⋯ (a, b)).measure (Iic ↑↑i) ≠ ∞

Tactic:
· obtain ⟨q, hq⟩ := exists_rat_gt x
      exact ⟨⟨q, hq⟩, measure_ne_top _ _⟩

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a) atTop
    (𝓝 (((Kernel.const Unit ρ.fst) a).real univ))

Tactic:
by
    simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]
    have h := ρ.tendsto_IicSnd_atTop MeasurableSet.univ
    have h0 : Tendsto ENNReal.toReal (𝓝 (ρ.fst univ)) (𝓝 (ρ.fst.real univ)) :=
      ENNReal.continuousAt_toReal (measure_ne_top _ _)
    exact h0.comp (h.comp hs_tendsto)

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
⊢ ρ (s ×ˢ ⋂ i, Iic ↑↑i) = ρ (s ×ˢ Iic ↑t)

Tactic:
congr with x : 1

Goal state after:
case e_6.e_a
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
t : ℚ
x : ℝ
⊢ x ∈ ⋂ i, Iic ↑↑i ↔ x ∈ Iic ↑t