ι : 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
π₀ : Prepartition I
⊢ Filter.map (integralSum f vol) (toFilteriUnion l I π₀) ×ˢ Filter.map (integralSum f vol) (toFilteriUnion l I π₀) ≤ 𝓤 F
ι : 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
π₀ : Prepartition I
⊢ Cauchy (Filter.map (integralSum f vol) (toFilteriUnion l I π₀))
refine' ⟨inferInstance, _⟩
ι : 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
π₀ : Prepartition I
⊢ Filter.map (fun p => (integralSum f vol p.fst, integralSum f vol p.snd))
      (toFilter l I ×ˢ toFilter l I ⊓
        𝓟
          ({π | TaggedPrepartition.iUnion π = Prepartition.iUnion π₀} ×ˢ
            {π | TaggedPrepartition.iUnion π = Prepartition.iUnion π₀})) ≤
    𝓤 F
ι : 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
π₀ : Prepartition I
⊢ Filter.map (integralSum f vol) (toFilteriUnion l I π₀) ×ˢ Filter.map (integralSum f vol) (toFilteriUnion l I π₀) ≤ 𝓤 F
rw [prod_map_map_eq, ← toFilter_inf_iUnion_eq, ← prod_inf_prod, prod_principal_principal]
no goals
ι : 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
π₀ : Prepartition I
⊢ Filter.map (fun p => (integralSum f vol p.fst, integralSum f vol p.snd))
      (toFilter l I ×ˢ toFilter l I ⊓
        𝓟
          ({π | TaggedPrepartition.iUnion π = Prepartition.iUnion π₀} ×ˢ
            {π | TaggedPrepartition.iUnion π = Prepartition.iUnion π₀})) ≤
    𝓤 F
exact h.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity.mono_left
  (inf_le_inf_left _ <| principal_mono.2 fun π h => h.1.trans h.2.symm)