ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>LinearOrderedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module E F<VAR>IsScalarTower 𝕜 E F<VAR>SMulCommClass 𝕜 E F<VAR>OrderedSMul 𝕜 E<VAR>OrderedSMul 𝕜 F<VAR>OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>LinearOrderedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module E F<VAR>IsScalarTower 𝕜 E F<VAR>SMulCommClass 𝕜 E F<VAR>OrderedSMul 𝕜 E<VAR>OrderedSMul 𝕜 F<VAR>OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>LinearOrderedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module E F<VAR>IsScalarTower 𝕜 E F<VAR>SMulCommClass 𝕜 E F<VAR>OrderedSMul 𝕜 F<VAR>OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>LinearOrderedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module E F<VAR>IsScalarTower 𝕜 E F<VAR>SMulCommClass 𝕜 E F<VAR>OrderedSMul 𝕜 F<VAR>OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>LinearOrderedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module E F<VAR>IsScalarTower 𝕜 E F<VAR>SMulCommClass 𝕜 E F<VAR>OrderedSMul 𝕜 E<VAR>OrderedSMul 𝕜 F<VAR>OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>LinearOrderedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module E F<VAR>IsScalarTower 𝕜 E F<VAR>SMulCommClass 𝕜 E F<VAR>OrderedSMul 𝕜 E<VAR>OrderedSMul 𝕜 F<VAR>OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>LinearOrderedAddCommGroup F<VAR>Module 𝕜 E<VAR>Module 𝕜 F<VAR>Module E F<VAR>IsScalarTower 𝕜 E F<VAR>SMulCommClass 𝕜 E F<VAR>OrderedSMul 𝕜 F<VAR>OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f * g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f * g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f * g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f * g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f * g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f * g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f * g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f g : 𝕜 → E<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedCommRing 𝕜<VAR>LinearOrderedCommRing E<VAR>Module 𝕜 E<VAR>OrderedSMul 𝕜 E<VAR>s : Set 𝕜<VAR>IsScalarTower 𝕜 E E<VAR>SMulCommClass 𝕜 E E<VAR>f : 𝕜 → E<VAR>hf : ConvexOn 𝕜 s f<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>n : ℕ<GOAL>ConvexOn 𝕜 s (f ^ n)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedCommRing 𝕜<VAR>n : ℕ<GOAL>ConvexOn 𝕜 (Set.Ici 0) fun x => x ^ n
<VAR>𝕜 : Type u_1<VAR>LinearOrderedCommRing 𝕜<VAR>n : ℕ<VAR>hn : Even n<GOAL>ConvexOn 𝕜 Set.univ fun x => x ^ n
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>n : ℤ<GOAL>ConvexOn 𝕜 (Set.Ioi 0) fun x => x ^ n
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x<VAR>dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>hdom : f.domain ≠ ⊤<GOAL>∃ g, f < g ∧ ∀ (x : ↥g.domain), ↑x ∈ s → 0 ≤ ↑g x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>p : E →ₗ.[ℝ] ℝ<VAR>hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x<VAR>hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<GOAL>∃ q ≥ p, q.domain = ⊤ ∧ ∀ (x : ↥q.domain), ↑x ∈ s → 0 ≤ ↑q x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x<VAR>dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ x ∈ s, 0 ≤ g x
<VAR>E : Type u_2<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>N : E → ℝ<VAR>N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x<VAR>N_add : ∀ (x y : E), N (x + y) ≤ N x + N y<VAR>hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
<VAR>β : Type u_2<VAR>OrderedAddCommGroup β<VAR>Module ℝ β<VAR>OrderedSMul ℝ β<VAR>f : ℝ → β<VAR>a b : ℝ<VAR>a_lt_b : a < b<VAR>h_local_min : IsLocalMinOn f (Set.Icc a b) a<VAR>h_conv : ConvexOn ℝ (Set.Icc a b) f<GOAL>IsMinOn f (Set.Icc a b) a
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module ℝ E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>OrderedAddCommGroup β<VAR>Module ℝ β<VAR>OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmin : IsLocalMinOn f s a<VAR>h_conv : ConvexOn ℝ s f<GOAL>IsMinOn f s a
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module ℝ E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>OrderedAddCommGroup β<VAR>Module ℝ β<VAR>OrderedSMul ℝ β<VAR>s : Set E<VAR>f : E → β<VAR>a : E<VAR>a_in_s : a ∈ s<VAR>h_localmax : IsLocalMaxOn f s a<VAR>h_conc : ConcaveOn ℝ s f<GOAL>IsMaxOn f s a
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module ℝ E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>OrderedAddCommGroup β<VAR>Module ℝ β<VAR>OrderedSMul ℝ β<VAR>f : E → β<VAR>a : E<VAR>h_local_min : IsLocalMin f a<VAR>h_conv : ConvexOn ℝ Set.univ f<VAR>x : E<GOAL>f a ≤ f x
<VAR>E : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup E<VAR>TopologicalSpace E<VAR>Module ℝ E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul ℝ E<VAR>OrderedAddCommGroup β<VAR>Module ℝ β<VAR>OrderedSMul ℝ β<VAR>f : E → β<VAR>a : E<VAR>h_local_max : IsLocalMax f a<VAR>h_conc : ConcaveOn ℝ Set.univ f<VAR>x : E<GOAL>f x ≤ f a
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<GOAL>BoxIntegral.integralSum f vol (π.biUnionTagged πi) = ∑ J ∈ π.boxes, BoxIntegral.integralSum f vol (πi J)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<VAR>hπi : ∀ J ∈ π, (πi J).IsPartition<GOAL>BoxIntegral.integralSum f vol (π.biUnionPrepartition πi) = BoxIntegral.integralSum f vol π
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>π' : BoxIntegral.Prepartition I<VAR>h : π'.IsPartition<GOAL>BoxIntegral.integralSum f vol (π.infPrepartition π') = BoxIntegral.integralSum f vol π
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>α : Type u_1<VAR>g : BoxIntegral.Box ι → α<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>∑ y ∈ Finset.image g π.boxes, BoxIntegral.integralSum f vol (π.filter fun x => g x = y) = BoxIntegral.integralSum f vol π
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h₁ : π₁.IsPartition<VAR>h₂ : π₂.IsPartition<GOAL>BoxIntegral.integralSum f vol π₁ - BoxIntegral.integralSum f vol π₂ = ∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes, ((vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) - (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)))
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>BoxIntegral.integralSum f vol (π₁.disjUnion π₂ h) = BoxIntegral.integralSum f vol π₁ + BoxIntegral.integralSum f vol π₂
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>BoxIntegral.integralSum (f + g) vol π = BoxIntegral.integralSum f vol π + BoxIntegral.integralSum g vol π
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>BoxIntegral.integralSum (-f) vol π = -BoxIntegral.integralSum f vol π
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>c : ℝ<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : BoxIntegral.TaggedPrepartition I<GOAL>BoxIntegral.integralSum (c • f) vol π = c • BoxIntegral.integralSum f vol π
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y : F<VAR>h : BoxIntegral.HasIntegral I l f vol y<GOAL>Filter.Tendsto (BoxIntegral.integralSum f vol) (l.toFilteriUnion I ⊤) (𝓝 y)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y : F<GOAL>BoxIntegral.HasIntegral I l f vol y ↔ ∀ ε > 0, ∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : BoxIntegral.TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (BoxIntegral.integralSum f vol π) y ≤ ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y : F<VAR>a : ℝ<VAR>h : ∀ (ε : ℝ), 0 < ε → ∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c : ℝ≥0) (π : BoxIntegral.TaggedPrepartition I), l.MemBaseSet I c (r c) π → π.IsPartition → dist (BoxIntegral.integralSum f vol π) y ≤ a * ε<GOAL>BoxIntegral.HasIntegral I l f vol y
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>CompleteSpace F<GOAL>BoxIntegral.Integrable I l f vol ↔ Cauchy (Filter.map (BoxIntegral.integralSum f vol) (l.toFilteriUnion I ⊤))
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>CompleteSpace F<GOAL>BoxIntegral.Integrable I l f vol ↔ ∀ ε > 0, ∃ r, (∀ (c : ℝ≥0), l.RCond (r c)) ∧ ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : BoxIntegral.TaggedPrepartition I), l.MemBaseSet I c₁ (r c₁) π₁ → π₁.IsPartition → l.MemBaseSet I c₂ (r c₂) π₂ → π₂.IsPartition → dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ≤ ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y : F<VAR>l₁ l₂ : BoxIntegral.IntegrationParams<VAR>h : BoxIntegral.HasIntegral I l₁ f vol y<VAR>hl : l₂ ≤ l₁<GOAL>BoxIntegral.HasIntegral I l₂ f vol y
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>h : BoxIntegral.Integrable I l f vol<GOAL>BoxIntegral.HasIntegral I l f vol (BoxIntegral.integral I l f vol)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>l' : BoxIntegral.IntegrationParams<VAR>h : BoxIntegral.Integrable I l f vol<VAR>hle : l' ≤ l<GOAL>BoxIntegral.Integrable I l' f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>h : BoxIntegral.HasIntegral I l f vol y<VAR>h' : BoxIntegral.HasIntegral I l f vol y'<GOAL>y = y'
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y : F<VAR>h : BoxIntegral.HasIntegral I l f vol y<GOAL>BoxIntegral.Integrable I l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y : F<VAR>h : BoxIntegral.HasIntegral I l f vol y<GOAL>BoxIntegral.integral I l f vol = y
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>h : BoxIntegral.HasIntegral I l f vol y<VAR>h' : BoxIntegral.HasIntegral I l g vol y'<GOAL>BoxIntegral.HasIntegral I l (f + g) vol (y + y')
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hf : BoxIntegral.Integrable I l f vol<VAR>hg : BoxIntegral.Integrable I l g vol<GOAL>BoxIntegral.Integrable I l (f + g) vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hf : BoxIntegral.Integrable I l f vol<VAR>hg : BoxIntegral.Integrable I l g vol<GOAL>BoxIntegral.integral I l (f + g) vol = BoxIntegral.integral I l f vol + BoxIntegral.integral I l g vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y : F<VAR>hf : BoxIntegral.HasIntegral I l f vol y<GOAL>BoxIntegral.HasIntegral I l (-f) vol (-y)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hf : BoxIntegral.Integrable I l f vol<GOAL>BoxIntegral.Integrable I l (-f) vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hf : BoxIntegral.Integrable I l (-f) vol<GOAL>BoxIntegral.Integrable I l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<GOAL>BoxIntegral.Integrable I l (-f) vol ↔ BoxIntegral.Integrable I l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<GOAL>BoxIntegral.integral I l (-f) vol = -BoxIntegral.integral I l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>h : BoxIntegral.HasIntegral I l f vol y<VAR>h' : BoxIntegral.HasIntegral I l g vol y'<GOAL>BoxIntegral.HasIntegral I l (f - g) vol (y - y')
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hf : BoxIntegral.Integrable I l f vol<VAR>hg : BoxIntegral.Integrable I l g vol<GOAL>BoxIntegral.Integrable I l (f - g) vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>hf : BoxIntegral.Integrable I l f vol<VAR>hg : BoxIntegral.Integrable I l g vol<GOAL>BoxIntegral.integral I l (f - g) vol = BoxIntegral.integral I l f vol - BoxIntegral.integral I l g vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c : E<GOAL>BoxIntegral.HasIntegral I l (fun x => c) vol ((vol I) c)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c : E<GOAL>BoxIntegral.integral I l (fun x => c) vol = (vol I) c
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>c : E<GOAL>BoxIntegral.Integrable I l (fun x => c) vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<GOAL>BoxIntegral.HasIntegral I l (fun x => 0) vol 0
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<GOAL>BoxIntegral.Integrable I l (fun x => 0) vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>l : BoxIntegral.IntegrationParams<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<GOAL>BoxIntegral.integral I l (fun x => 0) vol = 0