ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc : UniformContinuousOn f (↑Box.Icc I)
⊢ Integrable I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
have huc := I.isCompact_Icc.uniformContinuousOn_of_continuous hc
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
⊢ Integrable I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc : UniformContinuousOn f (↑Box.Icc I)
⊢ Integrable I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
rw [Metric.uniformContinuousOn_iff_le] at huc
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ r,
    (∀ (c : ℝ≥0), RCond l (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        MemBaseSet l I c₁ (r c₁) π₁ →
          IsPartition π₁ →
            MemBaseSet l I c₂ (r c₂) π₂ →
              IsPartition π₂ →
                dist (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₁)
                    (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₂) ≤
                  ε
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
⊢ Integrable I l f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ))
refine' integrable_iff_cauchy_basis.2 fun ε ε0 => _
case intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
⊢ ∃ r,
    (∀ (c : ℝ≥0), RCond l (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        MemBaseSet l I c₁ (r c₁) π₁ →
          IsPartition π₁ →
            MemBaseSet l I c₂ (r c₂) π₂ →
              IsPartition π₂ →
                dist (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₁)
                    (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₂) ≤
                  ε
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ r,
    (∀ (c : ℝ≥0), RCond l (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        MemBaseSet l I c₁ (r c₁) π₁ →
          IsPartition π₁ →
            MemBaseSet l I c₂ (r c₂) π₂ →
              IsPartition π₂ →
                dist (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₁)
                    (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₂) ≤
                  ε
rcases exists_pos_mul_lt ε0 (μ.toBoxAdditive I) with ⟨ε', ε0', hε⟩
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
⊢ ∃ r,
    (∀ (c : ℝ≥0), RCond l (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        MemBaseSet l I c₁ (r c₁) π₁ →
          IsPartition π₁ →
            MemBaseSet l I c₂ (r c₂) π₂ →
              IsPartition π₂ →
                dist (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₁)
                    (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₂) ≤
                  ε
case intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
⊢ ∃ r,
    (∀ (c : ℝ≥0), RCond l (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        MemBaseSet l I c₁ (r c₁) π₁ →
          IsPartition π₁ →
            MemBaseSet l I c₂ (r c₂) π₂ →
              IsPartition π₂ →
                dist (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₁)
                    (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₂) ≤
                  ε
rcases huc ε' ε0' with ⟨δ, δ0 : 0 < δ, Hδ⟩
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
⊢ dist (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₁)
      (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₂) ≤
    ε
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
⊢ ∃ r,
    (∀ (c : ℝ≥0), RCond l (r c)) ∧
      ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : TaggedPrepartition I),
        MemBaseSet l I c₁ (r c₁) π₁ →
          IsPartition π₁ →
            MemBaseSet l I c₂ (r c₂) π₂ →
              IsPartition π₂ →
                dist (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₁)
                    (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₂) ≤
                  ε
refine' ⟨fun _ _ => ⟨δ / 2, half_pos δ0⟩, fun _ _ _ => rfl, fun c₁ c₂ π₁ π₂ h₁ h₁p h₂ h₂p => _⟩
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
⊢ ‖∑ x in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        ↑(Measure.toBoxAdditive μ) x •
          (f (tag (infPrepartition π₁ π₂.toPrepartition) x) - f (tag (infPrepartition π₂ π₁.toPrepartition) x))‖ ≤
    ε
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
⊢ dist (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₁)
      (integralSum f (BoxAdditiveMap.toSMul (Measure.toBoxAdditive μ)) π₂) ≤
    ε
simp only [dist_eq_norm, integralSum_sub_partitions _ _ h₁p h₂p, BoxAdditiveMap.toSMul_apply,
  ← smul_sub]
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
this :
  ∀ (J : Box ι),
    J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition →
      ‖↑(Measure.toBoxAdditive μ) J •
            (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
        ↑(Measure.toBoxAdditive μ) J * ε'
⊢ ∑ b in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, ↑(Measure.toBoxAdditive μ) b * ε' ≤ ε
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
this :
  ∀ (J : Box ι),
    J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition →
      ‖↑(Measure.toBoxAdditive μ) J •
            (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
        ↑(Measure.toBoxAdditive μ) J * ε'
⊢ ‖∑ x in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
        ↑(Measure.toBoxAdditive μ) x •
          (f (tag (infPrepartition π₁ π₂.toPrepartition) x) - f (tag (infPrepartition π₂ π₁.toPrepartition) x))‖ ≤
    ε
refine' (norm_sum_le_of_le _ this).trans _
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
this :
  ∀ (J : Box ι),
    J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition →
      ‖↑(Measure.toBoxAdditive μ) J •
            (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
        ↑(Measure.toBoxAdditive μ) J * ε'
⊢ ↑(Measure.toBoxAdditive μ) I * ε' ≤ ε
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
this :
  ∀ (J : Box ι),
    J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition →
      ‖↑(Measure.toBoxAdditive μ) J •
            (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
        ↑(Measure.toBoxAdditive μ) J * ε'
⊢ ∑ b in (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, ↑(Measure.toBoxAdditive μ) b * ε' ≤ ε
rw [← Finset.sum_mul, μ.toBoxAdditive.sum_partition_boxes le_top (h₁p.inf h₂p)]
no goals
case intro.intro.intro.intro
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
this :
  ∀ (J : Box ι),
    J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition →
      ‖↑(Measure.toBoxAdditive μ) J •
            (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
        ↑(Measure.toBoxAdditive μ) J * ε'
⊢ ↑(Measure.toBoxAdditive μ) I * ε' ≤ ε
exact hε.le
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
⊢ ‖↑(Measure.toBoxAdditive μ) J •
        (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
    ↑(Measure.toBoxAdditive μ) J * ε'
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
⊢ ∀ (J : Box ι),
    J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition →
      ‖↑(Measure.toBoxAdditive μ) J •
            (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
        ↑(Measure.toBoxAdditive μ) J * ε'
intro J hJ
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ ‖↑(Measure.toBoxAdditive μ) J •
        (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
    ↑(Measure.toBoxAdditive μ) J * ε'
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
⊢ ‖↑(Measure.toBoxAdditive μ) J •
        (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
    ↑(Measure.toBoxAdditive μ) J * ε'
have : 0 ≤ μ.toBoxAdditive J := ENNReal.toReal_nonneg
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ ↑(Measure.toBoxAdditive μ) J *
      dist (f (tag (infPrepartition π₁ π₂.toPrepartition) J)) (f (tag (infPrepartition π₂ π₁.toPrepartition) J)) ≤
    ↑(Measure.toBoxAdditive μ) J * ε'
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ ‖↑(Measure.toBoxAdditive μ) J •
        (f (tag (infPrepartition π₁ π₂.toPrepartition) J) - f (tag (infPrepartition π₂ π₁.toPrepartition) J))‖ ≤
    ↑(Measure.toBoxAdditive μ) J * ε'
rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg this, ← dist_eq_norm]
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ dist (f (tag (infPrepartition π₁ π₂.toPrepartition) J)) (f (tag (infPrepartition π₂ π₁.toPrepartition) J)) ≤ ε'
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ ↑(Measure.toBoxAdditive μ) J *
      dist (f (tag (infPrepartition π₁ π₂.toPrepartition) J)) (f (tag (infPrepartition π₂ π₁.toPrepartition) J)) ≤
    ↑(Measure.toBoxAdditive μ) J * ε'
refine' mul_le_mul_of_nonneg_left _ this
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ dist (tag (infPrepartition π₁ π₂.toPrepartition) J) (tag (infPrepartition π₂ π₁.toPrepartition) J) ≤ δ
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ dist (f (tag (infPrepartition π₁ π₂.toPrepartition) J)) (f (tag (infPrepartition π₂ π₁.toPrepartition) J)) ≤ ε'
refine' Hδ _ (TaggedPrepartition.tag_mem_Icc _ _) _ (TaggedPrepartition.tag_mem_Icc _ _) _
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ dist (tag (infPrepartition π₁ π₂.toPrepartition) J) (tag (infPrepartition π₂ π₁.toPrepartition) J) ≤ δ / 2 + δ / 2
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ dist (tag (infPrepartition π₁ π₂.toPrepartition) J) (tag (infPrepartition π₂ π₁.toPrepartition) J) ≤ δ
rw [← add_halves δ]
case refine'_1
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ Prepartition.biUnionIndex π₁.toPrepartition (fun J => Prepartition.restrict π₂.toPrepartition J) J ∈ π₁

case refine'_2
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ J.upper ∈
    ↑Box.Icc (Prepartition.biUnionIndex π₁.toPrepartition (fun J => Prepartition.restrict π₂.toPrepartition J) J)

case refine'_3
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ Prepartition.biUnionIndex π₂.toPrepartition (fun J => Prepartition.restrict π₁.toPrepartition J) J ∈ π₂

case refine'_4
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ J.upper ∈
    ↑Box.Icc (Prepartition.biUnionIndex π₂.toPrepartition (fun J => Prepartition.restrict π₁.toPrepartition J) J)
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ dist (tag (infPrepartition π₁ π₂.toPrepartition) J) (tag (infPrepartition π₂ π₁.toPrepartition) J) ≤ δ / 2 + δ / 2
refine' (dist_triangle_left _ _ J.upper).trans (add_le_add (h₁.1 _ _ _) (h₂.1 _ _ _))
no goals
case refine'_1
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ Prepartition.biUnionIndex π₁.toPrepartition (fun J => Prepartition.restrict π₂.toPrepartition J) J ∈ π₁
exact Prepartition.biUnionIndex_mem _ hJ
no goals
case refine'_2
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ J.upper ∈
    ↑Box.Icc (Prepartition.biUnionIndex π₁.toPrepartition (fun J => Prepartition.restrict π₂.toPrepartition J) J)
exact Box.le_iff_Icc.1 (Prepartition.le_biUnionIndex _ hJ) J.upper_mem_Icc
case refine'_3
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₂.toPrepartition ⊓ π₁.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ Prepartition.biUnionIndex π₂.toPrepartition (fun J => Prepartition.restrict π₁.toPrepartition J) J ∈ π₂
case refine'_3
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ Prepartition.biUnionIndex π₂.toPrepartition (fun J => Prepartition.restrict π₁.toPrepartition J) J ∈ π₂
rw [_root_.inf_comm] at hJ
no goals
case refine'_3
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₂.toPrepartition ⊓ π₁.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ Prepartition.biUnionIndex π₂.toPrepartition (fun J => Prepartition.restrict π₁.toPrepartition J) J ∈ π₂
exact Prepartition.biUnionIndex_mem _ hJ
case refine'_4
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₂.toPrepartition ⊓ π₁.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ J.upper ∈
    ↑Box.Icc (Prepartition.biUnionIndex π₂.toPrepartition (fun J => Prepartition.restrict π₁.toPrepartition J) J)
case refine'_4
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₁.toPrepartition ⊓ π₂.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ J.upper ∈
    ↑Box.Icc (Prepartition.biUnionIndex π₂.toPrepartition (fun J => Prepartition.restrict π₁.toPrepartition J) J)
rw [_root_.inf_comm] at hJ
no goals
case refine'_4
ι : Type u
E : Type v
F : Type w
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
I✝ J✝ : Box ι
π : TaggedPrepartition I✝
inst✝² : Fintype ι
l : IntegrationParams
f✝ g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
y y' : F
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
hc : ContinuousOn f (↑Box.Icc I)
μ : MeasureTheory.Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
huc :
  ∀ (ε : ℝ),
    ε > 0 →
      ∃ δ, δ > 0 ∧ ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε
ε : ℝ
ε0 : ε > 0
ε' : ℝ
ε0' : 0 < ε'
hε : ↑(Measure.toBoxAdditive μ) I * ε' < ε
δ : ℝ
δ0 : 0 < δ
Hδ : ∀ (x : ι → ℝ), x ∈ ↑Box.Icc I → ∀ (y : ι → ℝ), y ∈ ↑Box.Icc I → dist x y ≤ δ → dist (f x) (f y) ≤ ε'
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : MemBaseSet l I c₁ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₁) π₁
h₁p : IsPartition π₁
h₂ : MemBaseSet l I c₂ ((fun x x => { val := δ / 2, property := (_ : 0 < δ / 2) }) c₂) π₂
h₂p : IsPartition π₂
J : Box ι
hJ : J ∈ π₂.toPrepartition ⊓ π₁.toPrepartition
this : 0 ≤ ↑(Measure.toBoxAdditive μ) J
⊢ J.upper ∈
    ↑Box.Icc (Prepartition.biUnionIndex π₂.toPrepartition (fun J => Prepartition.restrict π₁.toPrepartition J) J)
exact Box.le_iff_Icc.1 (Prepartition.le_biUnionIndex _ hJ) J.upper_mem_Icc