mathlib-initiative/mathlib-tactics huggingface dataset:
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]

Goal state after:
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)
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : 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 ω) • NormedSpace.exp (ε • ↑(X ω)) = NormedSpace.exp (ε • ↑(X ω)) * ↑(X ω)

Tactic:
smul_eq_mul,

Goal state after:
Ω : 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 ω) * NormedSpace.exp (ε • ↑(X ω)) = NormedSpace.exp (ε • ↑(X ω)) * ↑(X ω)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
t : ℝ
⊢ charFun (gaussianReal μ v) t = cexp (↑t * ↑μ * I - ↑↑v * ↑t ^ 2 / 2)

Tactic:
rw [← complexMGF_id_mul_I, complexMGF_id_gaussianReal]
  congr
  simp only [mul_pow, I_sq, mul_neg, mul_one, sub_eq_add_neg]
  ring_nf

Goal state after:
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
L' : F →L[ℝ] ℝ
⊢ Measure.map (⇑L') (Measure.map (⇑L) μ) = gaussianReal (∫ (x : E), (L' ∘SL L) x ∂μ) Var[⇑(L' ∘SL L); μ].toNNReal

Tactic:
rw [Measure.map_map (by fun_prop) hL, ← ContinuousLinearMap.coe_comp,
    IsGaussian.map_eq_gaussianReal]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ ((covarianceBilin μ) x) y = cov[fun u ↦ ⟪x, u⟫, fun u ↦ ⟪y, u⟫; μ]

Tactic:
rw [covarianceBilin_eq_covarianceBilinDual, covarianceBilinDual_eq_covariance h]
  rfl

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

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
t : E
⊢ cexp ((∫ (x : E), ↑(((toDualMap ℝ E) t) x) ∂μ) * I - ↑Var[⇑((toDualMap ℝ E) t); μ] / 2) =
    cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)

Tactic:
simp [toDualMap]

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

Goal state before:
pp: case hf
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ Integrable (fun y ↦ ⟪x, y⟫ • y) μ

Tactic:
exact memLp_one_iff_integrable.1 <| hμ.smul (hμ.const_inner x)

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ = ‖∫ (x : E), L₁ x * L₂ x ∂μ‖

Tactic:
by rw [uncenteredCovarianceBilinDual_apply h]

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

Goal state before:
pp: c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ logRatio c ≤ logRatio d

Tactic:
unfold logRatio

Goal state after:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ Real.log (c.toReal / (1 - c).toReal) / (8 * (1 + √2) ^ 2) ≤ Real.log (d.toReal / (1 - d).toReal) / (8 * (1 + √2) ^ 2)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ logRatio c * (a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)) * a⁻¹ ^ 2 = 2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n

Tactic:
unfold logRatio

Goal state after:
a : ℝ
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
n : ℕ
ha : ¬a = 0
⊢ Real.log (c.toReal / (1 - c).toReal) / (8 * (1 + √2) ^ 2) * (a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)) * a⁻¹ ^ 2 =
    2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
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_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ μ (closedBall 0 a)ᶜ = 0

Tactic:
change μ {x | ¬ x ∈ closedBall 0 a} = 0

Goal state after:
case pos
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_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ μ {x | x ∉ closedBall 0 a} = 0
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : NormedSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∏ i, charFunDual (Measure.map (fun p ↦ p i) (Measure.pi μ)) = ∏ i, charFunDual (μ i)

pp: case mX
ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : NormedSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∀ (i : ι), AEMeasurable (fun p ↦ p i) (Measure.pi μ)

pp: case hX
ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : NormedSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ iIndepFun (fun i p ↦ p i) (Measure.pi μ)

Tactic:
· refine Finset.prod_congr rfl fun i _ ↦ ?_
    rw [(measurePreserving_eval μ i).map_eq]

Goal state after:
case mX
ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : NormedSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ ∀ (i : ι), AEMeasurable (fun p ↦ p i) (Measure.pi μ)

case hX
ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : NormedSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ iIndepFun (fun i p ↦ p i) (Measure.pi μ)
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 X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f i
h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, (fun ω j ↦ X' i j ω) ⁻¹' g i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
h3'

Goal state after:
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 X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f i
h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, (fun ω j ↦ X' i j ω) ⁻¹' g i) = ∏ x ∈ s, (κ a) ((fun ω j ↦ X' x j ω) ⁻¹' g x)
Module: Mathlib.Probability.BrownianMotion.Basic

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

Tactic:
simp_rw [← this j i hij.symm (by grind), min_comm]
      grind

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ Tendsto (fun i ↦ ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 ((ν a).real univ • 1))

Tactic:
smul_eq_mul,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ Tendsto (fun i ↦ ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 ((ν a).real univ * 1))
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ Tendsto (fun i ↦ ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 ((ν a).real univ))

Tactic:
exact hf.tendsto_integral_of_monotone a seq hseq hseq_tendsto

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ q a ≤ ENNReal.ofReal 1

Tactic:
simp [ha]

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

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
t : ℝ≥0
⊢ (√↑c)⁻¹ * ∫ (a : Ω), B (c * t) a ∂P = 0

Tactic:
hB.integral_eval,

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
t : ℝ≥0
⊢ (√↑c)⁻¹ * 0 = 0
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ ∫ (a : Ω), B (t₀ + t) a ∂P - ∫ (a : Ω), B t₀ a ∂P = 0

pp: case refine_1.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B (t₀ + t)) P

pp: case refine_1.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B t₀) P

Tactic:
hB.integral_eval,

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ 0 - ∫ (a : Ω), B t₀ a ∂P = 0

case refine_1.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B (t₀ + t)) P

case refine_1.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B t₀) P
Module: Mathlib.Probability.BrownianMotion.Basic

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

pp: case refine_1.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B (t₀ + t)) P

pp: case refine_1.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B t₀) P

Tactic:
hB.integral_eval,

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ 0 - 0 = 0

case refine_1.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B (t₀ + t)) P

case refine_1.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ t : ℝ≥0
⊢ Integrable (B t₀) P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t : ℝ≥0
⊢ ↑t * ∫ (a : Ω), B (1 / t) a ∂P = 0

Tactic:
hB.integral_eval,

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t : ℝ≥0
⊢ ↑t * 0 = 0
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf)) ω) s =
    ((ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf)) ω) s

Tactic:
prod_apply' _ _ _ hs,

Goal state after:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ((ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf)) ω) s =
    ∫⁻ (b : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s) ∂(ξ ∘ₖ (κ ×ₖ deterministic f hf)) ω
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ((ξ ×ₖ prodMkLeft β η) (b, f ω)) s = ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (b, f ω)

Tactic:
prod_apply' _ _ _ hs,

Goal state after:
case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ∫⁻ (b_1 : δ), ((prodMkLeft β η) (b, f ω)) (Prod.mk b_1 ⁻¹' s) ∂ξ (b, f ω) =
    ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (b, f ω)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ)) ω) s =
    ((ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf)) ω) s

Tactic:
prod_apply' _ _ _ hs,

Goal state after:
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
⊢ ((ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ)) ω) s =
    ∫⁻ (b : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk b ⁻¹' s) ∂(ξ ∘ₖ (deterministic f hf ×ₖ κ)) ω
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ((ξ ×ₖ prodMkRight β η) (f ω, b)) s = ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (f ω, b)

Tactic:
prod_apply' _ _ _ hs,

Goal state after:
case e_f
β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ∫⁻ (b_1 : δ), ((prodMkRight β η) (f ω, b)) (Prod.mk b_1 ⁻¹' s) ∂ξ (f ω, b) =
    ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (f ω, b)
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 ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ κ.densityProcess ν n a x s ≤ 1

Tactic:
refine ENNReal.toReal_le_of_le_ofReal zero_le_one (ENNReal.div_le_of_le_mul ?_)
  rw [ENNReal.ofReal_one, one_mul]
  exact meas_countablePartitionSet_le_of_fst_le hκν n a x s

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

Goal state before:
pp: case h.hY
Ω : 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
⊢ MemLp (⇑L ∘ (Y - X)) 2 P

Tactic:
rw [map_comp_sub]

Goal state after:
case h.hY
Ω : 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
⊢ MemLp (⇑L ∘ Y - ⇑L ∘ X) 2 P
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case h.hg
Ω : 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
⊢ Integrable (⇑L ∘ (Y - X)) P

Tactic:
rw [map_comp_sub]

Goal state after:
case h.hg
Ω : 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
⊢ Integrable (⇑L ∘ Y - ⇑L ∘ X) P
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ 0 ≤ ∫ (a : Ω), ‖f (x, a)‖ ∂ρ.condKernel x

Tactic:
exact integral_nonneg_of_ae (Filter.Eventually.of_forall fun y ↦ norm_nonneg _)

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
⊢ Measurable
    ⇑{ toFun := fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
        invFun := fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }

Tactic:
by
    refine measurable_pi_lambda _ (fun x ↦ ?_)
    by_cases h : x ≤ a
    · simpa [h] using measurable_fst.eval
    · simpa [h] using measurable_snd.eval

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h :
  (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[Measure.map Prod.fst ((Kernel.const α ρ) a)]
    ⇑((Kernel.const α ρ) a).condKernel
⊢ (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel

Tactic:
Kernel.const_apply

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h : (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[Measure.map Prod.fst ρ] ⇑ρ.condKernel
⊢ (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[ρ.fst] ⇑ρ.condKernel