awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
⊢ integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B) =
    (∑' (x :
        (↑(s ∩
              HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
          Type u_1)),
        F (↑x : ι → ℝ)) /
      HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
have unfold : ∑ J ∈ (prepartition n B).boxes,
    ((((BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume) : ι →ᵇᵃ[⊤] ℝ →L[ℝ] ℝ) : (a : Box ι) → ℝ →L[ℝ] ℝ) J :
          ℝ →L[ℝ] ℝ) :
        (a : ℝ) → ℝ)
      (s.indicator F ((prepartition n B).tag J)) =
  (∑' (x :
      (↑(s ∩
            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
        Type u_1)),
      F (↑x : ι → ℝ)) /
    HPow.hPow (α := ℝ) (↑n : ℝ) (card ι)
Tactic: classical
  unfold integralSum
  have : Fintype ↑(s ∩ (n : ℝ)⁻¹ • L) := by
    apply Set.Finite.fintype
    rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))]
    exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)
  rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm]
  simp_rw [Set.indicator_apply, apply_ite, BoxAdditiveMap.toSMul_apply, Measure.toBoxAdditive_apply,
    smul_eq_mul, mul_zero, Finset.sum_ite, Finset.sum_const_zero, add_zero]
  refine Finset.sum_bij (fun x _ ↦ box n (index n x)) (fun _ hx ↦ Finset.mem_filter.mpr ?_)
    (fun _ hx _ hy h ↦ ?_) (fun I hI ↦ ?_) (fun _ hx ↦ ?_)
  · rw [Set.mem_toFinset] at hx
    refine ⟨mem_prepartition_boxes_iff.mpr
      ⟨index n _, mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1), rfl⟩, ?_⟩
    simp_rw [prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
      tag_index_eq_self_of_mem_smul_span n hx.2, hx.1]
  · rw [Set.mem_toFinset] at hx hy
    exact eq_of_mem_smul_span_of_index_eq_index n hx.2 hy.2 (box_injective n h)
  · rw [Finset.mem_filter] at hI
    refine ⟨(prepartition n B).tag I, Set.mem_toFinset.mpr ⟨hI.2, ?_⟩, box_index_tag_eq_self n hI.1⟩
    rw [← box_index_tag_eq_self n hI.1, prepartition_tag n
      (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))]
    exact tag_mem_smul_span _ _
  · rw [Set.mem_toFinset] at hx
    rw [measureReal_def, volume_box,
      prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
      tag_index_eq_self_of_mem_smul_span n hx.2, ENNReal.toReal_div,
      ENNReal.toReal_one, ENNReal.toReal_pow, ENNReal.toReal_natCast, mul_comm_div, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x))
have obtain : ∀ (B : Box ι) (hB : hasIntegralVertices B) (hs₀ : s ≤ (↑B : Set (ι → ℝ))),
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x))
Tactic: obtain ⟨B, hB, hs₀⟩ := le_hasIntegralVertices_of_isBounded hs₁
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      (∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
    atTop
    (𝓝
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x))
have refine : ∀ (ε : ℝ) (hε : ε > 0),
  ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε
Tactic: refine Metric.tendsto_atTop.mpr fun ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
have obtain : ∀ (C₀ : ℝ)
  (h₀ :
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀),
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
Tactic: obtain ⟨C₀, h₀⟩ := (Box.isCompact_Icc B).exists_bound_of_continuousOn hF.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
⊢ ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
have refine : ∀ (x : ι → ℝ) (hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x),
  ‖s.indicator F x‖ ≤ max 0 C₀
Tactic: refine ⟨max 0 C₀, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x
⊢ ‖if x ∈ s then F x else 0‖ ≤ max 0 C₀
have pos : ∀ (hs : x ∈ s), ‖F x‖ ≤ max 0 C₀
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖F x‖ ≤ C₀
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x
pos : ∀ (hs : x ∈ s), ‖F x‖ ≤ max 0 C₀
⊢ ‖if x ∈ s then F x else 0‖ ≤ max 0 C₀
have neg : ∀ (hs : x ∉ s), norm (E := ℝ) 0 ≤ max 0 C₀
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
⊢ ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε
have h₁ : ∃ (C : ℝ),
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x → ‖s.indicator F x‖ ≤ C
Tactic: have h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖Set.indicator s F x‖ ≤ C := by
    obtain ⟨C₀, h₀⟩ := (Box.isCompact_Icc B).exists_bound_of_continuousOn hF.continuousOn
    refine ⟨max 0 C₀, fun x hx ↦ ?_⟩
    rw [Set.indicator]
    split_ifs with hs
    · exact le_max_of_le_right (h₀ x hx)
    · exact norm_zero.trans_le <| le_max_left 0 _
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
⊢ ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
have h : ∀ (a : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ))
    {x : ι → ℝ |
      x ∈ (frontier s)ᶜ →
        Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | (fun (x : ι → ℝ) ↦ ContinuousAt (s.indicator F) x) x} x}
    a
Tactic: filter_upwards [compl_mem_ae_iff.mpr hs₃] with _ h
      using (hF.continuousOn).continuousAt_indicator h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h :
  ∀ (a : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ))
      {x : ι → ℝ |
        x ∈ (frontier s)ᶜ →
          Membership.mem (γ := Set (ι → ℝ)) {x : ι → ℝ | (fun (x : ι → ℝ) ↦ ContinuousAt (s.indicator F) x) x} x}
      a
⊢ ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
have h₂ : ∀ a ∈ (frontier s)ᶜ, ContinuousAt (s.indicator F) a
Tactic: filter_upwards [compl_mem_ae_iff.mpr hs₃] with _ h
      using (hF.continuousOn).continuousAt_indicator h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
⊢ ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε
have h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
Tactic: have h₂ : ∀ᵐ x, ContinuousAt (s.indicator F) x := by
    filter_upwards [compl_mem_ae_iff.mpr hs₃] with _ h
      using (hF.continuousOn).continuousAt_indicator h
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
⊢ ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε
have obtain : ∀ (r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)) (hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c))
  (hr₂ :
    ∀ (c : NNReal) (π : TaggedPrepartition B),
      IntegrationParams.Riemann.MemBaseSet B c (r c) π →
        π.IsPartition →
          dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
              (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
                (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
            ε / 2),
  ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε
Tactic: obtain ⟨r, hr₁, hr₂⟩ := (hasIntegral_iff.mp <|
      AEContinuous.hasBoxIntegral (volume : Measure (ι → ℝ)) h₁ h₂
        IntegrationParams.Riemann) (ε / 2) (half_pos hε)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
⊢ ∃ (N : ℕ),
    ∀ n ≥ N,
      dist
          ((∑' (x :
              (↑(s ∩
                    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
                Type u_1)),
              F (↑x : ι → ℝ)) /
            HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
          (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
            F x) <
        ε
have refine : ∀ (n : ℕ) (hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊),
  dist
      ((∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x) ≤
    ε / 2
Tactic: refine ⟨⌈(r 0 0 : ℝ)⁻¹⌉₊, fun n hn ↦ lt_of_le_of_lt ?_ (half_lt_self_iff.mpr hε)⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (hypothesis)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
⊢ dist
      ((∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x) ≤
    ε / 2
have this : NeZero n
Tactic: have : NeZero n :=
    ⟨Nat.ne_zero_iff_zero_lt.mpr <| (Nat.ceil_pos.mpr (inv_pos.mpr (r 0 0).prop)).trans_le hn⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
⊢ dist
      ((∑' (x :
          (↑(s ∩
                HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                  (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
            Type u_1)),
          F (↑x : ι → ℝ)) /
        HPow.hPow (α := ℝ) (↑n : ℝ) (card ι))
      (@MeasureTheory.integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume s) fun (x : ι → ℝ) ↦
        F x) ≤
    ε / 2
have rw : dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B))
    (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
      (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
  ε / 2
Tactic: rw [← integralSum_eq_tsum_div _ s F hB hs₀, ← Measure.restrict_restrict_of_subset hs₀,
    ← integral_indicator hs₂]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst : Fintype ι
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ :
  Eq (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (frontier s) : ENNReal) (0 : ENNReal)
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
ε : ℝ
hε : ε > 0
h₁ :
  ∃ (C : ℝ),
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) B : Set (ι → ℝ)) x →
        ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → (↑(Set.Ioi 0) : Type)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) π)
            (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
              (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0) : ℝ)⁻¹⌉₊
this : NeZero n
⊢ dist (integralSum (s.indicator F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B))
      (@MeasureTheory.integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
        (Measure.restrict volume (↑B : Set (ι → ℝ)) : Measure (ι → ℝ)) fun (x : ι → ℝ) ↦ s.indicator F x) ≤
    ε / 2
have refine_1 : (prepartition n B).IsSubordinate (r 0)
Tactic: refine hr₂ 0 _ ⟨?_, fun _ ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩ (prepartition_isPartition _ hB)