mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
x✝ : upcrossingsBefore a b f N ω ∈ Finset.range N
hi : upcrossingsBefore a b f N ω ∉ Finset.range (upcrossingsBefore a b f N ω)
heq : ¬lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
⊢ 0 ≤ f (↑N).untopA ω - f (↑(lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω)).untopA ω

Tactic:
· rw [sub_nonneg]
            exact le_trans (stoppedValue_lowerCrossingTime heq) hf

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalStopping

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
⊢ Submartingale f 𝒢 μ

Tactic:
refine submartingale_of_setIntegral_le hadp hint fun i j hij s hs => ?_

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : SigmaFiniteFiltration μ 𝒢
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf :
  ∀ (τ π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ →
      IsStoppingTime 𝒢 π →
        τ ≤ π → (∃ N, ∀ (ω : Ω), π ω ≤ ↑N) → ∫ (x : Ω), stoppedValue f τ x ∂μ ≤ ∫ (x : Ω), stoppedValue f π x ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
inst✝² : TopologicalSpace ι
inst✝¹ : SecondCountableTopology ι
inst✝ : OrderTopology ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
s : Set Ω
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ π ω}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ π ω})

Tactic:
by
  constructor <;> intro h
  · have : s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω} := by
      rw [Set.inter_assoc, Set.inter_self]
    rw [this]
    exact measurableSet_inter_le _ hπ _ h
  · rw [measurableSet_min_iff hτ hπ] at h
    exact h.1

Goal state after:
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b ≤ a
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
· rw [← sub_nonpos] at hab
    rw [ENNReal.ofReal_of_nonpos hab, zero_mul]
    exact zero_le

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
⊢ stoppedProcess (stoppedProcess u τ) σ = stoppedProcess u fun ω ↦ min (σ ω) (τ ω)

Tactic:
rw [stoppedProcess_stoppedProcess]

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : Nonempty ι
u : ι → Ω → β
τ σ : Ω → WithTop ι
inst✝ : LinearOrder ι
⊢ stoppedProcess u (σ ⊓ τ) = stoppedProcess u fun ω ↦ min (σ ω) (τ ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_1.coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
j : ι
h_set_eq : (fun x ↦ τ (↑x).2) ⁻¹' Set.Iic ↑j = (fun x ↦ (↑x).2) ⁻¹' {ω | τ ω ≤ ↑(min i j)}
⊢ MeasurableSet ((fun a ↦ τ (↑a).2) ⁻¹' Set.Iic ↑j)

Tactic:
rw [h_set_eq]

Goal state after:
case refine_1.coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : Nonempty ι
τ : Ω → WithTop ι
inst✝⁶ : LinearOrder ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : SecondCountableTopology ι
inst✝¹ : BorelSpace ι
f : Filtration ι m
inst✝ : PseudoMetrizableSpace ι
hτ : IsStoppingTime f τ
i : ι
m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)
m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x ↦ Subtype.instMeasurableSpace
s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ ↑i}
hs : MeasurableSet s
h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x ↦ ↑(↑x).1
j : ι
h_set_eq : (fun x ↦ τ (↑x).2) ⁻¹' Set.Iic ↑j = (fun x ↦ (↑x).2) ⁻¹' {ω | τ ω ≤ ↑(min i j)}
⊢ MeasurableSet ((fun x ↦ (↑x).2) ⁻¹' {ω | τ ω ≤ ↑(min i j)})
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
h_add : X = (fun x ↦ X x - integral μ X) + fun x ↦ integral μ X
⊢ Integrable X μ

Tactic:
h_add

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
h_int : ¬Integrable X μ
h_sub : Integrable (fun x ↦ X x - integral μ X) μ
h_add : X = (fun x ↦ X x - integral μ X) + fun x ↦ integral μ X
⊢ Integrable ((fun x ↦ X x - integral μ X) + fun x ↦ integral μ X) μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
rw [mgf_undef htX]

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᵐ[μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω ↦ rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ 0 ≤ mgf Y μ t
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1

Tactic:
rw [← ENNReal.toReal_eq_one_iff]

Goal state after:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ (∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (fun ω ↦ |X ω| ^ p * rexp (v * X ω)) μ
⊢ ∀ᵐ (a : Ω) ∂μ, ‖|X a ^ p| * rexp (v * X a)‖ ≤ |X a| ^ p * rexp (v * X a)

Tactic:
· refine ae_of_all _ fun ω ↦ ?_
      simp only [norm_mul, norm_eq_abs, abs_abs, abs_exp]
      gcongr
      exact abs_rpow_le_abs_rpow _ _

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ∫ (x : ℝ), gaussianPDFReal μ v x • cexp (z * ↑x) = ∫ (x : ℝ), ↑(gaussianPDFReal μ v x) * cexp (z * ↑x)

Tactic:
Complex.real_smul

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

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
⊢ ((covarianceBilin μ) x) y = x * y * Var[id; μ]

Tactic:
by_cases h : MemLp id 2 μ

Goal state after:
case pos
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ ((covarianceBilin μ) x) y = x * y * Var[id; μ]

case neg
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : ¬MemLp id 2 μ
⊢ ((covarianceBilin μ) x) y = x * y * Var[id; μ]
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ

Tactic:
by_cases h : MemLp id 2 μ

Goal state after:
case pos
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ

case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
⊢ covarianceBilin (Measure.map (fun x ↦ c + x) μ) = covarianceBilin μ
Module: Mathlib.Probability.Distributions.Gaussian.Basic

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

pp: case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ↑Var[⇑(u • L); μ] = ↑(max Var[⇑L; μ] 0) * ↑u ^ 2

Tactic:
· rw [integral_const_mul, integral_complex_ofReal]

Goal state after:
case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ↑Var[⇑(u • L); μ] = ↑(max Var[⇑L; μ] 0) * ↑u ^ 2
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

Tactic:
by_cases h : MemLp id 2 μ

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : ¬MemLp id 2 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L : StrongDual ℝ E
⊢ 0 ≤ ((covarianceBilinDual μ) L) L

Tactic:
by_cases h : MemLp id 2 μ

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L : StrongDual ℝ E
h : MemLp id 2 μ
⊢ 0 ≤ ((covarianceBilinDual μ) L) L

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : BorelSpace E
L : StrongDual ℝ E
h : ¬MemLp id 2 μ
⊢ 0 ≤ ((covarianceBilinDual μ) L) L
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : OrthonormalBasis ι ℝ E
this : (fun x ↦ ∑ i, x i • b i) = ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2
⊢ stdGaussian E =
    Measure.map (⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2) (Measure.pi fun x ↦ gaussianReal 0 1)

Tactic:
← Measure.map_map,

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : OrthonormalBasis ι ℝ E
this : (fun x ↦ ∑ i, x i • b i) = ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2
⊢ stdGaussian E =
    Measure.map (⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)))
      (Measure.map (toLp 2) (Measure.pi fun x ↦ gaussianReal 0 1))

case hg
ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : OrthonormalBasis ι ℝ E
this : (fun x ↦ ∑ i, x i • b i) = ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2
⊢ Measurable ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι))

case hf
ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : OrthonormalBasis ι ℝ E
this : (fun x ↦ ∑ i, x i • b i) = ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2
⊢ Measurable (toLp 2)

ι : Type u_1
inst✝⁵ : Fintype ι
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : OrthonormalBasis ι ℝ E
this : (fun x ↦ ∑ i, x i • b i) = ⇑((EuclideanSpace.basisFun ι ℝ).equiv b (Equiv.refl ι)) ∘ toLp 2
⊢ MeasurableSpace (EuclideanSpace ℝ ι)
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
⊢ X s - X r =ᵐ[P] X s

Tactic:
filter_upwards [h] with ω hω using by simp [hω]

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

Goal state before:
pp: case empty
Ω : 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
mX : ∀ i ∈ ∅, AEMeasurable (X i) P
hX : iIndepFun (∅.restrict X) P
x✝ : StrongDual ℝ E
⊢ charFunDual (Measure.map (∑ i ∈ ∅, X i) P) x✝ = (∏ i ∈ ∅, charFunDual (Measure.map (X i) P)) x✝

Tactic:
simp [show (0 : Ω → E) = fun _ ↦ 0 from rfl]

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

Goal state before:
pp: 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 : ∀ (t : T), X t =ᵐ[P] Y t
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
map_eq_iff_forall_finset_map_restrict_eq hX hY

Goal state after:
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 : ∀ (t : T), X t =ᵐ[P] Y t
⊢ ∀ (I : Finset T), Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: q : ℚ
⊢ defaultRatCDF q ≤ 1

Tactic:
by
  unfold defaultRatCDF
  split_ifs <;> simp

Goal state after:
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 : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑κ ∘ₘ P)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
⊢ iIndepFun (fun i ω j ↦ X i j ω) κ P

Tactic:
refine process_congr ?_ (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk.symm)
  refine iIndepFun_process (fun i j ↦ (hX i j).measurable_mk) fun I J ↦ ?_
  exact (h I J).process_congr (fun i j ↦ Measure.ae_ae_of_ae_comp (hX i j).ae_eq_mk)

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

Goal state before:
pp: case neg.hs
α : 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
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a =
    ∫⁻ (b : β) in s, ⨅ r, ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑↑r) ∂ν a
h_nonempty : Nonempty { r' // x < ↑r' }
⊢ Monotone fun b ↦ s ×ˢ Iic ↑↑b

Tactic:
exact fun i j hij ↦ prod_mono_right (by gcongr)

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

Goal state before:
pp: case refine_3.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P

pp: case refine_3.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X t - X s) 2 P

pp: case refine_3.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P

pp: case refine_3.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X t - X s) 2 P

pp: case refine_3.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P

Tactic:
· exact (law s).hasGaussianLaw.memLp_two

Goal state after:
case refine_3.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X t - X s) 2 P

case refine_3.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P

case refine_3.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X t - X s) 2 P

case refine_3.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_3.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P

pp: case refine_3.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X t - X s) 2 P

pp: case refine_3.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P

Tactic:
· exact (law s).hasGaussianLaw.memLp_two

Goal state after:
case refine_3.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X t - X s) 2 P

case refine_3.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_3.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
h0 : ∀ᵐ (ω : Ω) ∂P, X 0 ω = 0
s t : ℝ≥0
hst : s ≤ t
h1 : X s ⟂ᵢ[P] X t - X s
this : IsProbabilityMeasure P
h2 : X t = X t - X s + X s
⊢ MemLp (X s) 2 P

Tactic:
· exact (law s).hasGaussianLaw.memLp_two

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
n : ℕ
x✝ : Ω
⊢ ∫ (x : Ω), X 0 x ∂P = ∫ (x : Ω), X n x ∂P

Tactic:
(hident n).integral_eq

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
n : ℕ
x✝ : Ω
⊢ ∫ (x : Ω), X 0 x ∂P = ∫ (x : Ω), X 0 x ∂P