Convergence of integrals of bounded 1-forms #
Bounded continuous 1-forms preserve convergence of actual integrals along absolutely
continuous curves under uniform convergence of curves and L¹ convergence of derivatives.
The statements use the raw-curve integral ∫ t in a..b, ω (γ t) (deriv γ t).
For a Path, Mathlib's curveIntegral_eq_intervalIntegral_deriv gives this representation.
No uniform bound on the approximating velocities is assumed.
theorem
AbsolutelyContinuousOnInterval.intervalIntegrable_oneForm_of_continuous_bounded
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{a b : ℝ}
{γ : ℝ → E}
{ω : E → E →L[ℝ] F}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hω : Continuous ω)
{C : ℝ}
(hbound : ∀ (z : E), ‖ω z‖ ≤ C)
:
IntervalIntegrable (fun (t : ℝ) => (ω (γ t)) (deriv γ t)) MeasureTheory.volume a b
A bounded continuous 1-form is integrable along an absolutely continuous curve.
theorem
AbsolutelyContinuousOnInterval.tendsto_integral_oneForm_of_tendstoUniformlyOn
{E : Type u_1}
{F : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{a b : ℝ}
{γ : ℝ → E}
{ω : E → E →L[ℝ] F}
{γn : ℕ → ℝ → E}
(hγ : AbsolutelyContinuousOnInterval γ a b)
(hγn : ∀ (n : ℕ), AbsolutelyContinuousOnInterval (γn n) a b)
(hab : a ≤ b)
(hω : Continuous ω)
{C : ℝ}
(hbound : ∀ (z : E), ‖ω z‖ ≤ C)
(hconv : TendstoUniformlyOn γn γ Filter.atTop (Set.Icc a b))
(hdconv : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ) in a..b, ‖deriv (γn n) t - deriv γ t‖) Filter.atTop (nhds 0))
:
Uniform convergence of AC curves and L¹ convergence of their derivatives imply
convergence of the raw integrals ∫ t in a..b, ω (γ t) (deriv γ t)
of any bounded continuous 1-form.