awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
have μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have μ'D : μ' D = 0 := by
    rcases eventually_iff_exists_mem.1 hc with ⟨V, ae, hV⟩
    exact eq_of_le_of_not_lt (mem_ae_iff.1 ae ▸ (μ'.mono <| fun x h xV ↦ h.2 (hV x xV)))
      _root_.not_lt_zero
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
have obtain : ∀ (U : Set (ι → ℝ)) (UD : U ⊇ D) (Uopen : IsOpen U)
  (hU :
    (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U <
      HAdd.hAdd (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (ENNReal.ofReal ε₂)),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
Tactic: obtain ⟨U, UD, Uopen, hU⟩ := Set.exists_isOpen_lt_add D (show μ' D ≠ ⊤ by simp [μ'D]) ε₂0'
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU :
  (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U <
    HAdd.hAdd (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (ENNReal.ofReal ε₂)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
have hU₁ : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
Tactic: rw [μ'D, zero_add] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
have comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
Tactic: have comp : IsCompact (Box.Icc I \ U) :=
    I.isCompact_Icc.of_isClosed_subset (I.isCompact_Icc.isClosed.sdiff Uopen) Set.diff_subset
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x
this : oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x = 0
⊢ oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
have rw : 0 < ENNReal.ofReal ε₁
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
x : ι → ℝ
hx : Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x
⊢ oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
have suffices : oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x = 0
Tactic: suffices oscillationWithin f (Box.Icc I) x = 0 by rw [this]; exact ofReal_pos.2 ε₁0
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
have this : ∀ (x : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
    oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
Tactic: have : ∀ x ∈ (Box.Icc I \ U), oscillationWithin f (Box.Icc I) x < (ENNReal.ofReal ε₁) := by
    intro x hx
    suffices oscillationWithin f (Box.Icc I) x = 0 by rw [this]; exact ofReal_pos.2 ε₁0
    simpa [OscillationWithin.eq_zero_iff_continuousWithinAt, D, hx.1] using hx.2 ∘ (fun a ↦ UD a)
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
this :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
have rcases : ∀ (r : ℝ) (r0 : r > 0)
  (hr :
    ∀ (x : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
        ediam (f '' (eball x (ENNReal.ofReal r) ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) ≤ ENNReal.ofReal ε₁),
  ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
Tactic: rcases comp.uniform_oscillationWithin this with ⟨r, r0, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
this :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      ediam (f '' (eball x (ENNReal.ofReal r) ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) ≤ ENNReal.ofReal ε₁
⊢ ∃ (r : ℝ≥0 → (ι → ℝ) → (↑(Set.Ioi 0) : Type)),
    (∀ (c : ℝ≥0), l.RCond (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        l.MemBaseSet I c₁ (r c₁) π₁ →
          π₁.IsPartition →
            l.MemBaseSet I c₂ (r c₂) π₂ →
              π₂.IsPartition →
                dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
have refine : ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I)
  (h₁ :
    l.MemBaseSet I c₁
      ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) sorry)
        c₁)
      π₁)
  (h₁p : π₁.IsPartition)
  (h₂ :
    l.MemBaseSet I c₂
      ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) sorry)
        c₂)
      π₂)
  (h₂p : π₂.IsPartition), dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
Tactic: refine ⟨fun _ _ ↦ ⟨r / 2, half_pos r0⟩, fun _ _ _ ↦ rfl, fun c₁ c₂ π₁ π₂ h₁ h₁p h₂ h₂p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (goal)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
this :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      ediam (f '' (eball x (ENNReal.ofReal r) ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ :
  l.MemBaseSet I c₁
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) ⋯)
      c₁)
    π₁
h₁p : π₁.IsPartition
h₂ :
  l.MemBaseSet I c₂
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) ⋯)
      c₂)
    π₂
h₂p : π₂.IsPartition
⊢ dist (integralSum f μ.toBoxAdditive.toSMul π₁) (integralSum f μ.toBoxAdditive.toSMul π₂) ≤ ε
have simp : norm.{v} (E := E)
    (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
      HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
        (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
  ε
Tactic: simp only [dist_eq_norm, integralSum_sub_partitions _ _ h₁p h₂p, toSMul_apply, ← smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.Basic (hypothesis)
Goal:
ι : Type u
E : Type v
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Fintype ι
l : IntegrationParams
inst_3 : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst_4 : IsLocallyFiniteMeasure μ
hc :
  ∀ᵐ (x : ι → ℝ) ∂μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I),
    ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) I : ℝ) * ε₁ < ε
C : ℝ
hC :
  ∀ (x : ι → ℝ), Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x → ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) :=
  {x : ι → ℝ |
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I : Set (ι → ℝ)) x ∧
      ¬ContinuousWithinAt f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x}
μ' : Measure (ι → ℝ) := μ.restrict ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)
μ'D : Eq (α := ℝ≥0∞) ((μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) D : ℝ≥0∞) (0 : ℝ≥0∞)
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : (μ' : (a : Set (ι → ℝ)) → ℝ≥0∞) U < ENNReal.ofReal ε₂
comp : IsCompact.{u} (X := ι → ℝ) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U)
this :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      oscillationWithin f ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr :
  ∀ (x : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) ((Box.Icc : (a : Box ι) → Set (ι → ℝ)) I \ U : Set (ι → ℝ)) x →
      ediam (f '' (eball x (ENNReal.ofReal r) ∩ (Box.Icc : (a : Box ι) → Set (ι → ℝ)) I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ :
  l.MemBaseSet I c₁
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) ⋯)
      c₁)
    π₁
h₁p : π₁.IsPartition
h₂ :
  l.MemBaseSet I c₂
    ((fun (x : ℝ≥0) (x_1 : ι → ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (r / 2) ⋯)
      c₂)
    π₂
h₂p : π₂.IsPartition
⊢ norm.{v} (E := E)
      (∑ x ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        HSMul.hSMul (α := ℝ) ((μ.toBoxAdditive : (a : Box ι) → ℝ) x : ℝ)
          (f ((π₁.infPrepartition π₂.toPrepartition).tag x) - f ((π₂.infPrepartition π₁.toPrepartition).tag x))) ≤
    ε
have μI : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (ι → ℝ)) → ℝ≥0∞) (↑I : Set (ι → ℝ)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have μI : μ I < ⊤ := lt_of_le_of_lt (μ.mono I.coe_subset_Icc) I.isCompact_Icc.measure_lt_top