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

Goal state before:
pp: case refine_2
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
⊢ (Set.range (Y m)).Finite

pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
⊢ ∀ (x : ℕ × Ω),
    Tendsto (fun n ↦ ((fun m_1 ↦ { toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ }) n) x) atTop
      (𝓝 (Function.uncurry u x))

Tactic:
· apply Set.Finite.subset (s := ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k))
    · refine Set.Finite.biUnion' (by aesop) (fun n hn ↦ ?_)
      rcases n with rfl | n
      · exact @(h₀.approx m).finite_range
      · exact @((h n).approx m).finite_range
    · intro e he
      obtain ⟨⟨n, ω⟩, hnω⟩ := Set.mem_range.mp he
      simp_rw [Set.mem_iUnion, Set.mem_range]
      exact ⟨if n ≤ m then n else 0, by aesop, ω, by aesop⟩

Goal state after:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
⊢ ∀ (x : ℕ × Ω),
    Tendsto (fun n ↦ ((fun m_1 ↦ { toFun := Y m_1, measurableSet_fiber' := ⋯, finite_range' := ⋯ }) n) x) atTop
      (𝓝 (Function.uncurry u x))
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : PartialOrder F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
⊢ Supermartingale (c • f) ℱ μ

Tactic:
refine ⟨hf.1.smul c, fun i j hij => ?_, fun i => (hf.2.2 i).smul c⟩

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
F : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : PartialOrder F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : IsOrderedModule ℝ F
f : ι → Ω → F
c : ℝ
hc : 0 ≤ c
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ μ[(c • f) j | ↑ℱ i] ≤ᵐ[μ] (c • f) i
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
⊢ (if ∃ j ∈ Set.Icc m m, u j ω ∈ s then sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) else m) = m

Tactic:
ite_eq_right_iff,

Goal state after:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
⊢ (∃ j ∈ Set.Icc m m, u j ω ∈ s) → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
⊢ ∀ (x : ι), x ∈ Set.Icc m m ∧ u x ω ∈ s → sInf (Set.Icc m m ∩ {i | u i ω ∈ s}) = m

Tactic:
conv => intro; rw [Set.mem_Icc, Set.Icc_self, and_imp, and_imp]

Goal state after:
case inl
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
⊢ ∀ (x : ι), m ≤ x → x ≤ m → u x ω ∈ s → sInf ({m} ∩ {i | u i ω ∈ s}) = m
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 τ
i : ι
⊢ MeasurableSet {ω | ↑i < τ ω}

Tactic:
by
  have : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ := by
    ext1 ω; simp only [Set.mem_ofPred_eq, Set.mem_compl_iff, not_le]
  rw [this]
  exact (hτ.measurableSet_le i).compl

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
hle : τ ≤ π
s : Set Ω
hs : MeasurableSet s
i : ι
x✝ : Ω
hle' : π x✝ ≤ ↑i
a✝ : x✝ ∈ s
⊢ τ x✝ ≤ ↑i

Tactic:
exact le_trans (hle _) hle'

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c) then h.choose else 0
hle : ⨆ n, ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᵐ[μ.trim hle] g
ω : Ω
hω : g' ω = g ω
⊢ Tendsto (fun n ↦ f n ω) atTop (𝓝 (g' ω)) → Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))

Tactic:
hg'ω

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
g' : Ω → ℝ := fun ω ↦ if h : ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c) then h.choose else 0
hle : ⨆ n, ↑ℱ n ≤ m0
hg' : ∀ᵐ (ω : Ω) ∂μ.trim hle, Tendsto (fun n ↦ f n ω) atTop (𝓝 (g' ω))
g : Ω → ℝ
hgm : StronglyMeasurable g
hae : g' =ᵐ[μ.trim hle] g
ω : Ω
hω : g' ω = g ω
hg'ω : Tendsto (fun n ↦ f n ω) atTop (𝓝 (g' ω))
⊢ Tendsto (fun n ↦ f n ω) atTop (𝓝 (g ω))
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i

Tactic:
exact upcrossingsBefore_eq_sum hab

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

Goal state before:
pp: case pos.h_mono
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : a < b
this : ∀ (N : ℕ), ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ = ENNReal.ofReal (∫ (ω : Ω), (f N ω - a)⁺ ∂μ)
ω : Ω
N M : ℕ
hNM : N ≤ M
⊢ upcrossingsBefore a b f N ω ≤ upcrossingsBefore a b f M ω

Tactic:
exact upcrossingsBefore_mono hab hNM ω

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:
by
  rw [stoppedProcess_stoppedProcess]; rfl

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
⊢ mgf X 0 = 0

Tactic:
ext; simp [mgf]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬μ.real Set.univ = 0

Tactic:
measureReal_eq_zero_iff,

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬μ Set.univ = 0
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
inst✝ : MeasurableSpace E
μ : Measure E
L : E ≃L[𝕜] F
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)

Tactic:
by_cases h : Integrable (fun x ↦ x) μ

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
inst✝ : MeasurableSpace E
μ : Measure E
L : E ≃L[𝕜] F
h : Integrable (fun x ↦ x) μ
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)

case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedSpace ℝ F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
inst✝ : MeasurableSpace E
μ : Measure E
L : E ≃L[𝕜] F
h : ¬Integrable (fun x ↦ x) μ
⊢ ∫ (x : E), L x ∂μ = L (∫ (x : E), id x ∂μ)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω ↦ rexp (-t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp (|t| * |X ω|)) μ

Tactic:
rcases le_total 0 t with ht_nonneg | ht_nonpos
  · simp_rw [abs_of_nonneg ht_nonneg]
    exact integrable_exp_mul_abs ht_int_pos ht_int_neg
  · simp_rw [abs_of_nonpos ht_nonpos]
    exact integrable_exp_mul_abs ht_int_neg (by simpa using ht_int_pos)

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

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ deriv (cgf X μ) v = (∫ (x : Ω), (fun ω ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
simp only [hμ, cgf_zero_measure, integral_zero_measure, mgf_zero_measure, div_zero,
      Pi.zero_apply]
    exact deriv_const v 0

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

Goal state before:
pp: case left
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ l < v + min (v - l) (u - v) / 2

pp: case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 < u

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

Goal state after:
case right
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 < u
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω ↦ ↑|X ω| ^ n * cexp (z * ↑(X ω))) μ

Tactic:
convert! integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ ↑|X x✝| ^ n = ↑(|X x✝| ^ ↑n)
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✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ ((covarianceBilin μ) x) y = cov[fun u ↦ ⟪x, u⟫, fun u ↦ ⟪y, u⟫; μ]

Tactic:
rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_eq_covariance h]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ cov[⇑((toDualMap ℝ E) x), ⇑((toDualMap ℝ E) y); μ] = cov[fun u ↦ ⟪x, u⟫, fun u ↦ ⟪y, u⟫; μ]
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
⊢ ((∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)).toReal ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹

Tactic:
simp only [one_div]

Goal state after:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
⊢ ((∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹).toReal ≤
    (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤
    ENNReal.ofReal ((‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹)

Tactic:
rw [← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤
    ENNReal.ofReal (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
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
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ)) {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} =
    (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}

Tactic:
rw [Measure.map_apply (by fun_prop)]

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ (μ.prod μ) (⇑(ContinuousLinearMap.rotation (-(π / 4))) ⁻¹' {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}) =
    (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}

E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ MeasurableSet {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E
h2 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E =
    Real.sin θ • L ∘SL ContinuousLinearMap.inl ℝ E E + Real.cos θ • L ∘SL ContinuousLinearMap.inr ℝ E E
⊢ Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E); μ] +
      Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ] =
    Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]

Tactic:
rw [h1, h2]

Goal state after:
case e_a
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E
h2 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E =
    Real.sin θ • L ∘SL ContinuousLinearMap.inl ℝ E E + Real.cos θ • L ∘SL ContinuousLinearMap.inr ℝ E E
⊢ Var[⇑(Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E); μ] +
      Var[⇑(Real.sin θ • L ∘SL ContinuousLinearMap.inl ℝ E E + Real.cos θ • L ∘SL ContinuousLinearMap.inr ℝ E E); μ] =
    Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]
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
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (L : StrongDual ℝ E), charFunDual (Measure.map X P) L = cexp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * I - ↑Var[⇑L ∘ X; P] / 2)
⊢ HasGaussianLaw X P

Tactic:
by
    refine ⟨isGaussian_iff_charFunDual_eq.2 fun t ↦ ?_⟩
    rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def]
    all_goals fun_prop

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

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ gaussianReal (∫ (a : ↥I → ℝ), a s ∂projectiveFamily I - ∫ (a : ↥I → ℝ), a t ∂projectiveFamily I)
      (↑↑s - 2 * ↑(min ↑s ↑t) + ↑↑t).toNNReal =
    gaussianReal 0 (nndist ↑s ↑t)

Tactic:
congr
      · simp
      norm_cast
      rw [sub_add_eq_add_sub, ← NNReal.coe_add, ← NNReal.coe_sub, Real.toNNReal_coe]
      · wlog hst : (s : ℝ≥0) ≤ t generalizing s t
        · convert this t s (le_of_not_ge hst) using 1
          · rw [add_comm, min_comm]
          · rw [nndist_comm]
        grw [min_eq_left hst, NNReal.nndist_eq, max_eq_right (by grw [hst]), two_mul,
          add_tsub_add_eq_tsub_left]
      nth_grw 1 [two_mul, min_le_left, min_le_right]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ ∫⁻ (x_1 : β), ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) x) ∂ν a ≠ ∞

Tactic:
lintegral_stieltjesOfMeasurableRat hf

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ (κ a) (univ ×ˢ Iic x) ≠ ∞
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0) (t : ↑(Set.Iic t₀)), cov[fun ω ↦ B (t₀ + s) ω - B t₀ ω, B ↑t; P] = 0

Tactic:
· rintro s ⟨t, ht : t ≤ t₀⟩
    have := hB.isGaussianProcess.isProbabilityMeasure
    rw [covariance_fun_sub_left, hB.covariance_eval, hB.covariance_eval, min_eq_right, min_eq_right,
      sub_self]
    · grind
    · simp [ht, le_add_right]
    all_goals exact (hB.isGaussianProcess.hasGaussianLaw_eval _).memLp_two

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 t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq : ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a = (κ a) t
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t)ᶜ ∂ν a =
    ∫⁻ (b : β),
      ((IsCondKernelCDF.toKernel f hf) (a, b)) univ - ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' t) ∂ν a

Tactic:
by
        congr with x : 1
        exact measure_compl (measurable_prodMk_left ht)
          (measure_ne_top (hf.toKernel f (a, x)) _)

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 α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a ↦ κ.density ν a x s

Tactic:
by
  change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun a ↦ (a, x)))
  exact (measurable_density κ ν hs).comp measurable_prodMk_right

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 α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable fun x ↦ κ.density ν a x s

Tactic:
change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun x ↦ (a, x)))

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable ((fun p ↦ κ.density ν p.1 p.2 s) ∘ fun x ↦ (a, x))
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst✝ : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable X (Measure.map f ν)
hY : AEMeasurable Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ ⇑(condDistrib Y X (Measure.map f ν)) =ᵐ[Measure.map X (Measure.map f ν)] ⇑(condDistrib (Y ∘ f) (X ∘ f) ν)

Tactic:
refine condDistrib_ae_eq_of_measure_eq_compProd (μ := ν.map f) X hY ?_

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
ν : Measure γ
inst✝ : IsFiniteMeasure ν
f : γ → α
hX : AEMeasurable X (Measure.map f ν)
hY : AEMeasurable Y (Measure.map f ν)
hf : AEMeasurable f ν
⊢ Measure.map (fun x ↦ (X x, Y x)) (Measure.map f ν) = Measure.map X (Measure.map f ν) ⊗ₘ condDistrib (Y ∘ f) (X ∘ f) ν
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
this : ⇑κ =ᵐ[(μ ⊗ₘ κ).fst] ⇑(μ ⊗ₘ κ).condKernel
⊢ ⇑κ =ᵐ[μ] ⇑(μ ⊗ₘ κ).condKernel

Tactic:
rwa [Measure.fst_compProd] at this

Goal state after: