mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
by_cases h_Lp : MemLp id p μ

Goal state after:
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal

case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : ¬MemLp id p μ
⊢ ‖(toLpₗ μ p) L‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal
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 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[(fun u ↦ ⟪(basisFun ι ℝ) i, u⟫) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω,
      (fun u ↦ ⟪(basisFun ι ℝ) j, u⟫) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω; μ] =
    cov[X i, X j; μ]

pp: case hX
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪(basisFun ι ℝ) i, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

pp: case hY
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪(basisFun ι ℝ) j, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

pp: case hZ
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

pp: case h
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp id 2 (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

Tactic:
· simp [basisFun_inner]; rfl

Goal state after:
case hX
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪(basisFun ι ℝ) i, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

case hY
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEStronglyMeasurable (fun u ↦ ⟪(basisFun ι ℝ) j, u⟫) (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)

case hZ
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ AEMeasurable (fun ω ↦ toLp 2 fun x ↦ X x ω) μ

case h
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ MemLp id 2 (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) μ)
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
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ((uncenteredCovarianceBilinDual μ) L₁) L₂ = ∫ (x : E), L₁ x * L₂ x ∂μ

Tactic:
by
  simp only [uncenteredCovarianceBilinDual, ContinuousLinearMap.bilinearComp_apply,
    StrongDual.toLp_apply h, L2.inner_def, RCLike.inner_apply, conj_trivial]
  refine integral_congr_ae ?_
  filter_upwards [MemLp.coeFn_toLp (h.continuousLinearMap_comp L₁),
    MemLp.coeFn_toLp (h.continuousLinearMap_comp L₂)] with x hxL₁ hxL₂
  simp only [id_eq] at hxL₁ hxL₂
  rw [hxL₁, hxL₂, mul_comm]

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✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ((covarianceBilinDual μ) L₁) L₂ = ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ

Tactic:
rw [covarianceBilinDual, uncenteredCovarianceBilinDual_apply,
    integral_map (by fun_prop) (by fun_prop)]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝³ : NormedSpace ℝ E
inst✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ∫ (x : E), L₁ (x - ∫ (x : E), x ∂μ) * L₂ (x - ∫ (x : E), x ∂μ) ∂μ =
    ∫ (x : E), (L₁ x - ∫ (x : E), L₁ x ∂μ) * (L₂ x - ∫ (x : E), L₂ x ∂μ) ∂μ

case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝³ : NormedSpace ℝ E
inst✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ MemLp id 2 (Measure.map (fun x ↦ x - ∫ (x : E), x ∂μ) μ)
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✝² : BorelSpace E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L₁ L₂ : StrongDual ℝ E
⊢ ((covarianceBilinDual μ) L₁) L₂ = cov[⇑L₁, ⇑L₂; μ]

Tactic:
by
  rw [covarianceBilinDual_apply h, covariance]

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᵐ[P] Y
⊢ IsGaussian (Measure.map Y P)

Tactic:
by
    rw [← Measure.map_congr h]
    exact hX.isGaussian_map

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Finset ℝ≥0
f : (↥I → ℝ) → E
⊢ ∫ (x : ↥I → ℝ), f x ∂projectiveFamily I = ∫ (x : EuclideanSpace ℝ ↥I), f x.ofLp ∂multivariateGaussian 0 (covMatrix I)

Tactic:
simp [projectiveFamily, integral_map_equiv]

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

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
hst : ↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * ↑s = max (↑s - ↑t) (↑t - ↑s)

Tactic:
max_eq_right (by grw [hst]),

Goal state after:
I : Finset ℝ≥0
s t : ↥I
hst : ↑s ≤ ↑t
⊢ ↑s + ↑t - 2 * ↑s = ↑t - ↑s
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)

Tactic:
exact (IsGaussian.hasGaussianLaw_id.eval s).integrable

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 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
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
have h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i := (biInf_congr hg).symm

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
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
a : ℝ
h_of_pos : ∀ (a' : ℝ), 0 < a' → μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹
ha : a ≤ 0
⊢ μ {x | ‖x‖ ≤ a} ≤ 2⁻¹

pp: case inr
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
a : ℝ
h_of_pos : ∀ (a' : ℝ), 0 < a' → μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹
ha : 0 < a
⊢ μ {x | ‖x‖ ≤ a} ≤ 2⁻¹

Tactic:
· calc μ {x | ‖x‖ ≤ a}
        _ ≤ μ {x | ‖x‖ ≤ 1} := measure_mono fun x hx ↦ hx.trans (ha.trans (by positivity))
        _ ≤ 2⁻¹ := h_of_pos _ (by positivity)

Goal state after:
case inr
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
a : ℝ
h_of_pos : ∀ (a' : ℝ), 0 < a' → μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹
ha : 0 < a
⊢ μ {x | ‖x‖ ≤ a} ≤ 2⁻¹
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:
split_ifs with h; exacts [(hf h).tendsto_atTop_one, (hg h).tendsto_atTop_one]

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

Goal state before:
pp: case pos
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : t < 0
⊢ (⨅ r, if ↑r < 0 then 0 else 1) = 0

Tactic:
refine le_antisymm ?_ (le_ciInf fun x ↦ ?_)
    · obtain ⟨q, htq, hq_neg⟩ : ∃ q, t < q ∧ q < 0 := ⟨t / 2, by linarith, by linarith⟩
      refine (ciInf_le h_bdd ⟨q, htq⟩).trans ?_
      rw [if_pos]
      rwa [Subtype.coe_mk]
    · split_ifs
      exacts [le_rfl, zero_le_one]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ ρ (s ×ˢ ∅) = 0

Tactic:
simp only [prod_empty, measure_empty]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst✝ : IsFiniteMeasure ρ
⊢ ∫⁻ (x : α), preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) univ

Tactic:
by
  rw [← setLIntegral_univ, setLIntegral_preCDF_fst ρ r MeasurableSet.univ]

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
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ (fun ω t ↦ B (t₀ + t) ω - B t₀ ω) ⟂ᵢ[P] fun ω t ↦ B (↑t) ω

Tactic:
apply IsGaussianProcess.indepFun_of_covariance_eq_zero

Goal state after:
case hXY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ IsGaussianProcess (Sum.elim (fun s ω ↦ B (t₀ + s) ω - B t₀ ω) fun t ↦ B ↑t) P

case mX
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0), AEMeasurable (fun ω ↦ B (t₀ + s) ω - B t₀ ω) P

case mY
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (t : ↑(Set.Iic t₀)), AEMeasurable (B ↑t) P

case h
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
⊢ ∀ (s : ℝ≥0) (t : ↑(Set.Iic t₀)), cov[fun ω ↦ B (t₀ + s) ω - B t₀ ω, B ↑t; P] = 0
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_3.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
hst : s ≤ t
this✝ : IsProbabilityMeasure P
hs : s ≠ 0
this : 0 < t
⊢ ↑s * (↑t * ↑(min (1 / s) (1 / t))) = ↑s

Tactic:
rw [min_eq_right]

Goal state after:
case refine_3.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
hst : s ≤ t
this✝ : IsProbabilityMeasure P
hs : s ≠ 0
this : 0 < t
⊢ ↑s * (↑t * ↑(1 / t)) = ↑s

case refine_3.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
hst : s ≤ t
this✝ : IsProbabilityMeasure P
hs : s ≠ 0
this : 0 < t
⊢ 1 / t ≤ 1 / s
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
⊢ IsPreBrownianReal (fun t ω ↦ ↑t * B (1 / t) ω) P

Tactic:
by
  refine IsGaussianProcess.isPreBrownianReal_of_covariance ?_ (fun t ↦ ?_) (fun s t hst ↦ ?_)
  · exact (IsGaussianProcess.comp_right hB.isGaussianProcess _).smul _
  · rw [integral_const_mul, hB.integral_eval, mul_zero]
  · have := hB.isGaussianProcess.isProbabilityMeasure
    rw [covariance_const_mul_left, covariance_const_mul_right, hB.covariance_eval]
    obtain rfl | hs := eq_or_ne s 0
    · simp
    have : 0 < t := (pos_of_ne_zero hs).trans_le hst
    rw [min_eq_right]
    · norm_cast
      field_simp
    exact one_div_le_one_div_of_le (pos_of_ne_zero hs) hst

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
n : ℕ
x✝ : Ω
⊢ ∫ (x : Ω), X 0 x ∂P = ∫ (x : Ω), X n x ∂P

Tactic:
rw [(hident n).integral_eq]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ μ ⊗ₘ κ = μ ⊗ₘ (η ∘ₖ κ)

Tactic:
by
  by_cases hμ : SFinite μ
  swap; · simp [hμ]
  rw [Measure.compProd_eq_comp_prod, Measure.compProd_eq_comp_prod, Measure.comp_assoc,
    Kernel.parallelComp_comp_prod, Kernel.id_comp]

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

Goal state before:
pp: case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
⊢ ∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ ≤ 1

Tactic:
rw [ae_le_const_iff_forall_gt_measure_zero]
    intro r hr
    let s := {b | r ≤ κCond (a, b) Set.univ}
    have hs : MeasurableSet s := h_meas measurableSet_Ici
    have h_2_le : s.indicator (fun _ ↦ r) ≤ s.indicator (fun b ↦ (κCond (a, b)) Set.univ) := by
      intro b
      by_cases hbs : b ∈ s
      · simpa [hbs]
      · simp [hbs]
    have : ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) ≤ κ.fst a s :=
      (lintegral_mono h_2_le).trans_eq (h_eq s hs)
    rw [lintegral_indicator_const hs] at this
    contrapose! this with h_ne_zero
    conv_lhs => rw [← one_mul (κ.fst a s)]
    gcongr
    finiteness

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 α γ
n : ℕ
a : α
x : γ
⊢ κ.densityProcess ν n a x ∅ = 0

Tactic:
simp [densityProcess]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
hxuniv : (κ x) univ = (ρ.condKernel x) univ
t : Set ℝ
ht : MeasurableSet t
heq : (κ x) t = (ρ.condKernel x) t
⊢ (κ x) univ - (κ x) t = (ρ.condKernel x) tᶜ

Tactic:
heq,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
hxuniv : (κ x) univ = (ρ.condKernel x) univ
t : Set ℝ
ht : MeasurableSet t
heq : (κ x) t = (ρ.condKernel x) t
⊢ (κ x) univ - (ρ.condKernel x) t = (ρ.condKernel x) tᶜ
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae : ∀ᵐ (t : β) ∂κ.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}
⊢ (fun b ↦ ((borelMarkovFromReal Ω η) (a, b)) (Prod.mk b ⁻¹' t)) =ᵐ[κ.fst a] fun b ↦
    ((η.comapRight he) (a, b)) (Prod.mk b ⁻¹' t)

Tactic:
filter_upwards [h_ae] with a ha

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a✝ : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae : ∀ᵐ (t : β) ∂κ.fst a✝, (a✝, t) ∈ {p | (η p) (range e)ᶜ = 0}
a : β
ha : (η (a✝, a)) (range e)ᶜ = 0
⊢ ((borelMarkovFromReal Ω η) (a✝, a)) (Prod.mk a ⁻¹' t) = ((η.comapRight he) (a✝, a)) (Prod.mk a ⁻¹' t)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Measure.map X μ = (Measure.map (fun x ↦ (X x, Y x)) μ).fst
⊢ ⇑(condDistrib Y X μ) =ᵐ[Measure.map X μ] ⇑κ

Tactic:
heq,

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
hX : Measurable X
hY : Measurable Y
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
heq : Measure.map X μ = (Measure.map (fun x ↦ (X x, Y x)) μ).fst
⊢ ⇑(condDistrib Y X μ) =ᵐ[(Measure.map (fun x ↦ (X x, Y x)) μ).fst] ⇑κ
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 ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
⊢ ∫ (x : γ) in A, κ.density ν a x s ∂ν a = (κ a).real (A ×ˢ s)

Tactic:
by
  have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
  have hgen : ‹MeasurableSpace γ› =
      .generateFrom {s | ∃ n, MeasurableSet[countableFiltration γ n] s} := by
    rw [ofPred_exists, generateFrom_iUnion_measurableSet (countableFiltration γ),
      iSup_countableFiltration]
  have hpi : IsPiSystem {s | ∃ n, MeasurableSet[countableFiltration γ n] s} := by
    rw [ofPred_exists]
    exact isPiSystem_iUnion_of_monotone _
      (fun n ↦ @isPiSystem_measurableSet _ (countableFiltration γ n))
      fun _ _ ↦ (countableFiltration γ).mono
  induction A, hA using induction_on_inter hgen hpi with
  | empty => simp
  | basic s hs =>
    rcases hs with ⟨n, hn⟩
    exact setIntegral_density_of_measurableSet hκν n a hs hn
  | compl A hA hA_eq =>
    have h := integral_add_compl hA (integrable_density hκν a hs)
    rw [hA_eq, integral_density hκν a hs] at h
    have : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s := by
      rw [prod_sdiff_prod, compl_eq_univ_sdiff]
      simp
    rw [this, measureReal_def,
      measure_sdiff (by intro; simp) (hA.prod hs).nullMeasurableSet (measure_ne_top (κ a) _),
      ENNReal.toReal_sub_of_le (measure_mono (by intro x; simp)) (measure_ne_top _ _)]
    rw [eq_tsub_iff_add_eq_of_le, add_comm]
    · exact h
    · gcongr <;> simp
  | iUnion f hf_disj hf h_eq =>
    rw [integral_iUnion hf hf_disj (integrable_density hκν _ hs).integrableOn]
    simp_rw [h_eq, measureReal_def]
    rw [← ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]
    congr
    rw [iUnion_prod_const, measure_iUnion]
    · exact hf_disj.mono fun _ _ h ↦ h.set_prod_left _ _
    · exact fun i ↦ (hf i).prod hs

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
f✝ : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b ↦ ∫⁻ (a : β) in s, f b a ∂κ b

Tactic:
exact hf.setLIntegral_kernel_prod_right hs

Goal state after: