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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
⊢ b - a ≤ (f ω i - a)⁺ ↔ b ≤ f ω i

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b - a ≤ (f ω i - a)⁺
⊢ b ≤ f ω i

case refine_2
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
hab : a < b
hab' : 0 < b - a
i : Ω
ω : ℕ
h : b ≤ f ω i
⊢ b - a ≤ (f ω i - a)⁺
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : ℕ → Set Ω
hs : ∀ (i : ℕ), MeasurableSet (s i) ∧ ∀ (i_1 : ι), MeasurableSet (s i ∩ {ω | τ ω ≤ ↑i_1})
⊢ MeasurableSet (⋃ i, s i) ∧ ∀ (i : ι), MeasurableSet ((⋃ i, s i) ∩ {ω | τ ω ≤ ↑i})

Tactic:
by
    refine ⟨MeasurableSet.iUnion fun i ↦ (hs i).1, fun i ↦ ?_⟩
    replace hs := fun i ↦ (hs i).2
    rw [forall_comm] at hs
    rw [Set.iUnion_inter]
    exact MeasurableSet.iUnion (hs i)

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace

Tactic:
by
  refine le_antisymm ?_ ?_
  · exact le_inf (measurableSpace_mono _ hτ fun _ => min_le_left _ _)
      (measurableSpace_mono _ hπ fun _ => min_le_right _ _)
  · intro s
    change MeasurableSet[hτ.measurableSpace] s ∧ MeasurableSet[hπ.measurableSpace] s →
      MeasurableSet[(hτ.min hπ).measurableSpace] s
    simp_rw [IsStoppingTime.measurableSet]
    have : ∀ i, {ω | min (τ ω) (π ω) ≤ i} = {ω | τ ω ≤ i} ∪ {ω | π ω ≤ i} := by
      intro i; ext1 ω; simp
    simp_rw [this, Set.inter_union_distrib_left]
    exact fun h ↦ ⟨h.1.1, fun i ↦ (h.left.2 i).union (h.right.2 i)⟩

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ ↑i})

Tactic:
by
  rw [IsStoppingTime.measurableSet_min_iff hτ (isStoppingTime_const _ i),
    IsStoppingTime.measurableSpace_const, IsStoppingTime.measurableSet]
  refine ⟨fun h => ⟨h, ?_⟩, fun h ↦ h.1⟩
  have h' := h.2 i
  rwa [Set.inter_assoc, Set.inter_self] at h'

Goal state after:
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun f μ
hij : i < j
⊢ Indep (⨆ k ∈ {j}, MeasurableSpace.comap (f k) mβ) (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ

Tactic:
exact indep_iSup_of_disjoint (fun k => (hf k).measurable.comap_le) hfi (by simpa)

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

Goal state before:
pp: case e'_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := ⋯
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ BddAbove (Set.range fun n ↦ f n ω) ↔ BddAbove (Set.range fun n ↦ g n ω)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case e'_1.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
h : BddAbove (Set.range fun n ↦ f n ω)
⊢ BddAbove (Set.range fun n ↦ g n ω)

case e'_1.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
h : BddAbove (Set.range fun n ↦ g n ω)
⊢ BddAbove (Set.range fun n ↦ f n ω)
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case e'_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := ⋯
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ (∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case e'_2.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)

case e'_2.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
g : ℕ → Ω → ℝ := fun n ω ↦ f n ω - f 0 ω
hg : Submartingale g ℱ μ
hg0 : g 0 = 0
hgbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |g (i + 1) ω - g i ω| ≤ ↑R
ω : Ω
hω : BddAbove (Set.range fun n ↦ g n ω) ↔ ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
h : ∃ c, Tendsto (fun n ↦ g n ω) atTop (𝓝 c)
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace

Tactic:
by
      rw [IsStoppingTime.measurableSpace_min_const]
      exact inf_le_left

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
f : Ω → E
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
⊢ μ[f | ⋯.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}] μ[f | hτ.measurableSpace]

Tactic:
refine (condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le
    (hτ.min hσ).measurableSpace_le (hτ.measurableSet_le_stopping_time hσ) fun t => ?_).symm

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁷ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
f : Ω → E
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : SecondCountableTopology ι
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
this : SigmaFinite (μ.trim ⋯)
t : Set Ω
⊢ MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t) ↔ MeasurableSet ({ω | τ ω ≤ σ ω} ∩ t)
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ HasDerivAt (fun t ↦ ∫ (x : Ω), (fun ω ↦ X ω ^ n * rexp (t * X ω)) x ∂μ)
    (∫ (x : Ω), (fun ω ↦ X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ) t

Tactic:
by
  have h_re_of_mem n t (ht' : t ∈ interior (integrableExpSet X μ)) :
      (∫ ω, X ω ^ n * Complex.exp (t * X ω) ∂μ).re = ∫ ω, X ω ^ n * exp (t * X ω) ∂μ := by
    rw [← RCLike.re_eq_complex_re, ← integral_re]
    · norm_cast
    · refine integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet ?_ n
      simpa using ht'
  have h_re n : ∀ᶠ t' : ℝ in 𝓝 t, (∫ ω, X ω ^ n * Complex.exp (t' * X ω) ∂μ).re
      = ∫ ω, X ω ^ n * exp (t' * X ω) ∂μ := by
    filter_upwards [isOpen_interior.eventually_mem ht] with t ht' using h_re_of_mem n t ht'
  rw [← EventuallyEq.hasDerivAt_iff (h_re _), ← h_re_of_mem _ t ht]
  exact (hasDerivAt_integral_pow_mul_exp (by simp [ht]) n).real_of_complex

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : ℝ
v : ℝ≥0
f : ℝ → E
hv : v ≠ 0
⊢ ∫ (x : ℝ), f x ∂gaussianReal μ v = ∫ (x : ℝ), gaussianPDFReal μ v x • f x

Tactic:
by
  simp [gaussianReal, hv,
    integral_withDensity_eq_integral_toReal_smul (measurable_gaussianPDF _ _)
      (ae_of_all _ fun _ ↦ gaussianPDF_lt_top)]

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

Goal state before:
pp: case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ ((∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) / mgf X μ v ^ 2 = deriv (cgf X μ) v ^ 2

Tactic:
rw [deriv_cgf h]
      ring

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]

Goal state after:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ AEMeasurable X P

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ AEMeasurable Y P

case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (Measure.map X P)

case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (Measure.map Y P)
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 μ
c : E
L : StrongDual ℝ E
⊢ cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I) =
    cexp ((∫ (x : E), ↑(L x) ∂Measure.map (fun x ↦ x + c) μ) * I - ↑Var[⇑L; Measure.map (fun x ↦ x + c) μ] / 2)

Tactic:
have hL_comp : L ∘ (fun x ↦ x + c) = fun x ↦ L x + L c := by ext; simp

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 μ
c : E
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I) =
    cexp ((∫ (x : E), ↑(L x) ∂Measure.map (fun x ↦ x + c) μ) * I - ↑Var[⇑L; Measure.map (fun x ↦ x + c) μ] / 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 : ∀ (L : StrongDual ℝ E), Var[⇑L; μ] = 0
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp (↑(L (∫ (x : E), x ∂μ)) * I)

Tactic:
charFunDual_eq L,

Goal state after:
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 : ∀ (L : StrongDual ℝ E), Var[⇑L; μ] = 0
L : StrongDual ℝ E
⊢ cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2) = cexp (↑(L (∫ (x : E), x ∂μ)) * I)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
⊢ ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * μ {x | t n < ‖x‖} ≤
    ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
conv_rhs => rw [mul_assoc]
    gcongr
    exact measure_gt_normThreshold_le_exp h_rot ha_gt ha_lt n

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)

Tactic:
rw [hX.isGaussian_map.charFunDual_eq, integral_map hX.aemeasurable (by fun_prop),
    variance_map (by fun_prop) hX.aemeasurable, integral_complex_ofReal, Function.comp_def]

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

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw (fun ω ↦ (X s ω, X t ω)) P

Tactic:
by
  classical
  exact (hX.hasGaussianLaw {s, t}).prodMk ⟨s, by simp⟩ ⟨t, by simp⟩

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

Goal state before:
pp: case neg
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

Tactic:
let μ' := cond μ .univ

Goal state after:
case neg
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: ⊢ Tendsto defaultRatCDF atBot (𝓝 0)

Tactic:
refine (tendsto_congr' ?_).mp tendsto_const_nhds
  rw [EventuallyEq, eventually_atBot]
  refine ⟨-1, fun q hq => (if_pos (hq.trans_lt ?_)).symm⟩
  linarith

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ s ×ˢ t ⊆ s ×ˢ univ

Tactic:
prod_subset_prod_iff

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ s ⊆ s ∧ t ⊆ univ ∨ s = ∅ ∨ t = ∅
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∀ (i : ℕ), AEMeasurable (fun b ↦ ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i)) ((ν a).restrict s)

Tactic:
exact fun i ↦
        ((Kernel.measurable_coe _ (hf_meas i)).comp measurable_prodMk_left).aemeasurable.restrict

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun p ↦ (κ p.1) (countablePartitionSet n p.2 ×ˢ s) / (ν p.1) (countablePartitionSet n p.2)

Tactic:
refine Measurable.mono (measurable_densityProcess_countableFiltration_aux κ ν n hs) ?_ le_rfl

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ mα.prod (↑(countableFiltration γ) n) ≤ Prod.instMeasurableSpace
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0

Tactic:
have hs : MeasurableSet s := h_meas measurableSet_Ici

Goal state after:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
t : γ
ht : t ∈ u
⊢ (κ a) (countablePartitionSet n t ×ˢ s) / (ν a) (countablePartitionSet n t) = (κ a) (u ×ˢ s) / (ν a) u

Tactic:
countablePartitionSet_of_mem hu ht

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
t : γ
ht : t ∈ u
⊢ (κ a) (u ×ˢ s) / (ν a) u = (κ a) (u ×ˢ s) / (ν a) u
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)

Tactic:
rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int

Goal state after:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)) ∧
    Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (fun x ↦ ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst

Tactic:
rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int

Goal state after:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf_int :
  (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)) ∧
    Integrable (fun a ↦ ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (fun x ↦ ∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x) ρ.fst
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
⊢ IsMarkovKernel (partialTraj κ a b)

Tactic:
by
  obtain hab | hba := le_total a b
  · induction b, hab using Nat.le_induction with
    | base => rw [partialTraj_self]; infer_instance
    | succ k hak =>
      rw [partialTraj_succ_of_le hak]
      have := IsMarkovKernel.map (κ k) (piSingleton k).measurable
      exact IsMarkovKernel.map _ measurable_IicProdIoc
  · rw [partialTraj_le hba]; infer_instance

Goal state after: