Integrals over closed rectangles in the plane

Over a closed rectangle [a₁, b₁] × [a₂, b₂] in ℝ × ℝ, the fundamental theorem of calculus in one coordinate computes the integral of a partial derivative from the values on two opposite sides; in particular, a partial derivative of a function which takes the same values on the two opposite sides of the rectangle integrates to zero. Together with the vanishing of a continuous nonnegative function with zero integral, this is how energy identities on a fundamental domain of a doubly (twisted) periodic map are used.

Main declarations

• TauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_fst, TauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_snd: the integral of a partial derivative is the integral of the difference of the values on the two opposite sides.
• TauCeti.setIntegral_rect_eq_zero_of_hasDerivAt_fst, TauCeti.setIntegral_rect_eq_zero_of_hasDerivAt_snd: a partial derivative of a function with equal values on the two opposite sides integrates to zero over the rectangle.
• TauCeti.eqOn_zero_of_setIntegral_rect_eq_zero: a continuous nonnegative function with zero integral over a nondegenerate rectangle vanishes on it.
• TauCeti.setIntegral_Icc_prod_le_of_comp_add_le: comparison of the integrals of f and M over a translated strip [c + L, d + L] × I and the original one, when f (z + (L, 0)) ≤ M z.
• TauCeti.setIntegral_rect_le_mul_of_forall_setIntegral_le: an inequality between the integrals over the vertical segments {s} × [a₂, b₂] integrates to the same inequality over the rectangle.
• TauCeti.neg_mul_setIntegral_le_setIntegral_deriv_mul: for a monotone C¹ profile β and -B(t) ≤ f, the lower bound -(β(b₁) - β(a₁)) ∫ B ≤ ∫∫ β'(s) f.

theorem TauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_fst {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a₁ b₁ a₂ b₂ : ℝ} {Φ φ : ℝ × ℝ → E} (hφ : Continuous φ) (hΦ : ∀ (s t : ℝ), HasDerivAt (fun (s : ℝ) => Φ (s, t)) (φ (s, t)) s) (hab : a₁ ≤ b₁) : ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, φ z = ∫ (t : ℝ) in Set.Icc a₂ b₂, Φ (b₁, t) - Φ (a₁, t)

The fundamental theorem of calculus in the first coordinate. The integral of a continuous partial derivative φ = ∂₁ Φ over the rectangle [a₁, b₁] × [a₂, b₂] is the integral over [a₂, b₂] of the difference of the values of Φ on the two vertical sides.

theorem TauCeti.setIntegral_rect_eq_zero_of_hasDerivAt_fst {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a₁ b₁ a₂ b₂ : ℝ} {Φ φ : ℝ × ℝ → E} (hφ : Continuous φ) (hΦ : ∀ (s t : ℝ), HasDerivAt (fun (s : ℝ) => Φ (s, t)) (φ (s, t)) s) (hper : ∀ (t : ℝ), Φ (b₁, t) = Φ (a₁, t)) : ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, φ z = 0

A derivative in the first coordinate of a function with equal values on the vertical sides {a₁} × ℝ and {b₁} × ℝ integrates to zero over the rectangle [a₁, b₁] × [a₂, b₂].

theorem TauCeti.setIntegral_rect_eq_setIntegral_sub_of_hasDerivAt_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a₁ b₁ a₂ b₂ : ℝ} {Φ φ : ℝ × ℝ → E} (hφ : Continuous φ) (hΦ : ∀ (s t : ℝ), HasDerivAt (fun (t : ℝ) => Φ (s, t)) (φ (s, t)) t) (hab : a₂ ≤ b₂) : ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, φ z = ∫ (s : ℝ) in Set.Icc a₁ b₁, Φ (s, b₂) - Φ (s, a₂)

The fundamental theorem of calculus in the second coordinate. The integral of a continuous partial derivative φ = ∂₂ Φ over the rectangle [a₁, b₁] × [a₂, b₂] is the integral over [a₁, b₁] of the difference of the values of Φ on the two horizontal sides.

theorem TauCeti.setIntegral_rect_eq_zero_of_hasDerivAt_snd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {a₁ b₁ a₂ b₂ : ℝ} {Φ φ : ℝ × ℝ → E} (hφ : Continuous φ) (hΦ : ∀ (s t : ℝ), HasDerivAt (fun (t : ℝ) => Φ (s, t)) (φ (s, t)) t) (hper : ∀ (s : ℝ), Φ (s, b₂) = Φ (s, a₂)) : ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, φ z = 0

A derivative in the second coordinate of a function with equal values on the horizontal sides ℝ × {a₂} and ℝ × {b₂} integrates to zero over the rectangle [a₁, b₁] × [a₂, b₂].

theorem TauCeti.eqOn_zero_of_setIntegral_rect_eq_zero {a₁ b₁ a₂ b₂ : ℝ} {f : ℝ × ℝ → ℝ} (h₁ : a₁ < b₁) (h₂ : a₂ < b₂) (hf : Continuous f) (hf0 : 0 ≤ f) (hint : ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, f z = 0) : Set.EqOn f 0 (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)

A continuous nonnegative function with zero integral over a nondegenerate rectangle [a₁, b₁] × [a₂, b₂] vanishes on it.

theorem TauCeti.setIntegral_Icc_prod_le_of_comp_add_le {f M : ℝ × ℝ → ℝ} {c d L : ℝ} {I : Set ℝ} (hI : MeasurableSet I) (hfi : MeasureTheory.IntegrableOn f (Set.Icc (c + L) (d + L) ×ˢ I) MeasureTheory.volume) (hMi : MeasureTheory.IntegrableOn M (Set.Icc c d ×ˢ I) MeasureTheory.volume) (hfM : ∀ z ∈ Set.Icc c d ×ˢ I, f (z + (L, 0)) ≤ M z) : ∫ (z : ℝ × ℝ) in Set.Icc (c + L) (d + L) ×ˢ I, f z ≤ ∫ (z : ℝ × ℝ) in Set.Icc c d ×ˢ I, M z

Comparison of integrals over a translated strip. If f at the translate z + (L, 0) is pointwise bounded by M z on the strip [c, d] × I, with M integrable on that strip and f integrable on the translated strip [c + L, d + L] × I, then the integral of f over the translated strip is at most the integral of M over the original one.

theorem TauCeti.setIntegral_rect_le_mul_of_forall_setIntegral_le {a₁ b₁ a₂ b₂ : ℝ} {f g : ℝ × ℝ → ℝ} {c : ℝ} (hf : MeasureTheory.IntegrableOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) MeasureTheory.volume) (h : ∀ s ∈ Set.Icc a₁ b₁, ∫ (t : ℝ) in Set.Icc a₂ b₂, f (s, t) ≤ c * ∫ (t : ℝ) in Set.Icc a₂ b₂, g (s, t)) : ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, f z ≤ c * ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, g z

Integrating a slicewise inequality. If f and g are integrable over the rectangle [a₁, b₁] × [a₂, b₂] and, for every s ∈ [a₁, b₁], the integral of f (s, ·) over [a₂, b₂] is at most c times that of g (s, ·), then the integral of f over the rectangle is at most c times that of g.

theorem TauCeti.neg_mul_setIntegral_le_setIntegral_deriv_mul {a₁ b₁ a₂ b₂ : ℝ} {β : ℝ → ℝ} (hβ : ContDiff ℝ 1 β) (hβm : Monotone β) (hab : a₁ ≤ b₁) {f : ℝ × ℝ → ℝ} (hf : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)) {B : ℝ → ℝ} (hB : MeasureTheory.IntegrableOn B (Set.Icc a₂ b₂) MeasureTheory.volume) (hfB : ∀ z ∈ Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, -B z.2 ≤ f z) : -((β b₁ - β a₁) * ∫ (t : ℝ) in Set.Icc a₂ b₂, B t) ≤ ∫ (z : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, deriv β z.1 * f z

The integrated curvature bound of a monotone profile. Let β be a monotone C¹ profile and f a function continuous on [a₁, b₁] × [a₂, b₂] with -B(t) ≤ f there, for a function B integrable on [a₂, b₂]. Then -(β(b₁) - β(a₁)) ∫ B ≤ ∫∫ β'(s) f(s, t). Applied to f = (H₁ - H₀)(t, u) with H₀ - H₁ ≤ B, this bounds the curvature term -∫∫ ∂_s H of a linear homotopy H = H₀ + β(s) (H₁ - H₀) along a map u.