awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ AEMeasurable (_m := mΩ i) (X i) (Measure.map (fun (ω : (i : ι) → Ω i) ↦ ω i) (Measure.pi (α := Ω) μ))
have e_f : AEMeasurable (X i) (μ i)
Tactic: rw [(measurePreserving_eval _ i).map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
have ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
Tactic: have ha : ∀ᵐ ω ∂μ, a ≤ X ω := h.mono fun ω h => h.1
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
have hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
Tactic: have hb : ∀ᵐ ω ∂μ, X ω ≤ b := h.mono fun ω h => h.2
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
have hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
Tactic: have hX_int₂ : Integrable (fun ω ↦ -X ω ^ 2) μ :=
    (memLp_of_bounded h hX.aestronglyMeasurable 2).integrable_sq.neg
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
⊢ ∀ᵐ (a_1 : Ω) ∂μ, ‖X a_1‖ ≤ max |a| |b|
have h₁ : ∀ (a_1 : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ a ≤ X ω) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X ω ≤ b) x} x →
              Membership.mem (γ := Set Ω) {x : Ω | (fun (a_4 : Ω) ↦ ‖X a_4‖ ≤ max |a| |b|) x} x}
          x}
    a_1
Tactic: filter_upwards [ha, hb] with ω using abs_le_max_abs_abs
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
h₁ :
  ∀ (a_1 : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ a ≤ X ω) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X ω ≤ b) x} x →
                Membership.mem (γ := Set Ω) {x : Ω | (fun (a_4 : Ω) ↦ ‖X a_4‖ ≤ max |a| |b|) x} x}
            x}
      a_1
⊢ ∀ᵐ (a_1 : Ω) ∂μ, ‖X a_1‖ ≤ max |a| |b|
have h₂ : ∀ (a_1 : Ω), a ≤ X a_1 → X a_1 ≤ b → ‖X a_1‖ ≤ max |a| |b|
Tactic: filter_upwards [ha, hb] with ω using abs_le_max_abs_abs
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
have hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
Tactic: have hX_int₁ : Integrable (fun ω ↦ (a + b) * X ω) μ :=
    ((integrable_const (max |a| |b|)).mono' hX.aestronglyMeasurable
      (by filter_upwards [ha, hb] with ω using abs_le_max_abs_abs)).const_mul (a + b)
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
⊢ LE.le (α := ℝ) 0 (∫ (ω : Ω), (b - X ω) * (X ω - a) ∂μ)
have hf : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ (b - X x) * (X x - a)
Tactic: apply integral_nonneg_of_ae
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦ (b - X x) * (X x - a)
have h₁ : ∀ (ω : Ω) (ha' : a ≤ X ω) (hb' : X ω ≤ b), 0 ω ≤ (b - X ω) * (X ω - a)
Tactic: filter_upwards [ha, hb] with ω ha' hb'
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
ω : Ω
ha' : a ≤ X ω
hb' : X ω ≤ b
⊢ 0 ≤ b - X ω
have linarith : b - X ω < 0 → X ω - b + (b - X ω - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
ω : Ω
ha' : a ≤ X ω
hb' : X ω ≤ b
⊢ 0 ≤ X ω - a
have linarith : X ω - a < 0 → a - X ω + (X ω - a - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
have h0 : 0 ≤ -∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
Tactic: have h0 : 0 ≤ -μ[X ^ 2] + (a + b) * μ[X] - a * b :=
    calc
      _ ≤ ∫ ω, (b - X ω) * (X ω - a) ∂μ := by
        apply integral_nonneg_of_ae
        filter_upwards [ha, hb] with ω ha' hb'
        exact mul_nonneg (by linarith : 0 ≤ b - X ω) (by linarith : 0 ≤ X ω - a)
      _ = ∫ ω, -X ω ^ 2 + (a + b) * X ω - a * b ∂μ :=
        integral_congr_ae <| ae_of_all μ fun ω ↦ by ring
      _ = ∫ ω, - X ω ^ 2 + (a + b) * X ω ∂μ - ∫ _, a * b ∂μ :=
        integral_sub (by fun_prop) (integrable_const (a * b))
      _ = ∫ ω, - X ω ^ 2 + (a + b) * X ω ∂μ - a * b := by simp
      _ = - μ[X ^ 2] + (a + b) * μ[X] - a * b := by
        simp [← integral_neg, ← integral_const_mul, integral_add hX_int₂ hX_int₁]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ Var[X; μ] ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
have rw : ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 ≤
  (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
Tactic: rw [variance_eq_sub (memLp_of_bounded h hX.aestronglyMeasurable 2)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 ≤
    (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
have linarith : (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 <
    ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 →
  0 - (-∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b) +
      ((a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 -
        (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
have _ : Var[X; μ] ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
Tactic: calc
    _ ≤ (a + b) * μ[X] - a * b - μ[X] ^ 2 := by
      rw [variance_eq_sub (memLp_of_bounded h hX.aestronglyMeasurable 2)]
      linarith
    _ = (b - μ[X]) * (μ[X] - a) := by ring
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
ha : ∀ᵐ (ω : Ω) ∂μ, a ≤ X ω
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
hX_int₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ -HPow.hPow (β := ℕ) (X ω) 2) μ
hX_int₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ (a + b) * X ω) μ
h0 : 0 ≤ -∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ + (a + b) * ∫ (x : Ω), X x ∂μ - a * b
_ : Var[X; μ] ≤ (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
⊢ Var[X; μ] ≤ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
have _₁ : (a + b) * ∫ (x : Ω), X x ∂μ - a * b - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 =
  (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a)
Tactic: calc
    _ ≤ (a + b) * μ[X] - a * b - μ[X] ^ 2 := by
      rw [variance_eq_sub (memLp_of_bounded h hX.aestronglyMeasurable 2)]
      linarith
    _ = (b - μ[X]) * (μ[X] - a) := by ring
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ Var[fun (p : Ω × Ω') ↦ X p.1 + Y p.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
have refine_1 : (fun (x : Ω × Ω') ↦ X x.1) ⟂ᵢ[μ.prod ν] fun (x : Ω × Ω') ↦ Y x.2
Tactic: refine (IndepFun.variance_fun_add (hfμ.comp_fst ν) (hgν.comp_snd μ) ?_).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
refine_1 : (fun (x : Ω × Ω') ↦ X x.1) ⟂ᵢ[μ.prod ν] fun (x : Ω × Ω') ↦ Y x.2
⊢ Var[fun (p : Ω × Ω') ↦ X p.1 + Y p.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
have refine_2 : Var[fun (x : Ω × Ω') ↦ X x.1; μ.prod ν] + Var[fun (x : Ω × Ω') ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
Tactic: refine (IndepFun.variance_fun_add (hfμ.comp_fst ν) (hgν.comp_snd μ) ?_).trans ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
⊢ Var[fun (x : Ω × Ω') ↦ X x.1; μ.prod ν] + Var[fun (x : Ω × Ω') ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
have refine_2 : Var[X; μ] + Var[fun (x : Ω × Ω') ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
Tactic: rw [measurePreserving_fst.variance_fun_comp hfμ.aemeasurable,
      measurePreserving_snd.variance_fun_comp hgν.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
X : Ω → ℝ
Y : Ω' → ℝ
hfμ : MemLp X 2 μ
hgν : MemLp Y 2 ν
refine_2 : Var[X; μ] + Var[fun (x : Ω × Ω') ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
⊢ Var[fun (x : Ω × Ω') ↦ X x.1; μ.prod ν] + Var[fun (x : Ω × Ω') ↦ Y x.2; μ.prod ν] = Var[X; μ] + Var[Y; ν]
have refine_2₁ : Var[X; μ] + Var[Y; ν] = Var[X; μ] + Var[Y; ν]
Tactic: rw [measurePreserving_fst.variance_fun_comp hfμ.aemeasurable,
      measurePreserving_snd.variance_fun_comp hgν.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
⊢ Eq (α := (a : E × F) → ℝ) (⇑L : (a : E × F) → ℝ) fun (x : E × F) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)
have h : ∀ (x : E × F),
  (L : (a : E × F) → ℝ) x =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
x : E × F
⊢ (L : (a : E × F) → ℝ) x =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)
have h : Eq (α := ℝ) ((L : (a : E × F) → ℝ) x : ℝ) ((L : (a : E × F) → ℝ) x : ℝ)
Tactic: rw [L.comp_inl_add_comp_inr]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
⊢ Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] =
    Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]
have this : Eq (α := (a : E × F) → ℝ) (⇑L : (a : E × F) → ℝ) fun (x : E × F) ↦
  HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
    ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)
Tactic: have : L = fun x : E × F ↦ L.comp (.inl ℝ E F) x.1 + L.comp (.inr ℝ E F) x.2 := by
    ext; rw [L.comp_inl_add_comp_inr]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
this :
  Eq (α := (a : E × F) → ℝ) (⇑L : (a : E × F) → ℝ) fun (x : E × F) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)
⊢ Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] =
    Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]
have rw : Var[fun (x : E × F) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ);
    μ.prod ν] =
  Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
    Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]
Tactic: rw [this, variance_add_prod hLμ hLν]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : IsProbabilityMeasure μ
ν : Measure F
inst_5 : IsProbabilityMeasure ν
L : StrongDual ℝ (E × F)
hLμ : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ) 2 μ
hLν : MemLp (ε := ℝ) (⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ) 2 ν
this :
  Eq (α := (a : E × F) → ℝ) (⇑L : (a : E × F) → ℝ) fun (x : E × F) ↦
    HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
      ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ)
rw :
  Var[fun (x : E × F) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((L ∘SL ContinuousLinearMap.inl ℝ E F : (a : E) → ℝ) x.1 : ℝ)
        ((L ∘SL ContinuousLinearMap.inr ℝ E F : (a : F) → ℝ) x.2 : ℝ);
      μ.prod ν] =
    Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]
⊢ Var[(⇑L : (a : E × F) → ℝ); μ.prod ν] =
    Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
      Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]
have rw₁ : Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
    Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν] =
  Var[(⇑(L ∘SL ContinuousLinearMap.inl ℝ E F) : (a : E) → ℝ); μ] +
    Var[(⇑(L ∘SL ContinuousLinearMap.inr ℝ E F) : (a : F) → ℝ); ν]
Tactic: rw [this, variance_add_prod hLμ hLν]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ p.support
have rw : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mem_support_iff, Classical.not_not]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
rw :
  Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ p.support
have rw₁ : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mem_support_iff, Classical.not_not]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
⊢ Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞) ↔ p.support = {a}
have refine : ∀ (h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)) (a' : α) (ha' : a' ∈ p.support) (ha : a' ∉ {a}), False
Tactic: refine ⟨fun h => Set.Subset.antisymm (fun a' ha' => by_contra fun ha => ?_)
    fun a' ha' => ha'.symm ▸ (p.mem_support_iff a).2 fun ha => zero_ne_one <| ha.symm.trans h,
    fun h => _root_.trans (symm <| tsum_eq_single a
      fun a' ha' => (p.apply_eq_zero_iff a').2 (h.symm ▸ ha')) p.tsum_coe⟩
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ False
have suffices : LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
Tactic: suffices 1 < ∑' a, p a from ne_of_lt this p.tsum_coe.symm
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
have rw : ∃ (x : α), Ne (α := ℝ≥0∞) (if x = a then 0 else (p : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [pos_iff_ne_zero, ENNReal.summable.tsum_ne_zero_iff]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (hypothesis)
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
⊢ LT.lt (α := ℝ≥0∞) 1 (∑' (a : α), (p : (a : α) → ℝ≥0∞) a)
have this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
Tactic: have : 0 < ∑' b, ite (b = a) 0 (p b) := by
    rw [pos_iff_ne_zero, ENNReal.summable.tsum_ne_zero_iff]
    exact ⟨a', ite_ne_left_iff.2 ⟨ha, Ne.symm <| (p.mem_support_iff a').2 ha'⟩⟩
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Basic (goal)
Goal:
α : Type u_1
p : PMF α
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞)
a' : α
ha' : a' ∈ p.support
ha : a' ∉ {a}
this : LT.lt (α := ℝ≥0∞) 0 (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if a = a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
      (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (if True then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)
    (∑' (b : α), if b = a then 0 else (p : (a : α) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: rw [eq_self_iff_true, if_true]