ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>Fintype ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>hr₁ : π.IsSubordinate r₁<VAR>h : ∀ x ∈ BoxIntegral.Box.Icc I, r₁ x ≤ r₂ x<GOAL>π.IsSubordinate r₂
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>Fintype ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>h : π.IsSubordinate r<VAR>hJ : J ∈ π.boxes<GOAL>Metric.diam (BoxIntegral.Box.Icc J) ≤ 2 * ↑(r (π.tag J))
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>hJ : J ≤ I<VAR>x : ι → ℝ<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I J hJ x h).tag = fun x_1 => x
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>hJ : J ≤ I<VAR>x : ι → ℝ<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I J hJ x h).boxes.val = {J}
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>J' : BoxIntegral.Box ι<VAR>hJ : J ≤ I<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>J' ∈ BoxIntegral.TaggedPrepartition.single I J hJ x h ↔ J' = J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>hJ : J ≤ I<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I J hJ x h).IsPartition ↔ J = I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I I ⋯ x h).IsPartition
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>p : (ι → ℝ) → BoxIntegral.Box ι → Prop<VAR>hJ : J ≤ I<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(∀ J' ∈ BoxIntegral.TaggedPrepartition.single I J hJ x h, p ((BoxIntegral.TaggedPrepartition.single I J hJ x h).tag J') J') ↔ p x J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>hJ : J ≤ I<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I J hJ x h).IsHenstock ↔ x ∈ BoxIntegral.Box.Icc J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I I ⋯ x h).IsHenstock
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>Fintype ι<VAR>hJ : J ≤ I<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I J hJ x h).IsSubordinate r ↔ BoxIntegral.Box.Icc J ⊆ Metric.closedBall x ↑(r x)
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>hJ : J ≤ I<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I J hJ x h).iUnion = ↑J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).boxes = π₁.boxes ∪ π₂.boxes
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>J ∈ π₁.disjUnion π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<VAR>hJ : J ∈ π₁<GOAL>(π₁.disjUnion π₂ h).tag J = π₁.tag J
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<VAR>hJ : J ∈ π₂<GOAL>(π₁.disjUnion π₂ h).tag J = π₂.tag J
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>Fintype ι<VAR>h₁ : π₁.IsSubordinate r<VAR>h₂ : π₂.IsSubordinate r<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).IsSubordinate r
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>h₁ : π₁.IsHenstock<VAR>h₂ : π₂.IsHenstock<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).IsHenstock
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>h : J ∈ π<GOAL>J.distortion ≤ π.distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>c : ℝ≥0<GOAL>π.distortion ≤ c ↔ ∀ J ∈ π, J.distortion ≤ c
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>π : BoxIntegral.Prepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J<GOAL>(π.biUnionTagged πi).distortion = π.boxes.sup fun J => (πi J).distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J<GOAL>(π.biUnionPrepartition πi).distortion = π.boxes.sup fun J => (πi J).distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π₁ π₂ : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>h : Disjoint π₁.iUnion π₂.iUnion<GOAL>(π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>c : ℝ≥0<VAR>h₁ : π.boxes.Nonempty<VAR>h₂ : ∀ J ∈ π, J.distortion = c<GOAL>π.distortion = c
<VAR>ι : Type u_1<VAR>I J : BoxIntegral.Box ι<VAR>x : ι → ℝ<VAR>Fintype ι<VAR>hJ : J ≤ I<VAR>h : x ∈ BoxIntegral.Box.Icc I<GOAL>(BoxIntegral.TaggedPrepartition.single I J hJ x h).distortion = J.distortion
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.TaggedPrepartition I<VAR>Fintype ι<VAR>p : BoxIntegral.Box ι → Prop<GOAL>(π.filter p).distortion ≤ π.distortion
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>x : E<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>T.rayleighQuotient (c • x) = T.rayleighQuotient x
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>T.rayleighQuotient '' {0}ᶜ = T.rayleighQuotient '' Metric.sphere 0 r
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>⨆ x, T.rayleighQuotient ↑x = ⨆ x, T.rayleighQuotient ↑x
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>T : E →L[𝕜] E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>⨅ x, T.rayleighQuotient ↑x = ⨅ x, T.rayleighQuotient ↑x
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>T : F →L[ℝ] F<VAR>hT : (↑T).IsSymmetric<VAR>x₀ : F<GOAL>HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ) (T x₀)) x₀
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀<GOAL>∃ a b, (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ F<VAR>CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀<GOAL>T x₀ = T.rayleighQuotient x₀ • x₀
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀<GOAL>T x₀ = ↑(T.rayleighQuotient x₀) • x₀
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀<GOAL>Module.End.HasEigenvector (↑T) (↑(T.rayleighQuotient x₀)) x₀
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMaxOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀<GOAL>Module.End.HasEigenvector (↑T) (↑(⨆ x, T.rayleighQuotient ↑x)) x₀
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMinOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀<GOAL>Module.End.HasEigenvector (↑T) (↑(⨅ x, T.rayleighQuotient ↑x)) x₀
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>Module.End.HasEigenvalue T ↑(⨆ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>_i : Nontrivial E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<GOAL>Module.End.HasEigenvalue T ↑(⨅ x, RCLike.re ⟪T ↑x, ↑x⟫_𝕜 / ‖↑x‖ ^ 2)
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>hT' : ∀ (μ : 𝕜), Module.End.eigenspace T μ = ⊥<GOAL>Subsingleton E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<GOAL>p.leftInv i 0 = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<GOAL>p.leftInv i 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<GOAL>p.removeZero.leftInv i = p.leftInv i
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<GOAL>(p.leftInv i).comp p = FormalMultilinearSeries.id 𝕜 E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<GOAL>p.rightInv i 0 = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<GOAL>p.rightInv i 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<GOAL>p.removeZero.rightInv i = p.rightInv i
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 F E<VAR>v : Fin n → F<GOAL>(p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x => (q n) v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>n : ℕ<VAR>v : Fin (n + 2) → F<GOAL>∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (FormalMultilinearSeries.applyComposition (fun k => if k < n + 2 then p.rightInv i k else 0) c v) = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) ((p.rightInv i).applyComposition c v)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<VAR>h0 : p 0 = 0<GOAL>p.comp (p.rightInv i) = FormalMultilinearSeries.id 𝕜 F
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>p.rightInv i n = -(↑i.symm).compContinuousMultilinearMap (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i) c)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<VAR>h0 : p 0 = 0<GOAL>p.leftInv i = p.rightInv i
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<GOAL>p.leftInv i = p.rightInv i
<VAR>n : ℕ<VAR>p : ℕ → ℝ<VAR>hp : ∀ (k : ℕ), 0 ≤ p k<VAR>r a : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<GOAL>∑ k ∈ Finset.Ico 2 (n + 1), a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, p (c.blocksFun j) ≤ ∑ j ∈ Finset.Ico 2 (n + 1), r ^ j * (∑ k ∈ Finset.Ico 1 n, a ^ k * p k) ^ j
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>hn : 2 ≤ n + 1<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>r a C : ℝ<VAR>hr : 0 ≤ r<VAR>ha : 0 ≤ a<VAR>hC : 0 ≤ C<VAR>hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n<GOAL>∑ k ∈ Finset.Ico 1 (n + 1), a ^ k * ‖p.rightInv i k‖ ≤ ‖↑i.symm‖ * a + ‖↑i.symm‖ * C * ∑ k ∈ Finset.Ico 2 (n + 1), (r * ∑ j ∈ Finset.Ico 1 n, a ^ j * ‖p.rightInv i j‖) ^ k
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>hp : 0 < p.radius<GOAL>0 < (p.rightInv i).radius
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℂ 𝕜 E<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>f : SchwartzMap V E<GOAL>⇑((SchwartzMap.fourierTransformCLM 𝕜) f) = 𝓕 ⇑f
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℂ 𝕜 E<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>CompleteSpace E<VAR>f : SchwartzMap V E<GOAL>⇑((SchwartzMap.fourierTransformCLE 𝕜) f) = 𝓕 ⇑f
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>NormedSpace 𝕜 E<VAR>SMulCommClass ℂ 𝕜 E<VAR>V : Type u_3<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>MeasurableSpace V<VAR>BorelSpace V<VAR>CompleteSpace E<VAR>f : SchwartzMap V E<GOAL>⇑((SchwartzMap.fourierTransformCLE 𝕜).symm f) = 𝓕⁻ ⇑f
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>μ (BoxIntegral.Box.Icc I) < ⊤
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>μ ↑I < ⊤
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Countable ι<GOAL>MeasurableSet ↑I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Countable ι<GOAL>MeasurableSet (BoxIntegral.Box.Icc I)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Countable ι<GOAL>MeasurableSet (BoxIntegral.Box.Ioo I)
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<GOAL>↑I =ᵐ[MeasureTheory.volume] BoxIntegral.Box.Icc I
<VAR>ι : Type u_1<VAR>I : BoxIntegral.Box ι<VAR>Fintype ι<GOAL>BoxIntegral.Box.Ioo I =ᵐ[MeasureTheory.volume] BoxIntegral.Box.Icc I
<VAR>ι : Type u_1<VAR>Finite ι<VAR>I : BoxIntegral.Box ι<VAR>π : BoxIntegral.Prepartition I<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>(μ π.iUnion).toReal = ∑ J ∈ π.boxes, (μ ↑J).toReal
<VAR>ι : Type u_1<VAR>Finite ι<VAR>μ : MeasureTheory.Measure (ι → ℝ)<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>J : BoxIntegral.Box ι<GOAL>μ.toBoxAdditive J = (μ ↑J).toReal
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<GOAL>MeasureTheory.volume.toBoxAdditive I = ∏ i : ι, (I.upper i - I.lower i)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>I : BoxIntegral.Box ι<GOAL>(MeasureTheory.volume ↑I).toReal = ∏ i : ι, (I.upper i - I.lower i)
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>I : BoxIntegral.Box (Fin (n + 1))<GOAL>(∏ j : Fin n, ((I.face i).upper j - (I.face i).lower j)) * (I.upper i - I.lower i) = ∏ j : Fin (n + 1), (I.upper j - I.lower j)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>I : BoxIntegral.Box ι<VAR>x : E<GOAL>(BoxIntegral.BoxAdditiveMap.volume I) x = (∏ j : ι, (I.upper j - I.lower j)) • x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<GOAL>gramSchmidt 𝕜 f n = f n - ∑ i ∈ Finset.Iio n, ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 f i})) (f n))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<GOAL>f n = gramSchmidt 𝕜 f n + ∑ i ∈ Finset.Iio n, ↑((orthogonalProjection (Submodule.span 𝕜 {gramSchmidt 𝕜 f i})) (f n))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<GOAL>f n = gramSchmidt 𝕜 f n + ∑ i ∈ Finset.Iio n, (⟪gramSchmidt 𝕜 f i, f n⟫_𝕜 / ↑‖gramSchmidt 𝕜 f i‖ ^ 2) • gramSchmidt 𝕜 f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_4<VAR>LinearOrder ι<VAR>LocallyFiniteOrder ι<VAR>OrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>gramSchmidt 𝕜 f ⊥ = f ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>a b : ι<VAR>h₀ : a ≠ b<GOAL>⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>Pairwise fun a b => ⟪gramSchmidt 𝕜 f a, gramSchmidt 𝕜 f b⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<GOAL>⟪gramSchmidt 𝕜 v j, v i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>f i ∈ Submodule.span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>j i : ι<GOAL>i ≤ j → gramSchmidt 𝕜 f i ∈ Submodule.span 𝕜 (f '' Set.Iic j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>c : ι<GOAL>Submodule.span 𝕜 (gramSchmidt 𝕜 f '' Set.Iic c) = Submodule.span 𝕜 (f '' Set.Iic c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>c : ι<GOAL>Submodule.span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio c) = Submodule.span 𝕜 (f '' Set.Iio c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>Submodule.span 𝕜 (Set.range (gramSchmidt 𝕜 f)) = Submodule.span 𝕜 (Set.range f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>hf : Pairwise fun i j => ⟪f i, f j⟫_𝕜 = 0<GOAL>gramSchmidt 𝕜 f = f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent (ι := { x // x ∈ Set.Iic n }) 𝕜 (f ∘ Subtype.val)<GOAL>gramSchmidt 𝕜 f n ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent 𝕜 f<GOAL>gramSchmidt 𝕜 f n ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>i j : ι<VAR>hij : i < j<VAR>b : Basis ι 𝕜 E<GOAL>(b.repr (gramSchmidt 𝕜 (⇑b) i)) j = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>h₀ : LinearIndependent 𝕜 f<GOAL>LinearIndependent 𝕜 (gramSchmidt 𝕜 f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>b : Basis ι 𝕜 E<GOAL>⇑(gramSchmidtBasis b) = gramSchmidt 𝕜 ⇑b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent (ι := { x // x ∈ Set.Iic n }) 𝕜 (f ∘ Subtype.val)<GOAL>‖gramSchmidtNormed 𝕜 f n‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>h₀ : LinearIndependent 𝕜 f<GOAL>‖gramSchmidtNormed 𝕜 f n‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>hn : gramSchmidtNormed 𝕜 f n ≠ 0<GOAL>‖gramSchmidtNormed 𝕜 f n‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>h₀ : LinearIndependent 𝕜 f<GOAL>Orthonormal 𝕜 (gramSchmidtNormed 𝕜 f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>LinearOrder ι<VAR>LocallyFiniteOrderBot ι<VAR>IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<GOAL>Orthonormal 𝕜 fun i => gramSchmidtNormed 𝕜 f ↑i