Revision #1319 → #1835 · back to history
modifiedLine integral4ab2c3ff01e4
| Field | From #1319 | To #1835 |
|---|
| mathlib.decl | curveIntegral | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.MeasureTheory.Integral.CurveIntegral.Basic | — |
| note | `curveIntegral ω γ` integrates a 1-form along a path `γ`. | No general line integral over a curve is defined in Mathlib (no `curveIntegral` decl exists); only `intervalIntegral` over an interval and `circleIntegral` for circles. |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |
modifiedMesh of a partition7b6ae7fbe1f8
| Field | From #1319 | To #1835 |
|---|
| mathlib.module | Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction | Mathlib.Analysis.BoxIntegral.Partition.Basic |
modifiedUpper and lower bounds4c48510183a6
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Inequalities","snippet":"An integrable function f on [ a , b ] , is necessarily bounded on that interval"},{"type":"math_alttext","value":"{\\displaystyle m(b-a)\\leq \\int _{a}^{b}f(x)\\,dx\\leq M(b-a).}"}] | — |
modifiedInequalities between functionsac6559cc75c6
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Inequalities","snippet":"If f ( x ) ≤ g ( x ) for each x in [ a , b ] then each of the upper and lower sums of f is bounded above by the upper and lower sums, respectively, of g"},{"type":"math_alttext","value":"{\\displaystyle \\int _{a}^{b}f(x)\\,dx\\leq \\int _{a}^{b}g(x)\\,dx.}"},{"type":"math_alttext","value":"{\\displaystyle \\int _{a}^{b}f(x)\\,dx<\\int _{a}^{b}g(x)\\,dx.}"}] | — |
modifiedSubinterval inequalityd3b5f525baba
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Inequalities","snippet":"If [ c , d ] is a subinterval of [ a , b ] and f ( x ) is non-negative for all x , then"},{"type":"math_alttext","value":"{\\displaystyle \\int _{c}^{d}f(x)\\,dx\\leq \\int _{a}^{b}f(x)\\,dx.}"}] | — |
modifiedAbsolute value inequalityaeb50527cf46
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Inequalities","snippet":"If f is Riemann-integrable on [ a , b ] then the same is true for | f |"},{"type":"math_alttext","value":"{\\displaystyle (fg)(x)=f(x)g(x),\\;f^{2}(x)=(f(x))^{2},\\;|f|(x)=|f(x)|.}"},{"type":"math_alttext","value":"{\\displaystyle \\left|\\int _{a}^{b}f(x)\\,dx\\right|\\leq \\int _{a}^{b}|f(x)|\\,dx.}"},{"type":"math_alttext","value":"{\\displaystyle \\left(\\int _{a}^{b}(fg)(x)\\,dx\\right)^{2}\\leq \\left(\\int _{a}^{b}f(x)^{2}\\,dx\\right)\\left(\\int _{a}^{b}g(x)^{2}\\,dx\\right).}"}] | — |
modifiedCauchy–Schwarz inequality4bbdc27d794b
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Inequalities","snippet":"This inequality, known as the Cauchy–Schwarz inequality , plays a prominent role in Hilbert space theory"},{"type":"math_alttext","value":"{\\displaystyle (fg)(x)=f(x)g(x),\\;f^{2}(x)=(f(x))^{2},\\;|f|(x)=|f(x)|.}"},{"type":"math_alttext","value":"{\\displaystyle \\left|\\int _{a}^{b}f(x)\\,dx\\right|\\leq \\int _{a}^{b}|f(x)|\\,dx.}"},{"type":"math_alttext","value":"{\\displaystyle \\left(\\int _{a}^{b}(fg)(x)\\,dx\\right)^{2}\\leq \\left(\\int _{a}^{b}f(x)^{2}\\,dx\\right)\\left(\\int _{a}^{b}g(x)^{2}\\,dx\\right).}"}] | — |
| mathlib.decl | MeasureTheory.lintegral_mul_le_Lp_mul_Lq | ENNReal.lintegral_mul_le_Lp_mul_Lq |
modifiedHölder's inequalityfe228be3c798
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Inequalities","snippet":"Then the functions | f | p and | g | q are also integrable and the following Hölder's inequality holds"},{"type":"math_alttext","value":"{\\displaystyle \\left|\\int f(x)g(x)\\,dx\\right|\\leq \\left(\\int \\left|f(x)\\right|^{p}\\,dx\\right)^{1/p}\\left(\\int \\left|g(x)\\right|^{q}\\,dx\\right)^{1/q}.}"}] | — |
| mathlib.decl | MeasureTheory.lintegral_mul_le_Lp_mul_Lq | ENNReal.lintegral_mul_le_Lp_mul_Lq |
modifiedMinkowski inequality2c12f7057d7a
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Inequalities","snippet":"Then | f | p , | g | p and | f + g | p are also Riemann-integrable and the following Minkowski inequality holds"},{"type":"math_alttext","value":"{\\displaystyle \\left(\\int \\left|f(x)+g(x)\\right|^{p}\\,dx\\right)^{1/p}\\leq \\left(\\int \\left|f(x)\\right|^{p}\\,dx\\right)^{1/p}+\\left(\\int \\left|g(x)\\right|^{p}\\,dx\\right)^{1/p}.}"}] | — |
| mathlib.decl | MeasureTheory.lintegral_Lp_add_le | ENNReal.lintegral_Lp_add_le |
addedIntegral over a degenerate interval is zero154e370140b0
modifiedLine integral97b49efd2d0d
| Field | From #1319 | To #1835 |
|---|
| mathlib.decl | curveIntegral | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.MeasureTheory.Integral.CurveIntegral.Basic | — |
| note | `curveIntegral ω γ` integrates a 1-form along a path. | No general line integral over a curve is defined in Mathlib; only `intervalIntegral` (over an interval) and `circleIntegral` (over a circle) exist. |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |
modifiedContour integral0512b1b3f624
| Field | From #1319 | To #1835 |
|---|
| note | Mathlib formalizes `circleIntegral` (and `curveIntegral`); a generic complex contour integral is not separately defined. | Mathlib formalizes `circleIntegral`; a generic complex contour integral is not separately defined. |
| provenance | ai | ai-moderated |
modifiedDifferential one-formc899c8639f86
| Field | From #1319 | To #1835 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.DifferentialForm.Basic | Mathlib.Topology.Algebra.Module.Alternating.Basic |
| note | Differential 1-forms are represented as fields `E → E [⋀^Fin 1]→L[𝕜] F`; no dedicated `OneForm` abbreviation. | Differential 1-forms are represented as fields valued in `E [⋀^Fin 1]→L[𝕜] F`; no dedicated `OneForm` abbreviation. |
| provenance | ai | ai-moderated |
modifiedDifferential two-form7a73cff86e61
| Field | From #1319 | To #1835 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.DifferentialForm.Basic | Mathlib.Topology.Algebra.Module.Alternating.Basic |
| note | 2-forms are encoded as `E → E [⋀^Fin 2]→L[𝕜] F`; no dedicated `TwoForm` definition. | 2-forms are encoded as fields valued in `E [⋀^Fin 2]→L[𝕜] F`; no dedicated `TwoForm` definition. |
| provenance | ai | ai-moderated |
modifiedProbability density integral equals 150a6745271df
| Field | From #1319 | To #1835 |
|---|
| mathlib.module | Mathlib.Probability.Density.Basic | Mathlib.Probability.Density |
modifiedVolume by disc integrationb46624e1ebd2
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Applications","snippet":"The volume of a three-dimensional object such as a disc or washer can be computed by disc integration using the equation for the volume of a cylinder"},{"type":"math_alttext","value":"{\\displaystyle \\pi \\int _{a}^{b}f^{2}(x)\\,dx.}"}] | — |
modifiedDisplacement from velocity60b0900647d1
| Field | From #1319 | To #1835 |
|---|
| anchors | [{"section":"Applications","snippet":"in rectilinear motion , the displacement of an object over the time interval"},{"type":"math_alttext","value":"{\\displaystyle \\pi \\int _{a}^{b}f^{2}(x)\\,dx.}"}] | — |
modifiedTrapezoidal rule493548a5f16c
| Field | From #1319 | To #1835 |
|---|
| mathlib.decl | trapezoidal_integral | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule | — |
| note | `trapezoidal_integral f N a b` defines the composite trapezoidal approximation. | No dedicated trapezoidal-rule definition exists in Mathlib (no `trapezoidal_integral` decl). |
| provenance | ai | ai-moderated |
| status | formalized | not_formalized |