Move lemmas (#462)

Move general lemmas from the `Antichain` folder to appropriate files.

Author: mariainesdff

Carleson/Antichain/AntichainOperator.lean

@@ -315,12 +315,6 @@ lemma dens1_antichain (h𝔄 : IsAntichain (· ≤ ·) 𝔄)
 -- Todo: define this recursively in terms of previous constants
 def C2_0_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (128 * a ^ 3) / (q - 1)
 
---TODO: PR to Mathlib
-theorem ENNReal.rpow_le_self_of_one_le {x : ℝ≥0∞} {y : ℝ} (hx : 1 ≤ x) (hy : y ≤ 1) :
-    x ^ y ≤ x := by
-  nth_rw 2 [← ENNReal.rpow_one x]
-  exact ENNReal.rpow_le_rpow_of_exponent_le hx hy
-
 variable (X) in
 omit [TileStructure Q D κ S o] in
 private lemma ineq_aux_2_0_3 :

Carleson/Antichain/AntichainTileCount.lean

@@ -801,19 +801,12 @@ private lemma ineq_6_3_39 (h𝔄 : IsAntichain (· ≤ ·) 𝔄) {L : Grid X}
       gcongr; simp only [𝔄']
       exact sep_subset _ _
 
--- Copied from`ForestOperator.LargeSeparation`, where it is called
--- `IF_subset_THEN_distance_between_centers`.
--- **TODO**: move to common import.
-private lemma dist_c_le_of_subset {J J' : Grid X} (subset : (J : Set X) ⊆ J') :
-    dist (c J) (c J') < 4 * D ^ s J' :=
-  Grid_subset_ball (subset Grid.c_mem_Grid)
-
 -- Ineq. 6.3.41
 private lemma volume_L'_le {L : Grid X} (hL : L ∈ 𝓛' 𝔄 ϑ N) :
     volume (L' hL : Set X) ≤ 2 ^ (100*a^3 + 5*a) * volume (L : Set X) := by
   have hc : dist (c L) (c (L' hL)) + 4 * D ^ s (L' hL) ≤ 8 * D ^ s (L' hL) := by
     calc dist (c L) (c (L' hL)) + 4 * D ^ s (L' hL)
-      _ ≤ 4 * ↑D ^ s (L' hL) + 4 * D ^ s (L' hL) := by grw [dist_c_le_of_subset (L_le_L' hL).1]
+      _ ≤ 4 * ↑D ^ s (L' hL) + 4 * D ^ s (L' hL) := by grw [Grid.dist_c_le_of_subset (L_le_L' hL).1]
       _ ≤ 8 * ↑D ^ s (L' hL) := by linarith
   calc volume (L' hL : Set X)
     _ ≤ volume (ball (c (L' hL)) (4 * D ^ s (L' hL))) := by

Carleson/Antichain/Basic.lean

@@ -232,19 +232,6 @@ lemma MaximalBoundAntichain {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ 
       exact hx p hp
     simp only [h0, enorm_zero, zero_le]
 
--- TODO: PR to Mathlib
-omit [MetricSpace X] in
-lemma _root_.Set.eq_indicator_one_mul {F : Set X} {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
-    f = (F.indicator 1) * f := by
-  ext y
-  simp only [Pi.mul_apply, indicator, Pi.one_apply, ite_mul, one_mul, zero_mul]
-  split_ifs with hy
-  · rfl
-  · specialize hf y
-    simp only [indicator, hy, ↓reduceIte] at hf
-    rw [← norm_eq_zero]
-    exact le_antisymm hf (norm_nonneg _)
-
 -- Note: Proof shows that `111` can be replaced by `108`
 /-- Constant appearing in Lemma 6.1.3. -/
 noncomputable def C6_1_3 (a : ℕ) (q : ℝ≥0) : ℝ≥0 := 2 ^ (111 * a ^ 3) * (q - 1)⁻¹
@@ -315,7 +302,7 @@ lemma eLpNorm_𝓜_le_eLpNorm_𝓜p_mul (hf : Measurable f)
   have : ENNReal.ofReal p' ≠ ⊤ := ofReal_ne_top
   have hp_coe : p.toNNReal.toReal = p := Real.coe_toNNReal _ (by positivity)
 
-  conv_lhs => rw [eq_indicator_one_mul hfF]
+  conv_lhs => rw [eq_indicator_one_mul_of_norm_le hfF]
   apply eLpNorm_le_mul_eLpNorm_of_ae_le_mul''
   · exact AEStronglyMeasurable.maximalFunction 𝔄.to_countable
   · refine ae_of_all _ <| fun x ↦ ?_

Carleson/Antichain/TileCorrelation.lean

@@ -1,5 +1,6 @@
 import Carleson.HolderVanDerCorput
 import Carleson.Operators
+import Carleson.ToMathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
 
 macro_rules | `(tactic |gcongr_discharger) => `(tactic | with_reducible assumption)
 
@@ -21,11 +22,6 @@ section FunProp
 
 attribute [fun_prop] Complex.measurable_exp Complex.measurable_ofReal
 
--- TODO: PR to Mathlib
-@[fun_prop]
-lemma Complex.measurable_starRingEnd : Measurable (starRingEnd ℂ) :=
-   Complex.continuous_conj.measurable
-
 @[fun_prop]
 lemma measurable_correlation :
     Measurable (fun (s₁ s₂ : ℤ) (x y z : X) ↦ correlation s₁ s₂ x y z) := by
@@ -68,12 +64,6 @@ lemma mem_ball_of_mem_tsupport_correlation {s₁ s₂ : ℤ} {x₁ x₂ y : X}
 /-- The constant from lemma 6.2.1. -/
 def C6_2_1 (a : ℕ) : ℝ≥0 := 2 ^ (254 * a ^ 3)
 
---TODO: PR to Mathlib
-lemma ENNReal.mul_div_mul_comm {a b c d : ℝ≥0∞} (hc : c ≠ ⊤) (hd : d ≠ ⊤) :
-    a * b / (c * d) = a / c * (b / d) := by
-  simp only [div_eq_mul_inv, ENNReal.mul_inv (Or.inr hd) (Or.inl hc)]
-  ring
-
 lemma aux_6_2_3 (s₁ s₂ : ℤ) (x₁ x₂ y y' : X) :
   ‖Ks s₂ x₂ y‖ₑ * ‖Ks s₁ x₁ y - Ks s₁ x₁ y'‖ₑ ≤
   C2_1_3 a / volume (ball x₂ (D ^ s₂)) *
@@ -110,11 +100,13 @@ lemma e625 {s₁ s₂ : ℤ} {x₁ x₂ y y' : X} (hy' : y ≠ y') (hs : s₁ 
         norm_cast
         ring
       rw [mul_comm, mul_add, h2, mul_comm (volume _)]
-      rw [ENNReal.mul_div_mul_comm measure_ball_ne_top measure_ball_ne_top, mul_assoc]
+      rw [ENNReal.mul_div_mul_comm (Or.inr measure_ball_ne_top)
+        (Or.inl measure_ball_ne_top), mul_assoc]
       apply add_le_add (aux_6_2_3 s₁ s₂ x₁ x₂ y y')
       rw [← neg_sub, enorm_neg]
       convert aux_6_2_3 s₂ s₁ x₂ x₁ y' y using 1
-      simp only [← mul_assoc, ← ENNReal.mul_div_mul_comm measure_ball_ne_top measure_ball_ne_top]
+      simp only [← mul_assoc, ← ENNReal.mul_div_mul_comm (Or.inr measure_ball_ne_top)
+        (Or.inl measure_ball_ne_top)]
       rw [mul_comm (volume _), edist_comm]
     _ ≤ 2 ^ (252 * a ^ 3) / (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))) *
         (2 * (edist y y' ^ τ / (D ^ s₁) ^ τ)) := by
@@ -156,7 +148,8 @@ lemma correlation_kernel_bound {s₁ s₂ : ℤ} {x₁ x₂ : X} (hs : s₁ ≤
   have hφ' (y : X) : ‖correlation s₁ s₂ x₁ x₂ y‖ₑ ≤
       (C2_1_3 a) ^ 2 / (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))):= by
     simp only [correlation, enorm_mul, RCLike.enorm_conj, pow_two,
-      ENNReal.mul_div_mul_comm measure_ball_ne_top measure_ball_ne_top]
+      ENNReal.mul_div_mul_comm (Or.inr measure_ball_ne_top)
+        (Or.inl measure_ball_ne_top)]
     exact mul_le_mul enorm_Ks_le enorm_Ks_le (zero_le _) (zero_le _)
   -- 6.2.6 + 6.2.7
   calc
@@ -184,19 +177,6 @@ lemma correlation_kernel_bound {s₁ s₂ : ℤ} {x₁ x₂ : X} (hs : s₁ ≤
 
 variable [TileStructure Q D κ S o]
 
--- TODO: PR both versions to Mathlib
-theorem MeasureTheory.exists_ne_zero_of_setIntegral_ne_zero {α E : Type*} [NormedAddCommGroup E]
-    [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → E} {U : Set α}
-    (hU : ∫ (u : α) in U, f u ∂μ ≠ 0) : ∃ u : α, u ∈ U ∧ f u ≠ 0 := by
-  contrapose! hU
-  exact setIntegral_eq_zero_of_forall_eq_zero hU
-
-theorem MeasureTheory.exists_ne_zero_of_integral_ne_zero {α E : Type*} [NormedAddCommGroup E]
-    [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → E}
-    (h : ∫ (u : α), f u ∂μ ≠ 0) : ∃ u : α, f u ≠ 0 := by
-  contrapose! h
-  exact integral_eq_zero_of_ae ((eqOn_univ f 0).mp fun ⦃x⦄ a ↦ h x).eventuallyEq
-
 -- Lemma 6.2.2
 lemma range_support {p : 𝔓 X} {g : X → ℂ} {y : X} (hpy : adjointCarleson p g y ≠ 0) :
     y ∈ (ball (𝔠 p) (5 * D ^𝔰 p)) := by
@@ -432,23 +412,6 @@ lemma exp_ineq (ha : 4 ≤ a) : 0 < ((8 * a  : ℕ) : ℝ) * -(2 * (a : ℝ) ^ 2
   norm_cast
   nlinarith
 
--- TODO: PR to Mathlib
-lemma _root_.ENNReal.rpow_lt_rpow_of_neg {x y : ℝ≥0∞} {z : ℝ} (hz : z < 0) (h : x < y) :
-    y ^ z < x ^ z := by
-  rw [← neg_neg z, ENNReal.rpow_neg y, ENNReal.rpow_neg x, ← ENNReal.inv_rpow, ← ENNReal.inv_rpow]
-  exact ENNReal.rpow_lt_rpow (ENNReal.inv_lt_inv.mpr h) (neg_pos.mpr hz)
-
--- TODO: PR to Mathlib
-
-lemma _root_.ENNReal.rpow_lt_rpow_iff_of_neg {x y : ℝ≥0∞} {z : ℝ} (hz : z < 0) :
-    x ^ z < y ^ z ↔ y < x :=
-  ⟨lt_imp_lt_of_le_imp_le (fun h ↦ ENNReal.rpow_le_rpow_of_nonpos (le_of_lt hz) h),
-    fun h ↦ ENNReal.rpow_lt_rpow_of_neg hz h⟩
-
-lemma _root_.ENNReal.rpow_le_rpow_iff_of_neg {x y : ℝ≥0∞} {z : ℝ} (hz : z < 0) :
-    x ^ z ≤ y ^ z ↔ y ≤ x :=
-  le_iff_le_iff_lt_iff_lt.2 <| ENNReal.rpow_lt_rpow_iff_of_neg hz
-
 /-- Inequality 6.2.29. -/ -- TODO: add ‖g ↑x1‖ₑ * ‖g ↑x2‖ₑ in blueprint's RHS
 lemma I12_le (ha : 4 ≤ a) (p p' : 𝔓 X) (hle : 𝔰 p' ≤ 𝔰 p) (g : X → ℂ)
     (hinter : (ball (𝔠 p') (5 * D ^ 𝔰 p') ∩ ball (𝔠 p) (5 * D ^ 𝔰 p)).Nonempty)
@@ -728,12 +691,6 @@ lemma bound_6_2_29' (ha : 4 ≤ a) (p p' : 𝔓 X) (x2 : E p) : 2 ^ (254 * a^3 +
     _ ≤ (C6_1_5 a) * ((1 + dist_(p') (𝒬 p') (𝒬 p))^(-(2 * a^2 + a^3 : ℝ)⁻¹)) /
           (volume (coeGrid (𝓘 p))).toNNReal := by gcongr; exact hvol x2
 
--- TODO: PR to Mathlib
-omit [MetricSpace X] in
-lemma _root_.Set.indicator_one_le_one (x : X) : G.indicator (1 : X → ℝ) x ≤ 1 := by
-  classical
-  exact le_trans (ite_le_sup _ _ _) (by simp)
-
 omit [TileStructure Q D κ S o] in
 lemma enorm_eq_zero_of_notMem_closedBall {g : X → ℂ} (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
     {x : X} (hx : x ∉ (closedBall (cancelPt X) (defaultD a ^ defaultS X / 4))) :
@@ -850,12 +807,6 @@ lemma boundedCompactSupport_Ks_mul_star_g (p : 𝔓 X) {g : X → ℂ}
       _ ≤ C + C := by gcongr; exact hC x.1 x.2 hx
       _ = 2 * C := by ring
 
-
--- This was deleted from `BoundedCompactSupport.lean`, but I need it.
-open Bornology in
-lemma _root_.isBounded_range_iff_forall_norm_le {α β} [SeminormedAddCommGroup α] {f : β → α} :
-    IsBounded (range f) ↔ ∃ C, ∀ x, ‖f x‖ ≤ C := by convert isBounded_iff_forall_norm_le; simp
-
 -- memLp_top_of_bound
 lemma boundedCompactSupport_aux_6_2_26 (p p' : 𝔓 X) {g : X → ℂ}
     (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :
@@ -1067,7 +1018,6 @@ lemma integrableOn_I12 (ha : 4 ≤ a) {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p)
   exact MeasureTheory.IntegrableOn.congr_fun hf (fun _ hx ↦ by simp only [f, if_pos hx])
     (measurableSet_E.prod measurableSet_E)
 
-/- TODO: it should be way easier to deduce this from `integrableOn_I12`, right? -/
 lemma integrableOn_I12' (ha : 4 ≤ a) {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ} (hg : Measurable g)
     (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
     (hinter : (ball (𝔠 p') (5 * D ^ 𝔰 p') ∩ ball (𝔠 p) (5 * D ^ 𝔰 p)).Nonempty) :

Carleson/ForestOperator/LargeSeparation.lean

@@ -83,10 +83,6 @@ def holderFunction (f₁ f₂ : X → ℂ) (J : Grid X) (x : X) : ℂ :=
 
 /- AUXILIARY LEMMAS:START -/
 
-lemma IF_subset_THEN_distance_between_centers (subset : (J : Set X) ⊆ J') :
-    dist (c J) (c J') < 4 * D ^ s J' :=
-  Grid_subset_ball (subset Grid.c_mem_Grid)
-
 lemma IF_subset_THEN_not_disjoint {A B : Grid X} (h : (A : Set X) ⊆ B) :
     ¬ Disjoint (B : Set X) (A : Set X) := by
   rw [disjoint_comm]
@@ -928,7 +924,7 @@ lemma limited_scale_impact_second_estimate (hp : p ∈ t u₂ \ 𝔖₀ t u₁ u
       apply cdist_mono
       simp only [not_disjoint_iff] at h
       rcases h with ⟨middleX, lt_2, lt_3⟩
-      have lt_4 := IF_subset_THEN_distance_between_centers belongs.left
+      have lt_4 := Grid.dist_c_le_of_subset belongs.left
       intros x lt_1
       calc dist x (𝔠 p)
       _ ≤ dist x (c J') + dist (c J') (c J) + dist (c J) middleX + dist middleX (𝔠 p) := by
@@ -1890,7 +1886,7 @@ lemma lower_oscillation_bound (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u
         gcongr
       _ ≤ 100 * D ^ (s J' + 1) + 4 * D ^ (s J') := by
         have : dist (c J) (c J') < 4 * D ^ (s J') :=
-          IF_subset_THEN_distance_between_centers (subset := JleJ'.1)
+          Grid.dist_c_le_of_subset (subset := JleJ'.1)
         rw [dist_comm] at this
         gcongr
       _ = 100 * D ^ (s J + 2) + 4 * D ^ (s J + 1) := by

Carleson/GridStructure.lean

@@ -457,4 +457,8 @@ lemma dist_strictMono_iterate' {I J : Grid X} {d : ℤ} (hd : d ≥ 0) (hij : I
   rw [← Int.toNat_of_nonneg hd] at hs ⊢
   exact dist_strictMono_iterate hij hs
 
+lemma dist_c_le_of_subset {J J' : Grid X} (subset : (J : Set X) ⊆ J') :
+    dist (c J) (c J') < 4 * D ^ s J' :=
+  Grid_subset_ball (subset Grid.c_mem_Grid)
+
 end Grid

Carleson/TileStructure.lean

@@ -368,11 +368,6 @@ lemma dens₂_eq_biSup_dens₂ (𝔓' : Set (𝔓 X)) :
     dens₂ (𝔓') = ⨆ (p ∈ 𝔓'), dens₂ ({p}) := by
   simp [dens₂]
 
-lemma ENNReal.rpow_le_rpow_of_nonpos {x y : ℝ≥0∞} {z : ℝ} (hz : z ≤ 0) (h : x ≤ y) :
-    y ^ z ≤ x ^ z := by
-  rw [← neg_neg z, rpow_neg y, rpow_neg x, ← inv_rpow, ← inv_rpow]
-  exact rpow_le_rpow (ENNReal.inv_le_inv.mpr h) (neg_nonneg.mpr hz)
-
 /- A rough estimate. It's also less than 2 ^ (-a) -/
 lemma dens₁_le_one {𝔓' : Set (𝔓 X)} : dens₁ 𝔓' ≤ 1 := by
   conv_rhs => rw [← mul_one 1]

Carleson/ToMathlib/BoundedCompactSupport.lean

@@ -76,6 +76,10 @@ namespace BoundedCompactSupport
 
 section General
 
+open Bornology in
+lemma _root_.isBounded_range_iff_forall_norm_le {α β} [SeminormedAddCommGroup α] {f : β → α} :
+    IsBounded (range f) ↔ ∃ C, ∀ x, ‖f x‖ ≤ C := by convert isBounded_iff_forall_norm_le; simp
+
 variable [TopologicalSpace E] [ENorm E] [Zero E]
 
 theorem aestronglyMeasurable (hf : BoundedCompactSupport f μ) : AEStronglyMeasurable f μ :=

Carleson/ToMathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean

@@ -51,3 +51,17 @@ theorem MeasureTheory.setIntegral_union_2 (hst : Disjoint s t) (ht : MeasurableS
   setIntegral_union hst ht hfst.left_of_union hfst.right_of_union
 
 end SetIntegral_Union_2
+
+-- [Mathlib.MeasureTheory.Integral.Bochner.Set]
+theorem MeasureTheory.exists_ne_zero_of_setIntegral_ne_zero {α E : Type*} [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → E} {U : Set α}
+    (hU : ∫ (u : α) in U, f u ∂μ ≠ 0) : ∃ u : α, u ∈ U ∧ f u ≠ 0 := by
+  contrapose! hU
+  exact setIntegral_eq_zero_of_forall_eq_zero hU
+
+-- [Mathlib.MeasureTheory.Integral.Bochner.Basic]
+theorem MeasureTheory.exists_ne_zero_of_integral_ne_zero {α E : Type*} [NormedAddCommGroup E]
+    [NormedSpace ℝ E] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → E}
+    (h : ∫ (u : α), f u ∂μ ≠ 0) : ∃ u : α, f u ≠ 0 := by
+  contrapose! h
+  exact integral_eq_zero_of_ae ((Set.eqOn_univ f 0).mp fun ⦃x⦄ a ↦ h x).eventuallyEq

Carleson/ToMathlib/Misc.lean

@@ -106,20 +106,6 @@ lemma ENNReal.toReal_zpow (x : ℝ≥0∞) (z : ℤ) : x.toReal ^ z = (x ^ z).to
 
 end ENNReal
 
-section Indicator
-attribute [gcongr] Set.indicator_le_indicator mulIndicator_le_mulIndicator_of_subset
-
-lemma Set.indicator_eq_indicator' {α : Type*} {M : Type*} [Zero M] {s : Set α} {f g : α → M} (h : ∀ x ∈ s, f x = g x) :
-    s.indicator f = s.indicator g := by
-  ext x
-  unfold indicator
-  split
-  · rename_i hxs
-    exact h x hxs
-  · rfl
-
-end Indicator
-
 section NNReal
 
 
@@ -448,10 +434,55 @@ lemma Real.self_lt_two_rpow (x : ℝ) : x < 2 ^ x := by
       _ ≤ 2 ^ (⌊x⌋₊ : ℝ) := by exact_mod_cast Nat.lt_pow_self one_lt_two
       _ ≤ _ := rpow_le_rpow_of_exponent_le one_le_two (Nat.floor_le h)
 
+@[fun_prop]
+lemma Complex.measurable_starRingEnd : Measurable (starRingEnd ℂ) :=
+   Complex.continuous_conj.measurable
+
+namespace ENNReal
+
+lemma rpow_le_rpow_of_nonpos {x y : ℝ≥0∞} {z : ℝ} (hz : z ≤ 0) (h : x ≤ y) :
+    y ^ z ≤ x ^ z := by
+  rw [← neg_neg z, rpow_neg y, rpow_neg x, ← inv_rpow, ← inv_rpow]
+  exact rpow_le_rpow (ENNReal.inv_le_inv.mpr h) (neg_nonneg.mpr hz)
+
+lemma rpow_lt_rpow_of_neg {x y : ℝ≥0∞} {z : ℝ} (hz : z < 0) (h : x < y) :
+    y ^ z < x ^ z := by
+  rw [← neg_neg z, ENNReal.rpow_neg y, ENNReal.rpow_neg x, ← ENNReal.inv_rpow, ← ENNReal.inv_rpow]
+  exact ENNReal.rpow_lt_rpow (ENNReal.inv_lt_inv.mpr h) (neg_pos.mpr hz)
+
+lemma rpow_lt_rpow_iff_of_neg {x y : ℝ≥0∞} {z : ℝ} (hz : z < 0) :
+    x ^ z < y ^ z ↔ y < x :=
+  ⟨lt_imp_lt_of_le_imp_le (fun h ↦ ENNReal.rpow_le_rpow_of_nonpos (le_of_lt hz) h),
+    fun h ↦ ENNReal.rpow_lt_rpow_of_neg hz h⟩
+
+lemma rpow_le_rpow_iff_of_neg {x y : ℝ≥0∞} {z : ℝ} (hz : z < 0) :
+    x ^ z ≤ y ^ z ↔ y ≤ x :=
+  le_iff_le_iff_lt_iff_lt.2 <| ENNReal.rpow_lt_rpow_iff_of_neg hz
+
+theorem rpow_le_self_of_one_le {x : ℝ≥0∞} {y : ℝ} (hx : 1 ≤ x) (hy : y ≤ 1) :
+    x ^ y ≤ x := by
+  nth_rw 2 [← ENNReal.rpow_one x]
+  exact ENNReal.rpow_le_rpow_of_exponent_le hx hy
+
+end ENNReal
+
 namespace Set
 
+section Indicator
+
 open ComplexConjugate
 
+attribute [gcongr] Set.indicator_le_indicator mulIndicator_le_mulIndicator_of_subset
+
+lemma indicator_eq_indicator' {α : Type*} {M : Type*} [Zero M] {s : Set α} {f g : α → M} (h : ∀ x ∈ s, f x = g x) :
+    s.indicator f = s.indicator g := by
+  ext x
+  unfold indicator
+  split
+  · rename_i hxs
+    exact h x hxs
+  · rfl
+
 lemma indicator_eq_indicator_one_mul {ι M : Type*} [MulZeroOneClass M]
     (s : Set ι) (f : ι → M) (x : ι) : s.indicator f x = s.indicator 1 x * f x := by
   simp only [indicator]; split_ifs <;> simp
@@ -460,6 +491,25 @@ lemma conj_indicator {α 𝕜 : Type*} [RCLike 𝕜] {f : α → 𝕜} (s : Set
     conj (s.indicator f x) = s.indicator (conj f) x := by
   simp only [indicator]; split_ifs <;> simp
 
+lemma eq_indicator_one_mul_of_norm_le {X : Type*} {F : Set X} {f : X → ℂ}
+    (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
+    f = (F.indicator 1) * f := by
+  ext y
+  simp only [Pi.mul_apply, indicator, Pi.one_apply, ite_mul, one_mul, zero_mul]
+  split_ifs with hy
+  · rfl
+  · specialize hf y
+    simp only [indicator, hy, ↓reduceIte] at hf
+    rw [← norm_eq_zero]
+    exact le_antisymm hf (norm_nonneg _)
+
+lemma indicator_one_le_one {X : Type*} {G : Set X} (x : X) :
+    G.indicator (1 : X → ℝ) x ≤ 1 := by
+  classical
+  exact le_trans (ite_le_sup _ _ _) (by simp)
+
+end Indicator
+
 end Set
 
 section Norm