mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case neg
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
h_zero : ¬WithTop.untopA (min (↑i) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
⊢ f (k + 1) ω - r ≤ ↑R

Tactic:
have := notMem_of_lt_hittingAfter (?_ : k < leastGE f r ω)

Goal state after:
case neg.refine_2
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
h_zero : ¬WithTop.untopA (min (↑i) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
this : ⊥ ≤ ↑k → f (↑k) ω ∉ Set.Ici r
⊢ f (k + 1) ω - r ≤ ↑R

case neg.refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
ω : Ω
hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
h_zero : ¬WithTop.untopA (min (↑i) (leastGE f r ω)) = 0
k : ℕ
hk : WithTop.untopA (min (↑i) (leastGE f r ω)) = k + 1
⊢ ↑k < leastGE f r ω
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
h_integral : Continuous fun f ↦ ∫ (x : Ω), ↑↑↑f x ∂μ
⊢ Continuous fun f ↦ ∫ (x : Ω) in s, ↑↑↑f x ∂μ

Tactic:
simpa using! (continuous_setIntegral s).comp
        (ContinuousLinearMap.continuous (Submodule.subtypeL _))

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t a b : ℝ
ha : Integrable (fun ω ↦ rexp (a * X ω)) μ
hb : Integrable (fun ω ↦ rexp (b * X ω)) μ
hat : a ≤ t
htb : t ≤ b
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
by
  refine Integrable.mono (ha.add hb) ?_ (ae_of_all _ fun ω ↦ ?_)
  · by_cases hab : a = b
    · have ha_eq_t : a = t := le_antisymm hat (hab ▸ htb)
      rw [← ha_eq_t]
      exact ha.1
    · refine AEMeasurable.aestronglyMeasurable ?_
      refine measurable_exp.comp_aemeasurable (AEMeasurable.const_mul ?_ _)
      by_cases ha_zero : a = 0
      · refine aemeasurable_of_aemeasurable_exp_mul ?_ hb.1.aemeasurable
        rw [ha_zero] at hab
        exact Ne.symm hab
      · exact aemeasurable_of_aemeasurable_exp_mul ha_zero ha.1.aemeasurable
  · simp only [norm_eq_abs, abs_exp, Pi.add_apply]
    conv_rhs => rw [abs_of_nonneg (by positivity)]
    rcases le_total 0 (X ω) with h | h
    · calc exp (t * X ω)
      _ ≤ exp (b * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonneg_right htb h)
      _ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_left (exp_nonneg _)
    · calc exp (t * X ω)
      _ ≤ exp (a * X ω) := exp_le_exp.mpr (mul_le_mul_of_nonpos_right hat h)
      _ ≤ exp (a * X ω) + exp (b * X ω) := le_add_of_nonneg_right (exp_nonneg _)

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

Goal state before:
pp: case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
⊢ mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t

Tactic:
have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable

Goal state after:
case insert
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (fun ω ↦ rexp (t * X i ω)) μ
⊢ mgf (∑ i ∈ insert i s, X i) μ t = ∏ i ∈ insert i s, mgf (X i) μ t
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
⊢ MemLp (stoppedValue u τ) p μ

Tactic:
refine memLp_stoppedValue_of_mem_finset hτ hu (s := Finset.Iic N) fun ω => ?_

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : Nonempty ι
μ : Measure Ω
τ : Ω → WithTop ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝² : PartialOrder ι
ℱ : Filtration ι m
inst✝¹ : NormedAddCommGroup E
inst✝ : LocallyFiniteOrderBot ι
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
N : ι
hbdd : ∀ (ω : Ω), τ ω ≤ ↑N
ω : Ω
⊢ τ ω ∈ WithTop.some '' ↑(Finset.Iic N)
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case left
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ l < v - min (v - l) (u - v) / 2

Tactic:
calc l = v - (v - l) := by abel
    _ ≤ v - ((v - l) ⊓ (u - v)) := by gcongr; exact inf_le_left
    _ < v - ((v - l) ⊓ (u - v)) / 2 := by gcongr; exact half_lt_self (by positivity)

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

Goal state before:
pp: case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ AEMeasurable X μ

pp: case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
hvt : ¬v + t = 0
⊢ AEMeasurable X μ

Tactic:
· have hvt' : v - t ≠ 0 := by
      rw [sub_ne_zero]
      refine fun h_eq ↦ ht.ne' ?_
      simpa [h_eq] using hvt
    exact aemeasurable_of_aemeasurable_exp_mul hvt'
      (h_subset (sub_half_inf_sub_mem_Ioo hvlu)).aemeasurable

Goal state after:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
hvt : ¬v + t = 0
⊢ AEMeasurable X μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
y : ℝ
this : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x
⊢ Measure.map (fun x ↦ y + x) (gaussianReal (-μ) v) = gaussianReal (y + -μ) v

Tactic:
gaussianReal_map_const_add,

Goal state after:
μ : ℝ
v : ℝ≥0
y : ℝ
this : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x
⊢ gaussianReal (-μ + y) v = gaussianReal (y + -μ) v
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω ↦ X ω ^ p) μ

Tactic:
by
  convert! integrable_rpow_mul_exp_of_mem_interior_integrableExpSet h hp using 1
  simp

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
⊢ IsGaussian (Measure.map (fun x ↦ -x) μ)

Tactic:
change IsGaussian (μ.map (ContinuousLinearEquiv.neg ℝ))

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
⊢ IsGaussian (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : IsGaussian μ
t : E
⊢ charFun μ t = cexp (↑⟪t, ∫ (x : E), id x ∂μ⟫ * I - ↑(((covarianceBilin μ) t) t) / 2)

Tactic:
rw [IsGaussian.charFun_eq, covarianceBilin_self, integral_complex_ofReal,
    integral_inner]
  · rfl
  · exact IsGaussian.integrable_id
  · exact IsGaussian.memLp_two_id

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

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

Tactic:
by norm_num

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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
⊢ 1 ≠ ∞

Tactic:
by norm_num

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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
⊢ 2 ≠ ∞

Tactic:
by norm_num

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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
⊢ ∃ L, Var[⇑L; μ] ≠ 0

Tactic:
contrapose! h

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
x : E
h : ∀ (L : StrongDual ℝ E), Var[⇑L; μ] = 0
⊢ ∃ x, μ = Measure.dirac x
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 : Ω → E
μ : Measure E
hX : HasLaw X μ P
inst✝ : IsGaussian μ
⊢ IsGaussian (Measure.map X P)

Tactic:
hX.map_eq

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
μ : Measure E
hX : HasLaw X μ P
inst✝ : IsGaussian μ
⊢ IsGaussian μ
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
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
⊢ 2 ≠ ∞

Tactic:
by norm_num

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✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
X : Ω → E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hX : HasGaussianLaw X P
⊢ 1 ≠ ∞

Tactic:
by norm_num

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
⊢ X s ⟂ᵢ[P] X t - X s

Tactic:
refine (hX.indepFun_sub_sub hrs hst).congr ?_ .rfl

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
⊢ X s - X r =ᵐ[P] X s
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
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
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
h_iUnion : Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
      ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
n : ℕ
⊢ 0 < 2⁻¹

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Probability.Process.FiniteDimensionalLaws

Goal state before:
pp: case refine_2
T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h :
  ∀ (I : Finset T), Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P
hX' : IsProjectiveLimit (Measure.map (fun ω x ↦ X x ω) P) fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

Tactic:
exact hX'.unique (isProjectiveLimit_map hY)

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
⊢ stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y

Tactic:
have : Nonempty { r' : ℚ // y < ↑r' } := by
    obtain ⟨r, hrx⟩ := exists_rat_gt y
    exact ⟨⟨r, hrx⟩⟩

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x y : ℝ
hxy : x ≤ y
this : Nonempty { r' // y < ↑r' }
⊢ stieltjesFunctionAux f a x ≤ stieltjesFunctionAux f a y
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ‖(preCDF ρ x x_1).toReal‖ₑ ∂ρ.fst ≤ ρ.fst univ

Tactic:
simp_rw [← ofReal_norm, Real.norm_of_nonneg ENNReal.toReal_nonneg]
    rw [← lintegral_one]
    refine (setLIntegral_le_lintegral _ _).trans (lintegral_mono_ae ?_)
    filter_upwards [preCDF_le_one ρ] with a ha using ENNReal.ofReal_toReal_le.trans (ha _)

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
a✝ : (ν a) s < ∞
⊢ ∫ (x : β) in s, ⨅ r, f (a, x) ↑r ∂ν a = ∫ (x : β) in s, f (a, x) q ∂ν a

Tactic:
hf.setIntegral _ hs,

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
a✝ : (ν a) s < ∞
⊢ ∫ (x : β) in s, ⨅ r, f (a, x) ↑r ∂ν a = (κ a).real (s ×ˢ Iic ↑q)
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 : α
⊢ (κ a) (univ ×ˢ univ) = (κ a) univ

Tactic:
univ_prod_univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
⊢ (κ a) univ = (κ a) univ
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case iUnion
α : 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 ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (⋃ i, f i) ∂ν a = (κ a) (s ×ˢ ⋃ i, f i)

Tactic:
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.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 ?_)

Goal state after:
α : 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 β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ ENNReal.ofReal 1 * (ν a) (countablePartitionSet n x)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν ν' : Kernel α γ
hνν' : ν ≤ ν'
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
h_le : (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ν a ≤ ν' a

Tactic:
· apply hνν'

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 Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
this : ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b ↦ (a, b)) ⋯
h : ∀ᵐ (x : β) ∂(ρ a).fst, (κ.comap (fun b ↦ (a, b)) ⋯) x = (ρ a).condKernel x
⊢ (fun b ↦ κ (a, b)) =ᵐ[ρ.fst a] ⇑(ρ a).condKernel

Tactic:
Kernel.fst_apply

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
this : ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b ↦ (a, b)) ⋯
h : ∀ᵐ (x : β) ∂(ρ a).fst, (κ.comap (fun b ↦ (a, b)) ⋯) x = (ρ a).condKernel x
⊢ (fun b ↦ κ (a, b)) =ᵐ[Measure.map Prod.fst (ρ a)] ⇑(ρ a).condKernel
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 ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
h : ∀ (a_1 : ι) (b_1 : a_1 ≤ b), (if h : a_1 ≤ a then x.1 ⟨a_1, ⋯⟩ else x.2 ⟨a_1, ⋯⟩) ∈ s ⟨a_1, ⋯⟩
i : ι
x✝ : a < i ∧ i ≤ b
hi1 : a < i
hi2 : i ≤ b
⊢ x.2 ⟨i, ⋯⟩ = if h : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩

Tactic:
dif_neg (not_le.2 hi1)

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
h : ∀ (a_1 : ι) (b_1 : a_1 ≤ b), (if h : a_1 ≤ a then x.1 ⟨a_1, ⋯⟩ else x.2 ⟨a_1, ⋯⟩) ∈ s ⟨a_1, ⋯⟩
i : ι
x✝ : a < i ∧ i ≤ b
hi1 : a < i
hi2 : i ≤ b
⊢ x.2 ⟨i, ⋯⟩ = x.2 ⟨i, ⋯⟩
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hab : a < b
⊢ partialTraj κ a b =
    Nat.leRec Kernel.id
      (fun k x κ_k ↦ (Kernel.id ×ₖ (κ k).map ⇑(piSingleton k) ∘ₖ κ_k).map (_root_.IicProdIoc k (k + 1))) hab✝

Tactic:
· rw [partialTraj, dif_neg (not_le.2 hab)]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : Measurable X
hY : Measurable Y
hs : MeasurableSet s
⊢ Integrable ((Y ⁻¹' s).indicator fun ω ↦ 1) μ

Tactic:
exact (integrable_const _).indicator (hY hs)

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

Goal state before:
pp: case hfi
α : 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
this : IsFiniteKernel κ
⊢ Integrable (fun x ↦ κ.density ν a x s) ((ν a).restrict A)

Tactic:
exact (integrable_density hκν a hs).restrict

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

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)
⊢ univ = univ ×ˢ univ

Tactic:
univ_prod_univ

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal ((κ a) univ)
⊢ univ = univ