awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Eq (α := (ι → κ → X) → (a : (_ : ι) × κ) → X)
    (Function.comp (β := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
    (⇑(MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_1 : κ) ↦ X)) :
      (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
have h : ∀ (x : ι → κ → X) (x_1 : (_ : ι) × κ),
  Eq.{u_8 + 1} (α := X)
    (Function.comp (β := (b : ι × κ) → X)
        (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
              ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
          (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
        (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X) x x_1 :
      X)
    ((MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_2 : κ) ↦ X) :
          (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
        x x_1 :
      X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Eq (α := Measure ((a : (_ : ι) × κ) → X))
    (map (α := ι → κ → X)
      (Function.comp (β := (b : ι × κ) → X)
        (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
              ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
          (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
        (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
      (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j))
    (map (α := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))
have this : Eq (α := (ι → κ → X) → (a : (_ : ι) × κ) → X)
  (Function.comp (β := (b : ι × κ) → X)
    (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
          ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
      (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
  (⇑(MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_1 : κ) ↦ X)) :
    (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
Tactic: have : (MeasurableEquiv.piCongrLeft (fun _ ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘
        (MeasurableEquiv.curry ι κ X).symm = ⇑(MeasurableEquiv.piCurry (fun _ _ ↦ X)).symm := by
      ext; simp [piCongrLeft, Equiv.piCongrLeft, Sigma.uncurry]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
this :
  Eq (α := (ι → κ → X) → (a : (_ : ι) × κ) → X)
    (Function.comp (β := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
    (⇑(MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_1 : κ) ↦ X)) :
      (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
⊢ Eq (α := Measure ((a : (_ : ι) × κ) → X))
    (map (α := ι → κ → X)
      (Function.comp (β := (b : ι × κ) → X)
        (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
              ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
          (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
        (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
      (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j))
    (map (α := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))
have rw : Eq (α := Measure ((a : (_ : ι) × κ) → X))
  (infinitePi (X := fun (p : (_ : ι) × κ) ↦ X) fun (p : (_ : ι) × κ) ↦
    μ (p.fst (β := fun (i : ι) ↦ κ)) (p.snd (β := fun (i : ι) ↦ κ)))
  (map (α := (b : ι × κ) → X)
    (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
          ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
      (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
    (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))
Tactic: rw [this, infinitePi_map_piCurry_symm]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Eq (α := Measure (ι → κ → X))
    (map (α := ι × κ → X) (⇑(MeasurableEquiv.curry ι κ X) : (a : ι × κ → X) → ι → κ → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))
    (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j)
have rw : Eq (α := Measure (ι × κ → X)) (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2)
  (map (α := ι → κ → X) (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X)
    (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j))
Tactic: rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_curry_symm]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
rw :
  Eq (α := Measure (ι × κ → X)) (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2)
    (map (α := ι → κ → X) (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X)
      (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j))
⊢ Eq (α := Measure (ι → κ → X))
    (map (α := ι × κ → X) (⇑(MeasurableEquiv.curry ι κ X) : (a : ι × κ → X) → ι → κ → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))
    (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j)
have rw₁ : Eq (α := Measure (ι × κ → X)) (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2)
  (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2)
Tactic: rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_curry_symm]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X (↑i : ι)) → E
hf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) f
    (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : (i : ι) → X i), f (s.restrict (π := X) y) ∂infinitePi (X := X) μ)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι)))
      (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) fun (y : (i : ↥s) → X (↑i : ι)) ↦ f y)
have hφ : AEMeasurable (s.restrict (π := X)) (infinitePi (X := X) μ)
Tactic: rw [← integral_map, infinitePi_map_restrict]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X (↑i : ι)) → E
hf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) f
    (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))
hφ : AEMeasurable (s.restrict (π := X)) (infinitePi (X := X) μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : (i : ι) → X i), f (s.restrict (π := X) y) ∂infinitePi (X := X) μ)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι)))
      (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) fun (y : (i : ↥s) → X (↑i : ι)) ↦ f y)
have hfm : AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) f
  (Measure.map (s.restrict (π := X)) (infinitePi (X := X) μ))
Tactic: rw [← integral_map, infinitePi_map_restrict]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
f : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (y : (i : ι) → X i), f (s.restrict (π := X) y) ∂infinitePi (X := X) μ =
    ∫⁻ (y : (i : ↥s) → X (↑i : ι)), f y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)
have rw : ∫⁻ (a : (i : ↥s) → X (↑i : ι)), f a ∂Measure.map (s.restrict (π := X)) (infinitePi (X := X) μ) =
  ∫⁻ (y : (i : ↥s) → X (↑i : ι)), f y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)
Tactic: rw [← lintegral_map hf (measurable_restrict _), isProjectiveLimit_infinitePi μ]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
f : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (a : (i : ↥s) → X (↑i : ι)), f a ∂Measure.map (s.restrict (π := X)) (infinitePi (X := X) μ) =
    ∫⁻ (y : (i : ↥s) → X (↑i : ι)), f y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)
⊢ ∫⁻ (y : (i : ι) → X i), f (s.restrict (π := X) y) ∂infinitePi (X := X) μ =
    ∫⁻ (y : (i : ↥s) → X (↑i : ι)), f y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)
have rw₁ : ∫⁻ (a : (i : ↥s) → X (↑i : ι)),
    f
      a ∂(fun (I : Finset ι) ↦
        (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : Measure ((i : ↥I) → X (↑i : ι))))
      s =
  ∫⁻ (y : (i : ↥s) → X (↑i : ι)), f y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)
Tactic: rw [← lintegral_map hf (measurable_restrict _), isProjectiveLimit_infinitePi μ]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → E := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : (i : ι) → X i), f y ∂infinitePi (X := X) μ)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι)))
      (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) fun (y : (i : ↥s) → X (↑i : ι)) ↦
      f (Function.updateFinset (π := X) x s y))
have this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
Tactic: have this y : g (s.restrict y) = f y :=
    mf.dependsOn_of_piFinset fun i hi ↦ by simp_all [Function.updateFinset]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → E := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : (i : ι) → X i), f y ∂infinitePi (X := X) μ)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι)))
      (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) fun (y : (i : ↥s) → X (↑i : ι)) ↦
      f (Function.updateFinset (π := X) x s y))
have hf : AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) g
  (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))
Tactic: rw [← integral_congr_ae <| ae_of_all _ this, integral_restrict_infinitePi]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
⊢ ∫⁻ (y : (i : ι) → X i), f y ∂infinitePi (X := X) μ = lmarginal (X := X) μ s f x
have this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
Tactic: have this y : g (s.restrict y) = f y :=
    mf.dependsOn_of_piFinset fun i hi ↦ by simp_all [Function.updateFinset]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
⊢ ∫⁻ (y : (i : ι) → X i), f y ∂infinitePi (X := X) μ = lmarginal (X := X) μ s f x
have rw : (∫⁻ (y : (i : ↥s) → X (↑i : ι)), g y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) =
  lmarginal (X := X) μ s f x
Tactic: rw [← lintegral_congr_ae <| ae_of_all _ this, lintegral_restrict_infinitePi]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞ := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
rw :
  (∫⁻ (y : (i : ↥s) → X (↑i : ι)), g y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) =
    lmarginal (X := X) μ s f x
⊢ ∫⁻ (y : (i : ι) → X i), f y ∂infinitePi (X := X) μ = lmarginal (X := X) μ s f x
have hf : Measurable g
Tactic: rw [← lintegral_congr_ae <| ae_of_all _ this, lintegral_restrict_infinitePi]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ AEStronglyMeasurable (ProbabilityTheory.truncation f A) μ
have apply : AEStronglyMeasurable (m₀ := Real.measurableSpace) ((Set.Ioc (-A) A).indicator id) (Measure.map f μ)
Tactic: apply AEStronglyMeasurable.comp_aemeasurable _ hf.aemeasurable
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |A|
have simp : |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|
Tactic: simp only [truncation, Set.indicator, id, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|
have pos : ∀ (h : f x ∈ Set.Ioc (-A) A), |f x| ≤ |A|
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
pos : ∀ (h : f x ∈ Set.Ioc (-A) A), |f x| ≤ |A|
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |A|
have neg : ∀ (h : f x ∉ Set.Ioc (-A) A), |0| ≤ |A|
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
⊢ truncation f 0 = 0
have simp : Eq (α := α → ℝ) ((fun (x : ℝ) ↦ 0) ∘ f) 0
Tactic: simp [truncation]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|
have simp : |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|
Tactic: simp only [truncation, indicator, id, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|
have pos : f x ∈ Set.Ioc (-A) A → |f x| ≤ |f x|
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
pos : f x ∈ Set.Ioc (-A) A → |f x| ≤ |f x|
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|
have neg : f x ∉ Set.Ioc (-A) A → |0| ≤ |f x|
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
⊢ truncation f A x = f x
have simp : f x ∉ Set.Ioc (-A) A → 0 = f x
Tactic: simp only [truncation, indicator, id, Function.comp_apply, ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
⊢ 0 = f x
have apply : f x ∈ Set.Ioc (-A) A
Tactic: apply H.elim
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
⊢ truncation f A = (Set.Ioc 0 A).indicator id ∘ f
have h₁ : ∀ (x : α), truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
have h₁ : ∀ (hx : 0 < f x), truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
Tactic: rcases (h x).lt_or_eq with (hx | hx)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
h₁ : ∀ (hx : 0 < f x), truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
have h₂ : ∀ (hx : 0 = f x), truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
Tactic: rcases (h x).lt_or_eq with (hx | hx)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x
have h₁ : (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
Tactic: simp only [truncation, indicator, hx, Set.mem_Ioc, id, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
have pos : ∀ (h'x : f x ≤ A), (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
Tactic: by_cases h'x : f x ≤ A
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
pos : ∀ (h'x : f x ≤ A), (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
have neg : ∀ (h'x : ¬f x ≤ A), (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
Tactic: by_cases h'x : f x ≤ A
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
⊢ -A < f x
have linarith : f x ≤ -A → 2 * (0 - f x) + (f x - A) + (f x - -A) = 0
Tactic: linarith [h x]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
linarith : f x ≤ -A → 2 * (0 - f x) + (f x - A) + (f x - -A) = 0
⊢ -A < f x
have linarith₁ : f x ≤ -A → GT.gt (α := ℝ) 2 0
Tactic: linarith [h x]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
have this : -A < f x
Tactic: have : -A < f x := by linarith [h x]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ Integrable (truncation f A) μ
have rw : MemLp (truncation f A) 1 μ
Tactic: rw [← memLp_one_iff_integrable]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
⊢ Eq (α := ℝ) (∫ (x : α), truncation f A x ^ n ∂μ) (∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ)
have M : MeasurableSet (Set.Ioc (-A) A)
Tactic: have M : MeasurableSet (Set.Ioc (-A) A) := measurableSet_Ioc
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc (-A) A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ)
have rw : Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc (-A) A).indicator id y ^ n)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
    (Set.Ioc (-A) A).indicator (fun (x : ℝ) ↦ x ^ n) x)
Tactic: rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le,
    ← integral_indicator M]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc (-A) A).indicator id y ^ n)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc (-A) A).indicator (fun (x : ℝ) ↦ x ^ n) x)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc (-A) A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ)
have rw₁ : -A ≤ A
Tactic: rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le,
    ← integral_indicator M]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc (-A) A).indicator id y ^ n)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc (-A) A).indicator (fun (x : ℝ) ↦ x ^ n) x)
rw₁ : -A ≤ A
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc (-A) A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ)
have rw₂ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc (-A) A).indicator id z ^ n)
  (Measure.map f μ)
Tactic: rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le,
    ← integral_indicator M]