ι : 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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε
⊢ ∃ ia,
    (∀ (c : ℝ≥0), RCond l (ia c)) ∧
      ∀ (x : TaggedPrepartition I × TaggedPrepartition I),
        x ∈
            {π | ∃ c, MemBaseSet l I c (ia c) π} ×ˢ {π | ∃ c, MemBaseSet l I c (ia c) π} ∩
              {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd} →
          (integralSum f vol x.fst, integralSum f vol x.snd) ∈ {p | dist p.fst p.snd ≤ ε}
ι : 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
c c₁ c₂ : ℝ≥0
ε ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
⊢ Tendsto (fun π => (integralSum f vol π.fst, integralSum f vol π.snd))
    (toFilter l I ×ˢ toFilter l I ⊓ 𝓟 {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd}) (𝓤 F)
refine (((l.hasBasis_toFilter I).prod_self.inf_principal _).tendsto_iff
  uniformity_basis_dist_le).2 fun ε ε0 => ?_
ι : 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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
⊢ ∃ ia,
    (∀ (c : ℝ≥0), RCond l (ia c)) ∧
      ∀ (x : TaggedPrepartition I × TaggedPrepartition I),
        x ∈
            {π | ∃ c, MemBaseSet l I c (ia c) π} ×ˢ {π | ∃ c, MemBaseSet l I c (ia c) π} ∩
              {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd} →
          (integralSum f vol x.fst, integralSum f vol x.snd) ∈ {p | dist p.fst p.snd ≤ ε}
ι : 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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε
⊢ ∃ ia,
    (∀ (c : ℝ≥0), RCond l (ia c)) ∧
      ∀ (x : TaggedPrepartition I × TaggedPrepartition I),
        x ∈
            {π | ∃ c, MemBaseSet l I c (ia c) π} ×ˢ {π | ∃ c, MemBaseSet l I c (ia c) π} ∩
              {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd} →
          (integralSum f vol x.fst, integralSum f vol x.snd) ∈ {p | dist p.fst p.snd ≤ ε}
replace ε0 := half_pos ε0
ι : 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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
⊢ ∀ (x : TaggedPrepartition I × TaggedPrepartition I),
    x ∈
        {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π} ×ˢ
            {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π} ∩
          {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd} →
      (integralSum f vol x.fst, integralSum f vol x.snd) ∈ {p | dist p.fst p.snd ≤ ε}
ι : 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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
⊢ ∃ ia,
    (∀ (c : ℝ≥0), RCond l (ia c)) ∧
      ∀ (x : TaggedPrepartition I × TaggedPrepartition I),
        x ∈
            {π | ∃ c, MemBaseSet l I c (ia c) π} ×ˢ {π | ∃ c, MemBaseSet l I c (ia c) π} ∩
              {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd} →
          (integralSum f vol x.fst, integralSum f vol x.snd) ∈ {p | dist p.fst p.snd ≤ ε}
use h.convergenceR (ε / 2), h.convergenceR_cond (ε / 2)
case mk.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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁✝ π₂✝ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd}
h₁ : (π₁, π₂).fst ∈ {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π}
h₂ : (π₁, π₂).snd ∈ {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).fst, integralSum f vol (π₁, π₂).snd) ∈ {p | dist p.fst p.snd ≤ ε}
ι : 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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁ π₂ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
⊢ ∀ (x : TaggedPrepartition I × TaggedPrepartition I),
    x ∈
        {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π} ×ˢ
            {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π} ∩
          {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd} →
      (integralSum f vol x.fst, integralSum f vol x.snd) ∈ {p | dist p.fst p.snd ≤ ε}
rintro ⟨π₁, π₂⟩ ⟨⟨h₁, h₂⟩, hU⟩
case mk.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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁✝ π₂✝ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd}
h₁ : (π₁, π₂).fst ∈ {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π}
h₂ : (π₁, π₂).snd ∈ {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).fst, integralSum f vol (π₁, π₂).snd) ∈ {p | dist p.fst p.snd ≤ ε / 2 + ε / 2}
case mk.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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁✝ π₂✝ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd}
h₁ : (π₁, π₂).fst ∈ {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π}
h₂ : (π₁, π₂).snd ∈ {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).fst, integralSum f vol (π₁, π₂).snd) ∈ {p | dist p.fst p.snd ≤ ε}
rw [← add_halves ε]
no goals
case mk.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
c c₁ c₂ : ℝ≥0
ε✝ ε₁ ε₂ : ℝ
π₁✝ π₂✝ : TaggedPrepartition I
h : Integrable I l f vol
ε : ℝ
ε0 : 0 < ε / 2
π₁ π₂ : TaggedPrepartition I
hU : (π₁, π₂) ∈ {π | TaggedPrepartition.iUnion π.fst = TaggedPrepartition.iUnion π.snd}
h₁ : (π₁, π₂).fst ∈ {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π}
h₂ : (π₁, π₂).snd ∈ {π | ∃ c, MemBaseSet l I c (convergenceR h (ε / 2) c) π}
⊢ (integralSum f vol (π₁, π₂).fst, integralSum f vol (π₁, π₂).snd) ∈ {p | dist p.fst p.snd ≤ ε / 2 + ε / 2}
exact h.dist_integralSum_le_of_memBaseSet ε0 ε0 h₁.choose_spec h₂.choose_spec hU