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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
ω : Ω
h : τ ω < ↑n
⊢ τ ω ∈ WithTop.some '' ↑(Finset.Iic n)

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

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁶ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝⁵ : LinearOrder ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
inst✝² : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), Integrable (u n) μ
n : ι
ω : Ω
h : τ ω < ↑n
⊢ ∃ x ≤ n, ↑x = τ ω
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case mp.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd✝ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun n ↦ f n ω) atTop atTop
b : ℝ
hbdd : b ∈ upperBounds (Set.range fun n ↦ predictablePart f ℱ μ n ω)
⊢ False

Tactic:
rw [← tendsto_neg_atBot_iff] at ht

Goal state after:
case mp.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hfmono : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
hf : StronglyAdapted ℱ f
hint : ∀ (n : ℕ), Integrable (f n) μ
hbdd✝ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), ‖f (n + 1) ω - f n ω‖ ≤ ↑R
h₀ : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)
h₁ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
h₂ : ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
h₃ : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
ω : Ω
hω₁ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atTop
hω₂ : ¬Tendsto (fun n ↦ martingalePart f ℱ μ n ω) atTop atBot
hω₃ : ∀ (n : ℕ), 0 ≤ μ[f (n + 1) - f n | ↑ℱ n] ω
hω₄ : ∀ (n : ℕ), f n ω ≤ f (n + 1) ω
ht : Tendsto (fun x ↦ -f x ω) atTop atBot
b : ℝ
hbdd : b ∈ upperBounds (Set.range fun n ↦ predictablePart f ℱ μ n ω)
⊢ False
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case refine_2.e_a.inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)

Tactic:
· rw [abs_of_nonpos hx]
      simp only [neg_mul, mul_neg, sup_eq_right, exp_le_exp, le_neg_self_iff]
      exact mul_nonpos_of_nonneg_of_nonpos (abs_nonneg _) hx

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

Goal state before:
pp: case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ |X ω| ^ (n + 1) * ‖cexp (ε * ↑(X ω))‖ ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)

Tactic:
Complex.norm_exp

Goal state after:
case refine_4
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ |X ω| ^ (n + 1) * rexp (ε * ↑(X ω)).re ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 =
    (∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ) / mgf X μ v -
        (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v +
      deriv (cgf X μ) v ^ 2 * mgf X μ v / mgf X μ v

Tactic:
sub_add

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2 =
    (∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ) / mgf X μ v -
      ((2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v -
        deriv (cgf X μ) v ^ 2 * mgf X μ v / mgf X μ v)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case hX
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (Measure.map (⇑L) μ)
L : StrongDual ℝ E
⊢ AEMeasurable id (Measure.map (⇑L) μ)

pp: case hY
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (Measure.map (⇑L) μ)
L : StrongDual ℝ E
⊢ AEMeasurable (⇑L) μ

pp: case hφ
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (Measure.map (⇑L) μ)
L : StrongDual ℝ E
⊢ AEMeasurable (⇑L) μ

pp: case hfm
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (Measure.map (⇑L) μ)
L : StrongDual ℝ E
⊢ AEStronglyMeasurable id (Measure.map (⇑L) μ)

Tactic:
all_goals fun_prop

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

Goal state before:
pp: case pos
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ cov[fun u ↦ x * u, fun u ↦ y * u; μ] = x * y * Var[id; μ]

Tactic:
covariance_const_mul_left,

Goal state after:
case pos
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ x * cov[fun u ↦ u, fun u ↦ y * u; μ] = x * y * Var[id; μ]
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case hφ
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEMeasurable (⇑L) μ

pp: case hfm
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEStronglyMeasurable (fun z ↦ ⟪u, z - L (∫ (x : E), x ∂μ)⟫ * ⟪v, z - L (∫ (x : E), x ∂μ)⟫) (Measure.map (⇑L) μ)

Tactic:
all_goals fun_prop

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

Goal state before:
pp: 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 μ
x✝¹ x✝ : E
⊢ ¬MemLp id 2 (Measure.map (fun x ↦ c + x) μ)

Tactic:
(measurableEmbedding_addLeft _).memLp_map_measure_iff.not

Goal state after:
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 μ
x✝¹ x✝ : E
⊢ ¬MemLp (id ∘ fun x ↦ c + x) 2 μ
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
i : ι
x✝¹ : i ∈ Finset.univ
j : ι
x✝ : j ∈ Finset.univ
⊢ cov[fun ω ↦ x.ofLp i * X i ω, fun ω ↦ y.ofLp j * X j ω; μ] = x.ofLp i * y.ofLp j * cov[X i, X j; μ]

Tactic:
covariance_const_mul_left,

Goal state after:
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
i : ι
x✝¹ : i ∈ Finset.univ
j : ι
x✝ : j ∈ Finset.univ
⊢ x.ofLp i * cov[X i, fun ω ↦ y.ofLp j * X j ω; μ] = x.ofLp i * y.ofLp j * cov[X i, X j; μ]
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
⊢ charFunDual (μ.prod ν) L = cexp ((∫ (x : E × F), ↑(L x) ∂μ.prod ν) * I - ↑Var[⇑L; μ.prod ν] / 2)

Tactic:
charFunDual_prod,

Goal state after:
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
⊢ charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E F) * charFunDual ν (L ∘SL ContinuousLinearMap.inr ℝ E F) =
    cexp ((∫ (x : E × F), ↑(L x) ∂μ.prod ν) * I - ↑Var[⇑L; μ.prod ν] / 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✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ charFunDual (μ.prod μ) (L ∘SL ContinuousLinearMap.rotation θ) = charFunDual (μ.prod μ) L

Tactic:
charFunDual_prod,

Goal state after:
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)
⊢ charFunDual μ ((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E) *
      charFunDual μ ((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E) =
    charFunDual μ (L ∘SL ContinuousLinearMap.inl ℝ E E) * charFunDual μ (L ∘SL ContinuousLinearMap.inr ℝ E E)
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✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ cexp
      (-(↑Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E); μ] +
            ↑Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ]) /
        2) =
    cexp ((-↑Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + -↑Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]) / 2)

Tactic:
← neg_add

Goal state after:
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)
⊢ cexp
      (-(↑Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E); μ] +
            ↑Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ]) /
        2) =
    cexp (-(↑Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + ↑Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]) / 2)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
ha_pos : 0 < a
⊢ a / (1 - √2) < normThreshold a 0

Tactic:
by
  simp only [normThreshold_zero]
  calc a / (1 - √2)
  _ ≤ 0 := div_nonpos_of_nonneg_of_nonpos ha_pos.le (by simp)
  _ < a := ha_pos

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : c = 0
⊢ MemLp (fun x ↦ c) p μ

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
⊢ MemLp (fun x ↦ c) p μ

Tactic:
· simp [hx]

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
⊢ MemLp (fun x ↦ c) p μ
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
t : E
⊢ cexp (-∑ x, ↑⟪(stdOrthonormalBasis ℝ E) x, t⟫ ^ 2 / 2) = cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
← Finset.sum_div,

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ cexp (-((∑ i, ↑⟪(stdOrthonormalBasis ℝ E) i, t⟫ ^ 2) / 2)) = cexp (-↑‖t‖ ^ 2 / 2)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case ha
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ 0 ≤ logRatio c

pp: case hbc
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)

Tactic:
· exact (logRatio_pos hc_gt hc_lt).le

Goal state after:
case hbc
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: 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 ι))

pp: 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)

Tactic:
all_goals fun_prop

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

Goal state before:
pp: case hg
Ω : 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
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
this : IsGaussian (Measure.map X P)
⊢ AEMeasurable (⇑L) (Measure.map X P)

pp: case hf
Ω : 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
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
this : IsGaussian (Measure.map X P)
⊢ AEMeasurable X P

Tactic:
all_goals fun_prop

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

Goal state before:
pp: case hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable id (Measure.map X P)

pp: case hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable X P

pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable X P

pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEStronglyMeasurable id (Measure.map X P)

Tactic:
all_goals fun_prop

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

Goal state before:
pp: case hg
I : Finset ℝ≥0
⊢ Measurable (toLp 2)

pp: case hf
I : Finset ℝ≥0
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm

Tactic:
all_goals fun_prop

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

Goal state before:
pp: case hX
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)
t : E
⊢ AEMeasurable (fun x ↦ ⟪t, x⟫) (Measure.map X P)

pp: case hY
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)
t : E
⊢ AEMeasurable X P

pp: case hφ
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)
t : E
⊢ AEMeasurable X P

pp: case hfm
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsFiniteMeasure P
hX : AEMeasurable X P
h :
  ∀ (t : E),
    charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)
t : E
⊢ AEStronglyMeasurable (fun x ↦ ↑((fun x ↦ ⟪t, x⟫) x)) (Measure.map X P)

Tactic:
all_goals fun_prop

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

Goal state before:
pp: case hX
Ω : 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)
t : StrongDual ℝ E
⊢ AEMeasurable (⇑t) (Measure.map X P)

pp: case hY
Ω : 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)
t : StrongDual ℝ E
⊢ AEMeasurable X P

pp: case hφ
Ω : 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)
t : StrongDual ℝ E
⊢ AEMeasurable X P

pp: case hfm
Ω : 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)
t : StrongDual ℝ E
⊢ AEStronglyMeasurable (fun x ↦ ↑(t x)) (Measure.map X P)

Tactic:
all_goals fun_prop

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

Goal state before:
pp: case hg
Ω : 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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEStronglyMeasurable id (Measure.map X P)

pp: case hf
Ω : 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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEMeasurable X P

Tactic:
all_goals fun_prop

Goal state after: