mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
mF : MeasurableSpace F
inst✝¹ : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst✝ : IsGaussian μ
hL : Measurable ⇑L
⊢ IsGaussian (Measure.map (⇑L) μ)

Tactic:
refine isGaussian_of_map_eq_gaussianReal fun L' ↦ ⟨μ[L' ∘L L], Var[L' ∘L L; μ].toNNReal, ?_⟩
  rw [Measure.map_map (by fun_prop) hL, ← ContinuousLinearMap.coe_comp,
    IsGaussian.map_eq_gaussianReal]

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

Goal state before:
pp: μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂ ↔ μ₁ = μ₂ ∧ v₁ = v₂

Tactic:
by
  refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  rw [← integral_id_gaussianReal (μ := μ₁) (v := v₁),
    ← integral_id_gaussianReal (μ := μ₂) (v := v₂), h]
  simp only [integral_id_gaussianReal, true_and]
  suffices (v₁ : ℝ) = v₂ by simpa
  rw [← variance_id_gaussianReal (μ := μ₁) (v := v₁),
    ← variance_id_gaussianReal (μ := μ₂) (v := v₂), h]

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
θ c : ℝ
x : E × E
⊢ (Real.cos θ • (c • x).1 + Real.sin θ • (c • x).2, -Real.sin θ • (c • x).1 + Real.cos θ • (c • x).2) =
    (RingHom.id ℝ) c • (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2)

Tactic:
by simp [smul_comm c]

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
μ : 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); μ] / 2 +
        -↑Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ] / 2) =
    cexp (-↑Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] / 2 + -↑Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ] / 2)

Tactic:
← add_div,

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); μ] / 2 + -↑Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ] / 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)
⊢ 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); μ] / 2 + -↑Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ] / 2)

Tactic:
← add_div,

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.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
⊢ ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ

Tactic:
integrable_conv_iff (by fun_prop)

Goal state after:
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 :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
⊢ ∀ᵐ (y : E) ∂μ, Integrable (fun x ↦ rexp (C * ‖x - y‖ ^ 2)) μ
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
h : (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) = (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S))
⊢ IsGaussian (Measure.map (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) (stdGaussian (EuclideanSpace ℝ ι)))

Tactic:
rw [h, ← Measure.map_map (measurable_const_add μ) (by fun_prop)]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
h : (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) = (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S))
⊢ IsGaussian
    (Measure.map (fun x ↦ μ + x) (Measure.map (⇑(toEuclideanCLM (CFC.sqrt S))) (stdGaussian (EuclideanSpace ℝ ι))))
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:
by
  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.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : Fintype ι
E : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (fun ω x ↦ X x ω) P
⊢ HasGaussianLaw (fun ω ↦ ∑ i, X i ω) P

Tactic:
convert! hX.sum

Goal state after:
Ω : Type u_1
ι : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : Fintype ι
E : Type u_6
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X : ι → Ω → E
hX : HasGaussianLaw (fun ω x ↦ X x ω) P
x✝ : Ω
⊢ ∑ i, X i x✝ = (∑ i, X i) x✝
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: case insert.mY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s✝ : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
⊢ AEMeasurable (∑ x ∈ s, X x) P

pp: case insert.hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s✝ : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
⊢ X i ⟂ᵢ[P] ∑ x ∈ s, X x

Tactic:
· exact Finset.aemeasurable_sum s (fun i hi ↦ (mX i (mem_insert_of_mem hi)))

Goal state after:
case insert.hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s✝ : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
⊢ X i ⟂ᵢ[P] ∑ x ∈ s, X x
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝ : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) P) t = ∏ i, charFun (Measure.map (X i) P) (t.ofLp i)

Tactic:
iIndepFun_iff_map_fun_eq_pi_map hX,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝ : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ (Measure.map (fun ω i ↦ X i ω) P = Measure.pi fun i ↦ Measure.map (X i) P) ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) P) t = ∏ i, charFun (Measure.map (X i) P) (t.ofLp i)
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (L : StrongDual ℝ ((x : ι) → E x)),
      charFunDual (Measure.map (fun ω x ↦ X x ω) P) L =
        ∏ i, charFunDual (Measure.map (X i) P) (L ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
iIndepFun_iff_map_fun_eq_pi_map hX,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ (Measure.map (fun ω i ↦ X i ω) P = Measure.pi fun i ↦ Measure.map (X i) P) ↔
    ∀ (L : StrongDual ℝ ((x : ι) → E x)),
      charFunDual (Measure.map (fun ω x ↦ X x ω) P) L =
        ∏ i, charFunDual (Measure.map (X i) P) (L ∘SL ContinuousLinearMap.single ℝ E i)
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst✝⁸ : Fact (1 ≤ p)
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (Measure.map (fun ω ↦ toLp p fun x ↦ X x ω) P) L =
        ∏ i,
          charFunDual (Measure.map (X i) P)
            (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
iIndepFun_iff_map_fun_eq_pi_map hX,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst✝⁸ : Fact (1 ≤ p)
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ (Measure.map (fun ω i ↦ X i ω) P = Measure.pi fun i ↦ Measure.map (X i) P) ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (Measure.map (fun ω ↦ toLp p fun x ↦ X x ω) P) L =
        ∏ i,
          charFunDual (Measure.map (X i) P)
            (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : InnerProductSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (x y : E), cov[fun ω ↦ ⟪x, X s ω⟫, fun ω ↦ ⟪y, Y t ω⟫; P] = 0
s : S
t : T
L₁ L₂ : StrongDual ℝ E
⊢ cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0

Tactic:
by
    simpa using! h s t ((toDual ℝ E).symm L₁) ((toDual ℝ E).symm L₂)

Goal state after:
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✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
⊢ Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ'.prod μ') =
    ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ)

Tactic:
simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]

Goal state after:
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✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
hμ' : IsProbabilityMeasure μ'
⊢ ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • μ.prod μ = μ'.prod μ'

Tactic:
simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]

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

Goal state before:
pp: case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
i : ι
⊢ Integrable id (Measure.map (X i) P)

Tactic:
exact (hX1 i).isGaussian_map.integrable_id

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 : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫⁻ (b : β), ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (univ ×ˢ Iic x)

Tactic:
by
  rw [← setLIntegral_univ, setLIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]

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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
h : ∀ (a : ℚ), Measurable fun x ↦ f x a
⊢ Measurable fun t ↦ f (a, t) q

Tactic:
exact (h q).comp measurable_prodMk_left

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
law : ∀ (t : ℝ≥0), HasLaw (X t) (gaussianReal 0 t) P
incr : HasIndepIncrements X P
⊢ IsPreBrownianReal X P

Tactic:
have h0 : ∀ᵐ ω ∂P, X 0 ω = 0 := by
      apply HasLaw.ae_eq_of_dirac
      rw [← gaussianReal_zero_var]
      exact law 0
  refine IsGaussianProcess.isPreBrownianReal_of_covariance ?_ (fun t ↦ ?_) (fun s t hst ↦ ?_)
  · exact incr.isGaussianProcess (fun t ↦ (law t).hasGaussianLaw) h0
  · rw [(law t).integral_eq, integral_id_gaussianReal]
  have h1 := incr.indepFun_eval_sub zero_le hst h0
  have := (law 0).isProbabilityMeasure
  have h2 : X t = X t - X s + X s := by simp
  rw [h2, covariance_add_right, h1.covariance_eq_zero, covariance_self, (law s).variance_eq,
    variance_id_gaussianReal]
  · simp
  · exact (law s).aemeasurable
  · exact (law s).hasGaussianLaw.memLp_two
  · exact (law t).hasGaussianLaw.memLp_two.sub (law s).hasGaussianLaw.memLp_two
  · exact (law s).hasGaussianLaw.memLp_two
  · exact (law t).hasGaussianLaw.memLp_two.sub (law s).hasGaussianLaw.memLp_two
  · exact (law s).hasGaussianLaw.memLp_two

Goal state after:
Module: Mathlib.Probability.CDF

Goal state before:
pp: f : StieltjesFunction ℝ
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ cdf f.measure = f

Tactic:
by
  refine (cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0
  have h_prob : IsProbabilityMeasure f.measure :=
    ⟨by rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]⟩
  exact measure_cdf f.measure

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 : Set ℝ
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)

Tactic:
induction t, ht
    using MeasurableSpace.induction_on_inter (borel_eq_generateFrom_Iic ℝ) isPiSystem_Iic with
  | empty => simp only [measure_empty, lintegral_const, zero_mul, prod_empty]
  | basic t ht =>
    obtain ⟨q, rfl⟩ := ht
    exact setLIntegral_toKernel_Iic hf a _ hs
  | compl t ht iht =>
    calc ∫⁻ b in s, hf.toKernel f (a, b) tᶜ ∂(ν a)
      = ∫⁻ b in s, hf.toKernel f (a, b) univ - hf.toKernel f (a, b) t ∂(ν a) := by
          congr with x; rw [measure_compl ht (measure_ne_top (hf.toKernel f (a, x)) _)]
    _ = ∫⁻ b in s, hf.toKernel f (a, b) univ ∂(ν a)
          - ∫⁻ b in s, hf.toKernel f (a, b) t ∂(ν a) := by
        rw [lintegral_sub]
        · exact (Kernel.measurable_coe (hf.toKernel f) ht).comp measurable_prodMk_left
        · rw [iht]
          exact measure_ne_top _ _
        · exact Eventually.of_forall fun a ↦ measure_mono (subset_univ _)
    _ = κ a (s ×ˢ univ) - κ a (s ×ˢ t) := by
        rw [setLIntegral_toKernel_univ hf a hs, iht]
    _ = κ a (s ×ˢ tᶜ) := by
        rw [← measure_sdiff _ (hs.prod ht).nullMeasurableSet (measure_ne_top _ _)]
        · rw [prod_sdiff_prod, compl_eq_univ_sdiff]
          simp only [sdiff_self, empty_prod, union_empty]
        · rw [prod_subset_prod_iff]
          exact Or.inl ⟨subset_rfl, subset_univ t⟩
  | iUnion f hf_disj hf_meas ihf =>
    simp_rw [measure_iUnion hf_disj hf_meas]
    rw [lintegral_tsum, prod_iUnion, measure_iUnion]
    · simp_rw [ihf]
    · exact hf_disj.mono fun i j h ↦ h.set_prod_right _ _
    · exact fun i ↦ MeasurableSet.prod hs (hf_meas i)
    · exact fun i ↦
        ((Kernel.measurable_coe _ (hf_meas i)).comp measurable_prodMk_left).aemeasurable.restrict

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 (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' f' i) ∂ν a = (κ a) (f' i)
h_eq : ∀ (a : β), Prod.mk a ⁻¹' ⋃ i, f' i = ⋃ i, Prod.mk a ⁻¹' f' i
h_disj : ∀ (a : β), Pairwise (Disjoint on fun i ↦ Prod.mk a ⁻¹' f' i)
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ i, Prod.mk b ⁻¹' f' i) ∂ν a =
    ∫⁻ (b : β), ∑' (i : ℕ), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' f' i) ∂ν a

Tactic:
by
          congr with x : 1
          rw [measure_iUnion (h_disj x) fun i ↦ measurable_prodMk_left (hf_meas i)]

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

Goal state before:
pp: case h.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ (⇑L ∘ X) ⟂ᵢ[P] ⇑L ∘ (Y - X)

Tactic:
exact h.comp (by fun_prop) (by fun_prop)

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 α γ
hκν : κ.fst ≤ ν
a : α
s : Set β
⊢ eLpNorm (fun x ↦ κ.density ν a x s) 1 (ν a) ≤ (ν a) univ

Tactic:
refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun t ↦ ?_))).trans ?_
  · simp only [Real.norm_eq_abs, abs_of_nonneg (density_nonneg hκν a t s),
      density_le_one hκν a t s]
  · simp

Goal state after: