feat(measure_theory/integral/{interval,circle}_integral): add strict inequalities (#11061)

Author: urkud

src/measure_theory/integral/circle_integral.lean

@@ -311,6 +311,41 @@ calc ∥∮ z in C(c, R), f z∥ ≤ 2 * π * |R| * C :
   norm_integral_le_of_norm_le_const' $ by rwa this
 ... = 2 * π * R * C : by rw this
 
+lemma norm_two_pi_I_inv_smul_integral_le_of_norm_le_const {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 ≤ R)
+  (hf : ∀ z ∈ sphere c R, ∥f z∥ ≤ C) :
+  ∥(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), f z∥ ≤ R * C :=
+begin
+  have : ∥(2 * π * I : ℂ)⁻¹∥ = (2 * π)⁻¹, by simp [real.pi_pos.le],
+  rw [norm_smul, this, ← div_eq_inv_mul, div_le_iff real.two_pi_pos, mul_comm (R * C), ← mul_assoc],
+  exact norm_integral_le_of_norm_le_const hR hf
+end
+
+/-- If `f` is continuous on the circle `|z - c| = R`, `R > 0`, the `∥f z∥` is less than or equal to
+`C : ℝ` on this circle, and this norm is strictly less than `C` at some point `z` of the circle,
+then `∥∮ z in C(c, R), f z∥ < 2 * π * R * C`. -/
+lemma norm_integral_lt_of_norm_le_const_of_lt {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 < R)
+  (hc : continuous_on f (sphere c R)) (hf : ∀ z ∈ sphere c R, ∥f z∥ ≤ C)
+  (hlt : ∃ z ∈ sphere c R, ∥f z∥ < C) :
+  ∥∮ z in C(c, R), f z∥ < 2 * π * R * C :=
+begin
+  rw [← _root_.abs_of_pos hR, ← image_circle_map_Ioc] at hlt,
+  rcases hlt with ⟨_, ⟨θ₀, hmem, rfl⟩, hlt⟩,
+  calc ∥∮ z in C(c, R), f z∥ ≤ ∫ θ in 0..2 * π, ∥deriv (circle_map c R) θ • f (circle_map c R θ)∥ :
+    interval_integral.norm_integral_le_integral_norm real.two_pi_pos.le
+  ... < ∫ θ in 0..2 * π, R * C :
+    begin
+      simp only [norm_smul, deriv_circle_map, norm_eq_abs, complex.abs_mul, abs_I, mul_one,
+        abs_circle_map_zero, abs_of_pos hR],
+      refine interval_integral.integral_lt_integral_of_continuous_on_of_le_of_exists_lt
+        real.two_pi_pos _ continuous_on_const (λ θ hθ, _) ⟨θ₀, Ioc_subset_Icc_self hmem, _⟩,
+      { exact continuous_on_const.mul (hc.comp (continuous_circle_map _ _).continuous_on
+          (λ θ hθ, circle_map_mem_sphere _ hR.le _)).norm },
+      { exact mul_le_mul_of_nonneg_left (hf _ $ circle_map_mem_sphere _ hR.le _) hR.le },
+      { exact (mul_lt_mul_left hR).2 hlt }
+    end
+  ... = 2 * π * R * C : by simp [mul_assoc]
+end
+
 @[simp] lemma integral_smul {𝕜 : Type*} [is_R_or_C 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 ℂ E]
   (a : 𝕜) (f : ℂ → E) (c : ℂ) (R : ℝ) :
   ∮ z in C(c, R), a • f z = a • ∮ z in C(c, R), f z :=

src/measure_theory/integral/interval_integral.lean

@@ -1148,58 +1148,98 @@ begin
   { rw [integral_symm, neg_eq_zero, integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm] }
 end
 
+/-- If `f` is nonnegative and integrable on the unordered interval `set.interval_oc a b`, then its
+integral over `a..b` is positive if and only if `a < b` and the measure of
+`function.support f ∩ set.Ioc a b` is positive. -/
 lemma integral_pos_iff_support_of_nonneg_ae'
-  (hf : 0 ≤ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] f) (hfi : interval_integrable f μ a b) :
+  (hf : 0 ≤ᵐ[μ.restrict (Ι a b)] f) (hfi : interval_integrable f μ a b) :
   0 < ∫ x in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b) :=
 begin
-  obtain hab | hab := le_total b a;
-    simp only [Ioc_eq_empty hab.not_lt, empty_union, union_empty] at hf ⊢,
-  { rw [←not_iff_not, not_and_distrib, not_lt, not_lt, integral_of_ge hab, neg_nonpos],
-    exact iff_of_true (integral_nonneg_of_ae hf) (or.intro_left _ hab) },
-  rw [integral_of_le hab, set_integral_pos_iff_support_of_nonneg_ae hf hfi.1, iff.comm,
-    and_iff_right_iff_imp],
-  contrapose!,
-  intro h,
-  rw [Ioc_eq_empty h.not_lt, inter_empty, measure_empty],
-  exact le_refl 0,
+  cases lt_or_le a b with hab hba,
+  { rw interval_oc_of_le hab.le at hf,
+    simp only [hab, true_and, integral_of_le hab.le,
+      set_integral_pos_iff_support_of_nonneg_ae hf hfi.1] },
+  { suffices : ∫ x in a..b, f x ∂μ ≤ 0, by simp only [this.not_lt, hba.not_lt, false_and],
+    rw [integral_of_ge hba, neg_nonpos],
+    rw [interval_oc_swap, interval_oc_of_le hba] at hf,
+    exact integral_nonneg_of_ae hf }
 end
 
-lemma integral_pos_iff_support_of_nonneg_ae
-  (hf : 0 ≤ᵐ[μ] f) (hfi : interval_integrable f μ a b) :
+/-- If `f` is nonnegative a.e.-everywhere and it is integrable on the unordered interval
+`set.interval_oc a b`, then its integral over `a..b` is positive if and only if `a < b` and the
+measure of `function.support f ∩ set.Ioc a b` is positive. -/
+lemma integral_pos_iff_support_of_nonneg_ae (hf : 0 ≤ᵐ[μ] f) (hfi : interval_integrable f μ a b) :
   0 < ∫ x in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b) :=
 integral_pos_iff_support_of_nonneg_ae' (ae_mono measure.restrict_le_self hf) hfi
 
-variable (hab : a ≤ b)
+/-- If `f` and `g` are two functions that are interval integrable on `a..b`, `a ≤ b`,
+`f x ≤ g x` for a.e. `x ∈ set.Ioc a b`, and `f x < g x` on a subset of `set.Ioc a b`
+of nonzero measure, then `∫ x in a..b, f x ∂μ < ∫ x in a..b, g x ∂μ`. -/
+lemma integral_lt_integral_of_ae_le_of_measure_set_of_lt_ne_zero (hab : a ≤ b)
+  (hfi : interval_integrable f μ a b) (hgi : interval_integrable g μ a b)
+  (hle : f ≤ᵐ[μ.restrict (Ioc a b)] g) (hlt : μ.restrict (Ioc a b) {x | f x < g x} ≠ 0) :
+  ∫ x in a..b, f x ∂μ < ∫ x in a..b, g x ∂μ :=
+begin
+  rw [← sub_pos, ← integral_sub hgi hfi, integral_of_le hab,
+    measure_theory.integral_pos_iff_support_of_nonneg_ae],
+  { refine pos_iff_ne_zero.2 (mt (measure_mono_null _) hlt),
+    exact λ x hx, (sub_pos.2 hx).ne' },
+  exacts [hle.mono (λ x, sub_nonneg.2), hgi.1.sub hfi.1]
+end
 
-include hab
+/-- If `f` and `g` are continuous on `[a, b]`, `a < b`, `f x ≤ g x` on this interval, and
+`f c < g c` at some point `c ∈ [a, b]`, then `∫ x in a..b, f x < ∫ x in a..b, g x`. -/
+lemma integral_lt_integral_of_continuous_on_of_le_of_exists_lt {f g : ℝ → ℝ} {a b : ℝ}
+  (hab : a < b) (hfc : continuous_on f (Icc a b)) (hgc : continuous_on g (Icc a b))
+  (hle : ∀ x ∈ Icc a b, f x ≤ g x) (hlt : ∃ c ∈ Icc a b, f c < g c) :
+  ∫ x in a..b, f x < ∫ x in a..b, g x :=
+begin
+  refine integral_lt_integral_of_ae_le_of_measure_set_of_lt_ne_zero hab.le
+    (hfc.interval_integrable_of_Icc hab.le) (hgc.interval_integrable_of_Icc hab.le)
+    ((ae_restrict_mem measurable_set_Ioc).mono $ λ x hx, hle x (Ioc_subset_Icc_self hx)) _,
+  simp only [measure.restrict_apply' measurable_set_Ioc],
+  rcases hlt with ⟨c, ⟨hac, hcb⟩, hlt⟩,
+  have : ∀ᶠ x in 𝓝[Icc a b] c, f x < g x,
+    from ((hfc c ⟨hac, hcb⟩).prod (hgc c ⟨hac, hcb⟩)).eventually (is_open_lt_prod.mem_nhds hlt),
+  rcases (eventually_nhds_within_iff.1 this).exists_Ioo_subset with ⟨l, u, ⟨hlc, hcu⟩, hsub⟩,
+  have A : Ioo (max a l) (min b u) ⊆ Ioc a b,
+    from Ioo_subset_Ioc_self.trans (Ioc_subset_Ioc (le_max_left _ _) (min_le_left _ _)),
+  have B : Ioo (max a l) (min b u) ⊆ Ioo l u,
+    from Ioo_subset_Ioo (le_max_right _ _) (min_le_right _ _),
+  refine ne_of_gt _,
+  calc (0 : ℝ≥0∞) < volume (Ioo (max a l) (min b u)) :
+    by simp [hab, hlc.trans_le hcb, hac.trans_lt hcu, hlc.trans hcu]
+  ... ≤ volume ({x | f x < g x} ∩ Ioc a b) :
+    measure_mono (λ x hx, ⟨hsub (B hx) (Ioc_subset_Icc_self $ A hx), A hx⟩)
+end
 
-lemma integral_nonneg_of_ae_restrict (hf : 0 ≤ᵐ[μ.restrict (Icc a b)] f) :
+lemma integral_nonneg_of_ae_restrict (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Icc a b)] f) :
   0 ≤ (∫ u in a..b, f u ∂μ) :=
 let H := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf in
 by simpa only [integral_of_le hab] using set_integral_nonneg_of_ae_restrict H
 
-lemma integral_nonneg_of_ae (hf : 0 ≤ᵐ[μ] f) :
+lemma integral_nonneg_of_ae (hab : a ≤ b) (hf : 0 ≤ᵐ[μ] f) :
   0 ≤ (∫ u in a..b, f u ∂μ) :=
 integral_nonneg_of_ae_restrict hab $ ae_restrict_of_ae hf
 
-lemma integral_nonneg_of_forall (hf : ∀ u, 0 ≤ f u) :
+lemma integral_nonneg_of_forall (hab : a ≤ b) (hf : ∀ u, 0 ≤ f u) :
   0 ≤ (∫ u in a..b, f u ∂μ) :=
 integral_nonneg_of_ae hab $ eventually_of_forall hf
 
 lemma integral_nonneg [topological_space α] [opens_measurable_space α] [order_closed_topology α]
-  (hf : ∀ u, u ∈ Icc a b → 0 ≤ f u) :
+  (hab : a ≤ b) (hf : ∀ u, u ∈ Icc a b → 0 ≤ f u) :
   0 ≤ (∫ u in a..b, f u ∂μ) :=
 integral_nonneg_of_ae_restrict hab $ (ae_restrict_iff' measurable_set_Icc).mpr $ ae_of_all μ hf
 
-lemma abs_integral_le_integral_abs :
+lemma abs_integral_le_integral_abs (hab : a ≤ b) :
   |∫ x in a..b, f x ∂μ| ≤ ∫ x in a..b, |f x| ∂μ :=
 by simpa only [← real.norm_eq_abs] using norm_integral_le_integral_norm hab
 
 section mono
 
-variables (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b)
+variables (hab : a ≤ b) (hf : interval_integrable f μ a b) (hg : interval_integrable g μ a b)
 
-include hf hg
+include hab hf hg
 
 lemma integral_mono_ae_restrict (h : f ≤ᵐ[μ.restrict (Icc a b)] g) :
   ∫ u in a..b, f u ∂μ ≤ ∫ u in a..b, g u ∂μ :=