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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
⊢ upcrossings a b f ω < ∞ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
have : upcrossings a b f ω < ∞ ↔ ∃ k : ℝ≥0, upcrossings a b f ω ≤ k := by
    constructor
    · intro h
      lift upcrossings a b f ω to ℝ≥0 using h.ne with r hr
      exact ⟨r, le_rfl⟩
    · rintro ⟨k, hk⟩
      exact lt_of_le_of_lt hk ENNReal.coe_lt_top

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
⊢ upcrossings a b f ω < ∞ ↔ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
⊢ ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω ≤ k

Tactic:
refine ⟨m, fun N => Nat.cast_le.1 ((hk N).trans ?_)⟩

Goal state after:
case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
N : ℕ
⊢ ↑k ≤ ↑m
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 Ω
h : MeasurableSet (s ∩ {ω | τ ω ≤ π ω})
⊢ s ∩ {ω | τ ω ≤ π ω} = s ∩ {ω | τ ω ≤ π ω} ∩ {ω | τ ω ≤ π ω}

Tactic:
rw [Set.inter_assoc, Set.inter_self]

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 ι
⊢ stoppedValue (stoppedProcess u τ) σ = fun ω ↦
    if σ ω ≠ ⊤ then stoppedValue u (fun ω ↦ min (σ ω) (τ ω)) ω
    else stoppedValue u (fun ω ↦ min (↑(Classical.arbitrary ι)) (τ ω)) ω

Tactic:
ext ω
  simp only [stoppedValue, stoppedProcess, ne_eq, ite_not]
  cases σ ω <;> cases τ ω <;> simp

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

Goal state before:
pp: case neg
Ω : 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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
h : ¬τ (↑ω).2 = ⊤
⊢ ↑↑(↑ω).1 ≤ τ (↑ω).2

Tactic:
lift τ (ω : Set.Iic i × Ω).2 to ι using h with t ht

Goal state after:
case neg
Ω : 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
sc : Set (↑(Set.Iic i) × Ω) := sᶜ
ω : ↑sc
hx_fst_le : ↑(↑ω).1 ≤ i
t : ι
ht : ↑t = τ (↑ω).2
⊢ ↑↑(↑ω).1 ≤ ↑t
Module: Mathlib.Probability.Martingale.BorelCantelli

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

Tactic:
set g : ℕ → Ω → ℝ := fun n ω => f n ω - f 0 ω
  have hg : Submartingale g ℱ μ :=
    hf.sub_martingale (martingale_const_fun _ _ (hf.stronglyAdapted 0) (hf.integrable 0))
  have hg0 : g 0 = 0 := by
    ext ω
    simp only [g, sub_self, Pi.zero_apply]
  have hgbdd : ∀ᵐ ω ∂μ, ∀ i : ℕ, |g (i + 1) ω - g i ω| ≤ ↑R := by
    simpa only [g, sub_sub_sub_cancel_right]
  filter_upwards [hg.bddAbove_iff_exists_tendsto_aux hg0 hgbdd] with ω hω
  convert! hω using 1
  · refine ⟨fun h => ?_, fun h => ?_⟩ <;> obtain ⟨b, hb⟩ := h <;>
    refine ⟨b + |f 0 ω|, fun y hy => ?_⟩ <;> obtain ⟨n, rfl⟩ := hy
    · simp_rw [g, sub_eq_add_neg]
      exact add_le_add (hb ⟨n, rfl⟩) (neg_le_abs _)
    · exact sub_le_iff_le_add.1 (le_trans (sub_le_sub_left (le_abs_self _) _) (hb ⟨n, rfl⟩))
  · refine ⟨fun h => ?_, fun h => ?_⟩ <;> obtain ⟨c, hc⟩ := h
    · exact ⟨c - f 0 ω, hc.sub_const _⟩
    · refine ⟨c + f 0 ω, ?_⟩
      have := hc.add_const (f 0 ω)
      simpa only [g, sub_add_cancel]

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

Goal state before:
pp: case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ Integrable (fun ω ↦ rexp (-t * (-X) ω)) μ

Tactic:
· simp_rw [Pi.neg_apply, neg_mul_neg]
    exact h_int

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
⊢ X ω ≤ b → rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))

Tactic:
hb

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb✝ : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
hb : X ω ≤ b
⊢ rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : IsGaussian μ
⊢ μ Set.univ = 1

Tactic:
by
    have : μ.map (0 : StrongDual ℝ E) Set.univ = 1 := by
      simp [-FunLike.coe_zero, IsGaussian.map_eq_gaussianReal]
    simpa [-FunLike.coe_zero,
      Measure.map_apply (by fun_prop : Measurable (0 : StrongDual ℝ E)) .univ] using this

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

Goal state before:
pp: case e'_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x✝ : ℝ
⊢ 0 = deriv (cgf X μ) 0

pp: case convert_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x✝ : ℝ
⊢ UniqueDiffWithinAt ℝ (Set.Icc 0 t) 0

Tactic:
· simpa [hc] using (deriv_cgf_zero (hs ⟨le_refl 0, le_of_lt ht⟩)).symm

Goal state after:
case convert_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x✝ : ℝ
⊢ UniqueDiffWithinAt ℝ (Set.Icc 0 t) 0
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case zero
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}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ μ {x | a < ‖x‖} ≤ μ {x | ‖x‖ ≤ a} * ((1 - μ {x | ‖x‖ ≤ a}) / μ {x | ‖x‖ ≤ a})

Tactic:
ENNReal.mul_div_cancel hc_pos.ne' hc_lt_top.ne

Goal state after:
case zero
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}
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ μ {x | a < ‖x‖} ≤ 1 - μ {x | ‖x‖ ≤ a}
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ ∫ (x : E), x ∂stdGaussian E = 0

Tactic:
rw [stdGaussian, integral_map _ (by fun_prop), integral_finsetSum]
  · simp [integral_smul_const, integral_eval]
  · exact fun i _ ↦ Integrable.smul_const (integrable_eval IsGaussian.integrable_id) _
  · exact (Finset.measurable_sum _ (by fun_prop)).aemeasurable

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

Goal state before:
pp: c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 < c.toReal / (1 - c).toReal

Tactic:
one_lt_div_iff

Goal state after:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case refine_2
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ (1 - c).toReal < c.toReal

Tactic:
· 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.Fernique

Goal state before:
pp: c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
⊢ 0 ≤ logRatio c

Tactic:
cases hc_ge.eq_or_lt'

Goal state after:
case inl
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h✝ : c = 2⁻¹
⊢ 0 ≤ logRatio c

case inr
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h✝ : 2⁻¹ < c
⊢ 0 ≤ logRatio c
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✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
hC'_pos : 0 < C'
hC'_lt : C' < C
h_int : ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
y : E
hy : Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
ε : ℝ := (C - C') / C'
hε : 0 < ε
x : E
⊢ ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + 2 * ‖x - y‖ * ‖y‖ ≤ ‖x - y‖ ^ 2 + ‖y‖ ^ 2 + ε * ‖x - y‖ ^ 2 + ε⁻¹ * ‖y‖ ^ 2

Tactic:
by
      simp_rw [add_assoc]
      gcongr
      exact two_mul_le_add_mul_sq (by positivity)

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
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
x : E
⊢ rexp (-C * ‖x‖ ^ 2) ≤ 1 x

Tactic:
simp only [neg_mul, Pi.one_apply, Real.exp_le_one_iff, Left.neg_nonpos_iff]

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
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
x : E
⊢ 0 ≤ C * ‖x‖ ^ 2
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
μ : Measure E
hX : HasLaw X μ P
inst✝ : IsGaussian μ
⊢ IsGaussian (Measure.map X P)

Tactic:
rwa [hX.map_eq]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ ⟪(ContinuousLinearMap.adjoint (toEuclideanCLM (CFC.sqrt S))) x,
      (ContinuousLinearMap.adjoint (toEuclideanCLM (CFC.sqrt S))) y⟫ =
    x.ofLp ⬝ᵥ S *ᵥ y.ofLp

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ MemLp id 2 (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
ContinuousLinearMap.adjoint_inner_left,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ ⟪x, (toEuclideanCLM (CFC.sqrt S)) ((ContinuousLinearMap.adjoint (toEuclideanCLM (CFC.sqrt S))) y)⟫ =
    x.ofLp ⬝ᵥ S *ᵥ y.ofLp

case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ MemLp id 2 (stdGaussian (EuclideanSpace ℝ ι))
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ ⟪x, (toEuclideanCLM (CFC.sqrt S) * toEuclideanCLM (CFC.sqrt S)) y⟫ = x.ofLp ⬝ᵥ S *ᵥ y.ofLp

pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ IsSelfAdjoint (toEuclideanCLM (CFC.sqrt S))

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ MemLp id 2 (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
← map_mul,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ ⟪x, (toEuclideanCLM (CFC.sqrt S * CFC.sqrt S)) y⟫ = x.ofLp ⬝ᵥ S *ᵥ y.ofLp

ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ IsSelfAdjoint (toEuclideanCLM (CFC.sqrt S))

case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ MemLp id 2 (stdGaussian (EuclideanSpace ℝ ι))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
⊢ ∫ (x : EuclideanSpace ℝ ↥I), x.ofLp ∂multivariateGaussian 0 (covMatrix I) = 0

Tactic:
← PiLp.coe_continuousLinearEquiv 2 ℝ,

Goal state after:
I : Finset ℝ≥0
⊢ ∫ (x : EuclideanSpace ℝ ↥I), (PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ) x ∂multivariateGaussian 0 (covMatrix I) = 0
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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (fun ω i ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i
⊢ IndepFun (fun ω i ↦ X' i ω) Y κ P

Tactic:
rintro - - ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (fun ω i ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i
s : Set ((i : S) → 𝓧 i)
hs : MeasurableSet s
t : Set 𝓨
ht : MeasurableSet t
⊢ ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X' i ω) ⁻¹' s ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X' i ω) ⁻¹' s) * (κ a) (Y ⁻¹' t)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
⊢ IsRatStieltjesPoint f (a, b) → Monotone (f (a, b))

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
hb : IsRatStieltjesPoint f (a, b)
⊢ Monotone (f (a, b))
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
⊢ IsRatStieltjesPoint f (a, b) → Tendsto (f (a, b)) atTop (𝓝 1)

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
hb : IsRatStieltjesPoint f (a, b)
⊢ Tendsto (f (a, b)) atTop (𝓝 1)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
⊢ IsRatStieltjesPoint f (a, b) → Tendsto (f (a, b)) atBot (𝓝 0)

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
hb : IsRatStieltjesPoint f (a, b)
⊢ Tendsto (f (a, b)) atBot (𝓝 0)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
⊢ IsRatStieltjesPoint f (a, b) → ∀ (q : ℚ), ⨅ r, f (a, b) ↑r = f (a, b) q

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
b : β
hb : IsRatStieltjesPoint f (a, b)
⊢ ∀ (q : ℚ), ⨅ r, f (a, b) ↑r = f (a, b) q
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
b : β
⊢ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q = f (a, b) q →
    b ∈ s → ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q = f (a, b) q

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
b : β
hb : ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q = f (a, b) q
⊢ b ∈ s → ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q = f (a, b) q
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
a : α
h : IsRatStieltjesPoint f a
q : ℚ
⊢ (if IsRatStieltjesPoint f a then f a else defaultRatCDF) q = f a q

Tactic:
if_pos h

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
a : α
h : IsRatStieltjesPoint f a
q : ℚ
⊢ f a q = f a q
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case hv
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
⊢ covarianceBilin
      (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm)
        (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)) =
    covarianceBilin (Measure.map (⇑(PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ).symm) (projectiveFamily I))

Tactic:
rw [← ContinuousLinearMap.toBilinForm_inj]
      refine LinearMap.BilinForm.ext_of_isSymm isPosSemidef_covarianceBilin.isSymm
        isPosSemidef_covarianceBilin.isSymm fun x ↦ ?_
      simp only [ContinuousLinearMap.toBilinForm_apply]
      rw [PiLp.coe_symm_continuousLinearEquiv, covarianceBilin_apply_pi, covarianceBilin_apply_pi]
      · congrm ∑ i, ∑ j, _ * ?_
        rw [covariance_eval_projectiveFamily, covariance_map]
        · wlog hij : i.1 ≤ j.1 generalizing i j
          · rw [covariance_comm, this j i (by grind), min_comm]
          rw [min_eq_left hij]
          exact h3 i j hij
        any_goals exact Measurable.aestronglyMeasurable (by fun_prop)
        exact aemeasurable_pi_lambda _ (fun _ ↦ h1.aemeasurable _)
      · exact fun i ↦ (IsGaussian.hasGaussianLaw_id.eval i).memLp_two
      · exact fun i ↦ ((h1.hasGaussianLaw I).isGaussian_map.hasGaussianLaw_id.eval i).memLp_two

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
⊢ ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
      ↑(min (t i.castSucc) (t j.castSucc)) =
    0

Tactic:
wlog h : i < j generalizing i j

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this✝ : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
this :
  ∀ (i j : Fin n),
    i ≠ j →
      i < j →
        ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
            ↑(min (t i.castSucc) (t j.castSucc)) =
          0
h : ¬i < j
⊢ ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
      ↑(min (t i.castSucc) (t j.castSucc)) =
    0

Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
this : IsProbabilityMeasure P
n : ℕ
t : Fin (n + 1) → ℝ≥0
ht : Monotone t
i j : Fin n
hij : i ≠ j
h : i < j
⊢ ↑(min (t i.succ) (t j.succ)) - ↑(min (t i.succ) (t j.castSucc)) - ↑(min (t i.castSucc) (t j.succ)) +
      ↑(min (t i.castSucc) (t j.castSucc)) =
    0