mathlib-initiative/mathlib-tactics huggingface dataset:
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 μ') = μ'.prod μ'

Tactic:
by

Goal state after:
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
i : S
⊢ ∀ (i_1 : T i), univ ∈ {s | MeasurableSet s}

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁶ : LinearOrder T
inst✝⁵ : Bot T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
X : T → Ω → E
h : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
I : Finset T
⊢ (fun ω ↦ I.restrict fun x ↦ X x ω) =ᵐ[P]
    ⇑(incrementsToRestrict R I) ∘ fun ω i ↦
      X (I.orderEmbOfFinWithBot i.succ) ω - X (I.orderEmbOfFinWithBot i.castSucc) ω

Tactic:
by

Goal state after:
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
i : S
⊢ MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)

Tactic:
by

Goal state after:
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
⊢ ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) =
    ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : LinearOrder T
inst✝⁶ : OrderBot T
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
⊢ HasGaussianLaw (fun ω ↦ I.restrict fun x ↦ X x ω) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
C : ℝ≥0 → Ω → ℝ
hB : IsPreBrownianReal B P
h : ∀ (t : ℝ≥0), B t =ᵐ[P] C t
I : Finset ℝ≥0
⊢ HasLaw (fun ω ↦ I.restrict fun x ↦ C x ω) (projectiveFamily I) P

Tactic:
by

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
t : ℝ≥0
⊢ t ∈ {t}

Tactic:
by

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
⊢ ∀ᵐ (ω : Ω) ∂P, B 0 ω = 0

Tactic:
by

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
s t : ℝ≥0
⊢ s ∈ {s, t}

Tactic:
by

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
s t : ℝ≥0
⊢ t ∈ {s, t}

Tactic:
by

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
t : ℝ≥0
⊢ ∫ (x : Ω), B t x ∂P = 0

Tactic:
(hB.hasLaw_eval t).integral_eq,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t : ℝ≥0
⊢ ∫ (x : ℝ), x ∂gaussianReal 0 t = 0
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t : ℝ≥0
⊢ ∫ (x : Ω), B t x ∂P = 0

Tactic:
by

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
s t : ℝ≥0
x : ↥{s, t} → ℝ
⊢ t ∈ {s, t}

Tactic:
by

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 μ
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
x y z : StrongDual ℝ ((i : ι) → E i)
⊢ ∑ i, ((L i) ((x + y) ∘SL single ℝ E i)) (z ∘SL single ℝ E i) =
    ∑ i, ((L i) (x ∘SL single ℝ E i)) (z ∘SL single ℝ E i) + ∑ i, ((L i) (y ∘SL single ℝ E i)) (z ∘SL single ℝ E i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable fun a ↦ ↑(f a) q
hf_bot : ∀ (a : α), Tendsto (↑(f a)) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a)) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (f a).measure
⊢ ∀ s ∈ range Iic, Measurable fun a ↦ (f a).measure s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint (fun p ↦ f p.2) ((), a) ↔ IsRatStieltjesPoint f a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet {a | Monotone (f a)}

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
c : ℝ
m n : StrongDual ℝ ((i : ι) → E i)
⊢ ∑ i, ((L i) ((c • m) ∘SL single ℝ E i)) (n ∘SL single ℝ E i) =
    c • ∑ i, ((L i) (m ∘SL single ℝ E i)) (n ∘SL single ℝ E i)

Tactic:
by

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
s t : ℝ≥0
⊢ Measurable (Function.eval ⟨s, ⋯⟩)

Tactic:
by

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
s t : ℝ≥0
⊢ Measurable fun x ↦ x ⟨t, ⋯⟩

Tactic:
by

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
s t : ℝ≥0
⊢ cov[B s, B t; P] = ↑(min s t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
⊢ MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
x y z : StrongDual ℝ ((i : ι) → E i)
⊢ ∑ i, ((L i) (x ∘SL single ℝ E i)) ((y + z) ∘SL single ℝ E i) =
    ∑ i, ((L i) (x ∘SL single ℝ E i)) (y ∘SL single ℝ E i) + ∑ i, ((L i) (x ∘SL single ℝ E i)) (z ∘SL single ℝ E i)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
c : ℝ
m n : StrongDual ℝ ((i : ι) → E i)
⊢ ∑ i, ((L i) (m ∘SL single ℝ E i)) ((c • n) ∘SL single ℝ E i) =
    c • ∑ i, ((L i) (m ∘SL single ℝ E i)) (n ∘SL single ℝ E i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
h4 : MeasurableSet {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
this :
  {a | IsRatStieltjesPoint f a} =
    {a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
      {a | ∀ (t : ℚ), ⨅ r, f a ↑r = f a t}
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet {a | IsRatStieltjesPoint f a}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Monotone (if p a then f a else g a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Tendsto (if p a then f a else g a) atTop (𝓝 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ Tendsto (if p a then f a else g a) atBot (𝓝 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
⊢ ∀ (t : ℚ), ⨅ r, (if p a then f a else g a) ↑r = (if p a then f a else g a) t

Tactic:
by

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

Goal state before:
pp: ⊢ Monotone defaultRatCDF

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ 0 ≤ defaultRatCDF q

Tactic:
by

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

Goal state before:
pp: q : ℚ
⊢ defaultRatCDF q ≤ 1

Tactic:
by

Goal state after:
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
⊢ iIndepFun (fun i ω j ↦ X i j ω) κ P

Tactic:
by

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

Goal state before:
pp: ⊢ Tendsto defaultRatCDF atTop (𝓝 1)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L✝ L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
g : LinearMap.BilinForm ℝ (StrongDual ℝ ((i : ι) → E i)) :=
  LinearMap.mk₂ ℝ (fun x y ↦ ∑ i, ((L i) (x ∘SL single ℝ E i)) (y ∘SL single ℝ E i)) ⋯ ⋯ ⋯ ⋯
⊢ ∀ (x y : StrongDual ℝ ((i : ι) → E i)), ‖(g x) y‖ ≤ (∑ i, ‖L i‖) * ‖x‖ * ‖y‖

Tactic:
by

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

Goal state before:
pp: t : ℚ
⊢ BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)

Tactic:
by

Goal state after:
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 α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑κ ∘ₘ P)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
⊢ iIndepFun (fun i ω j ↦ X i j ω) κ P

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : (fun ω i ↦ X i ω) ⟂ᵢ[P] Y
h2 : ∀ (i : S), X i =ᵐ[P] X' i
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : Y ⟂ᵢ[P] fun ω i ↦ X i ω
h2 : ∀ (i : S), X i =ᵐ[P] X' i
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
by

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

Goal state before:
pp: t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
⊢ t < t / 2

Tactic:
by

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

Goal state before:
pp: t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
⊢ t / 2 < 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x y : StrongDual ℝ ((i : ι) → E i)
⊢ ((diagonalStrongDualPi L).toBilinForm x) y = ((diagonalStrongDualPi L).toBilinForm y) x

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : T → Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : (j : T) → MeasurableSpace (𝓨 j)
X X' : (i : S) → Ω → 𝓧 i
Y Y' : (j : T) → Ω → 𝓨 j
hXY : (fun ω i ↦ X i ω) ⟂ᵢ[P] fun ω j ↦ Y j ω
hX : ∀ (i : S), X i =ᵐ[P] X' i
hY : ∀ (j : T), Y j =ᵐ[P] Y' j
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : T → Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : (j : T) → MeasurableSpace (𝓨 j)
X X' : (i : S) → Ω → 𝓧 i
Y Y' : (j : T) → Ω → 𝓨 j
hXY : (fun ω i ↦ X i ω) ⟂ᵢ[P] fun ω j ↦ Y j ω
hX : ∀ (i : S), X i =ᵐ[P] X' i
hY : ∀ (j : T), Y j =ᵐ[P] Y' j
⊢ ∀ (j : T), ∀ᵐ (a : Unit) ∂Measure.dirac (), Y j =ᵐ[(Kernel.const Unit P) a] Y' j

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) P
hY : AEMeasurable Y P
h : ∀ (I : Finset S), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] Y
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (X i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by

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

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x : StrongDual ℝ ((i : ι) → E i)
⊢ 0 ≤ ((diagonalStrongDualPi L).toBilinForm x) x

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) P
hY : AEMeasurable Y P
h : ∀ (I : Finset S), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] Y
inst✝ : IsZeroOrProbabilityMeasure P
⊢ AEMeasurable Y (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
inst✝² : MeasurableSpace 𝓧
inst✝¹ : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable X P
hY : ∀ (i : S), AEMeasurable (Y i) P
h : ∀ (I : Finset S), X ⟂ᵢ[P] fun ω i ↦ Y (↑i) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ AEMeasurable X (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
inst✝² : MeasurableSpace 𝓧
inst✝¹ : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable X P
hY : ∀ (i : S), AEMeasurable (Y i) P
h : ∀ (I : Finset S), X ⟂ᵢ[P] fun ω i ↦ Y (↑i) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (Y i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) P
hY : ∀ (j : T), AEMeasurable (Y j) P
h : ∀ (I : Finset S) (J : Finset T), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] fun ω j ↦ Y (↑j) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (X i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) P
hY : ∀ (j : T), AEMeasurable (Y j) P
h : ∀ (I : Finset S) (J : Finset T), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] fun ω j ↦ Y (↑j) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (j : T), AEMeasurable (Y j) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : S → Type u_4
𝓧 : (i : S) → T i → Type u_5
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) P
h2 : ∀ (i : S) (j : T i), X i j =ᵐ[P] X' i j
⊢ ∀ (i : S) (j : T i), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i j =ᵐ[(Kernel.const Unit P) a] X' i j

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
L₁✝ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂✝ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ
x y z : StrongDual ℝ (E × F)
⊢ (L₁ ((x + y) ∘SL inl ℝ E F)) (z ∘SL inl ℝ E F) + (L₂ ((x + y) ∘SL inr ℝ E F)) (z ∘SL inr ℝ E F) =
    (L₁ (x ∘SL inl ℝ E F)) (z ∘SL inl ℝ E F) + (L₂ (x ∘SL inr ℝ E F)) (z ∘SL inr ℝ E F) +
      ((L₁ (y ∘SL inl ℝ E F)) (z ∘SL inl ℝ E F) + (L₂ (y ∘SL inr ℝ E F)) (z ∘SL inr ℝ E F))

Tactic:
by

Goal state after: