wip: use fun_prop for BoundedCompactSupport (#499)

- Many proofs can be golfed nicely. This PR also golfs some other proofs
using fun_prop.
- The proof in `AntichainOperator` puzzles me and smells like a fun_prop
bug.
- A couple of proofs do not work because
`BoundedCompactSupport.indicator` has a measurability side condition;
running `fun_prop (discharger := assumption)` did not work. Perhaps a
better incantation will fix this.

Author: grunweg

Carleson/Antichain/AntichainOperator.lean

@@ -20,6 +20,7 @@ variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X
   [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
   {𝔄 : Set (𝔓 X)} {f g : X → ℂ}
 
+-- set_option trace.Meta.Tactic.fun_prop true in
 open Classical in
 lemma dens1_antichain_rearrange (bg : BoundedCompactSupport g) :
     eLpNorm (adjointCarlesonSum 𝔄 g) 2 ^ 2 ≤
@@ -36,8 +37,15 @@ lemma dens1_antichain_rearrange (bg : BoundedCompactSupport g) :
       congr 1
       rw [integral_finset_sum]
       · congr! with p mp
-        exact integral_finset_sum _ fun p' mp' ↦
-          (bg.adjointCarleson.mul bg.adjointCarleson.conj).integrable
+        exact integral_finset_sum _ fun p' mp' ↦ by
+          -- This smells like a fun_prop bug: removing the `change` makes fun_prop fail to prove
+          -- `fails` below, even though it knows about `BoundedCompactSupport.integrable` and
+          -- can prove that.
+          have : BoundedCompactSupport (fun x ↦ (starRingEnd ℂ) (adjointCarleson p' g x)) volume := by fun_prop
+          --have fails : Integrable (fun x ↦ (starRingEnd ℂ) (adjointCarleson p' g x)) volume := by
+          --  fun_prop
+          change Integrable (adjointCarleson p g * star (adjointCarleson p' g)) volume
+          fun_prop
       · exact fun p mp ↦ (BoundedCompactSupport.finset_sum fun p' mp' ↦
           bg.adjointCarleson.mul bg.adjointCarleson.conj).integrable
     _ ≤ ∑ p with p ∈ 𝔄, ‖∑ p' with p' ∈ 𝔄,

Carleson/ForestOperator/Forests.lean

@@ -893,23 +893,21 @@ lemma forest_operator_g_prelude
   calc
     _ = ‖∑ u with u ∈ t, ∫ x, conj (g x) * carlesonSum (t u) f x‖ₑ := by
       congr; rw [← integral_finset_sum]; swap
-      · exact fun _ _ ↦ (bg.conj.mul bf.carlesonSum).integrable
+      · fun_prop
       simp_rw [Finset.mul_sum]
     _ = ‖∑ u with u ∈ t, ∫ x, conj (adjointCarlesonSum (t u) g x) * f x‖ₑ := by
       congr! 2 with u mu; exact adjointCarlesonSum_adjoint bf bg _
     _ = ‖∫ x, f x * ∑ u with u ∈ t, conj (adjointCarlesonSum (t u) g x)‖ₑ := by
       congr; rw [← integral_finset_sum]; swap
-      · exact fun _ _ ↦ (bg.adjointCarlesonSum.conj.mul bf).integrable
+      · intro _ _
+        fun_prop
       simp_rw [Finset.mul_sum, mul_comm (f _)]
     _ ≤ ∫⁻ x, ‖f x‖ₑ * ‖∑ u with u ∈ t, conj (adjointCarlesonSum (t u) g x)‖ₑ := by
       simp_rw [← enorm_mul]; exact enorm_integral_le_lintegral_enorm _
     _ ≤ _ := by
       simp_rw [← map_sum, RCLike.enorm_conj]
       conv_rhs => rw [← eLpNorm_enorm]; enter [2]; rw [← eLpNorm_enorm]
-      exact ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance
-        bf.enorm.aestronglyMeasurable.aemeasurable
-        (BoundedCompactSupport.finset_sum fun _ _ ↦
-          bg.adjointCarlesonSum).enorm.aestronglyMeasurable.aemeasurable
+      exact ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance (by fun_prop) (by fun_prop)
 
 lemma adjointCarlesonRowSum_rowSupport :
     adjointCarlesonRowSum t j f = adjointCarlesonRowSum t j ((rowSupport t j).indicator f) := by
@@ -952,9 +950,7 @@ lemma forest_operator_g_main (hg : Measurable g) (h2g : ∀ x, ‖g x‖ ≤ G.i
   let TR (j : ℕ) (x : X) := adjointCarlesonRowSum t j ((rowSupport t j).indicator g) x
   have bcsrsi (j : ℕ) : BoundedCompactSupport ((t.rowSupport j).indicator g) volume :=
     bg.indicator measurableSet_rowSupport
-  have bcsTR (j : ℕ) : BoundedCompactSupport (TR j) :=
-    BoundedCompactSupport.finset_sum fun _ _ ↦
-      BoundedCompactSupport.finset_sum fun _ _ ↦ (bcsrsi j).adjointCarleson
+  have bcsTR (j : ℕ) : BoundedCompactSupport (TR j) := by unfold TR adjointCarlesonRowSum; fun_prop
   calc
     _ = eLpNorm (∑ j ∈ Finset.range (2 ^ n), adjointCarlesonRowSum t j g ·) 2 ^ 2 := by
       congr; ext x
@@ -1061,8 +1057,7 @@ lemma forest_operator_f_prelude
         rw [indicator_of_notMem hx, norm_le_zero_iff] at h2g
         rw [h2g, zero_mul]
     _ ≤ _ :=
-      ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance
-        bg.enorm.aestronglyMeasurable.aemeasurable
+      ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance (by fun_prop)
         ((BoundedCompactSupport.finset_sum fun _ _ ↦
           bf.carlesonSum).indicator measurableSet_G).enorm.aestronglyMeasurable.aemeasurable
 
@@ -1104,8 +1099,8 @@ lemma forest_operator_f_inner (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.
       apply ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance
       · exact ((BoundedCompactSupport.finset_sum fun _ _ ↦ bIGTf.adjointCarlesonSum).indicator
           measurableSet_F).enorm.aestronglyMeasurable.aemeasurable
-      · exact bf.enorm.aestronglyMeasurable.aemeasurable
-    _ ≤ _ := by exact mul_le_mul_right' (indicator_row_bound bIGTf support_indicator_subset) _
+      · fun_prop
+    _ ≤ _ := by gcongr; exact indicator_row_bound bIGTf support_indicator_subset
 
 /-- The constant in the `f` side of Proposition 2.0.4.
 Has value `2 ^ (283 * a ^ 3)` in the blueprint. -/
@@ -1269,7 +1264,7 @@ theorem forest_operator' {n : ℕ} (𝔉 : Forest X n) {f : X → ℂ} {A : Set
   the sum to be controlled. -/
   have bf := bcs_of_measurable_of_le_indicator_f hf h2f
   rw [← enorm_integral_starRingEnd_mul_eq_lintegral_enorm]; swap
-  · exact (BoundedCompactSupport.finset_sum (fun i hi ↦ bf.carlesonSum.restrict)).integrable
+  · exact (BoundedCompactSupport.finset_sum (fun i hi ↦ by fun_prop)).integrable
   rw [← integral_indicator hA]
   simp_rw [indicator_mul_left, ← comp_def,
     Set.indicator_comp_of_zero (g := starRingEnd ℂ) (by simp)]
@@ -1281,10 +1276,7 @@ theorem forest_operator' {n : ℕ} (𝔉 : Forest X n) {f : X → ℂ} {A : Set
     · rw [hnorm]; norm_num
     · rw [div_self hnorm]
   apply (forest_operator 𝔉 hf h2f ?_ fun x ↦ ?_).trans; rotate_left
-  · refine Measurable.indicator ?_ hA
-    suffices Measurable (∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f ·) by
-      exact this.div (measurable_ofReal.comp this.norm)
-    exact Finset.measurable_sum _ fun _ _ ↦ measurable_carlesonSum hf
+  · exact Measurable.indicator (by fun_prop) hA
   · exact (bAi _).trans (indicator_le_indicator_apply_of_subset sA (by simp))
   gcongr
   · simp only [sub_nonneg, inv_le_inv₀ zero_lt_two (q_pos X)]
@@ -1313,9 +1305,8 @@ theorem forest_operator_le_volume {n : ℕ} (𝔉 : Forest X n) {f : X → ℂ}
   apply (forest_operator' 𝔉 hf h2f hA sA).trans
   gcongr
   calc
-  _ ≤ eLpNorm (F.indicator (fun x ↦ 1) : X → ℝ) 2 volume := by
-    apply eLpNorm_mono (fun x ↦ ?_)
-    exact (h2f x).trans (le_abs_self _)
+  _ ≤ eLpNorm (F.indicator (fun x ↦ 1) : X → ℝ) 2 volume :=
+    eLpNorm_mono (fun x ↦ (h2f x).trans (le_abs_self _))
   _ ≤ _ := by
     rw [eLpNorm_indicator_const measurableSet_F (by norm_num) (by norm_num)]
     simp

Carleson/ForestOperator/QuantativeEstimate.lean

@@ -463,11 +463,11 @@ lemma density_tree_bound1
   simpa using density_tree_bound_aux hf hc hg h2g hu
 
 omit [TileStructure Q D κ S o] in
--- move somewhere else
+-- TODO: move somewhere else
 lemma _root_.MeasureTheory.BoundedCompactSupport.const_smul (hf : BoundedCompactSupport f) (c : ℝ) :
-  BoundedCompactSupport (c • f) := by
-  simp_rw [Pi.smul_def,Complex.real_smul]
-  apply hf.const_mul
+    BoundedCompactSupport (c • f) := by
+  simp_rw [Pi.smul_def, Complex.real_smul]
+  fun_prop
 
 omit [TileStructure Q D κ S o] [MetricSpace X] in
 -- rename, move somewhere else

Carleson/Operators.lean

@@ -42,12 +42,7 @@ with nontrivial rework in order to move from `Measurable` to `AEStronglyMeasurab
 lemma measurable_carlesonOn {p : 𝔓 X} {f : X → ℂ} (measf : Measurable f) :
     Measurable (carlesonOn p f) := by
   refine (StronglyMeasurable.integral_prod_right ?_).measurable.indicator measurableSet_E
-  refine ((Measurable.mul ?_ measurable_Ks).mul ?_).stronglyMeasurable
-  · have : Measurable fun (p : X × X) ↦ (p.1, p.1) := by fun_prop
-    refine ((Measurable.sub ?_ ?_).const_mul I).cexp <;> apply measurable_ofReal.comp
-    · exact measurable_Q₂
-    · exact measurable_Q₂.comp this
-  · exact measf.comp measurable_snd
+  exact ((Measurable.mul (by fun_prop) measurable_Ks).mul (by fun_prop)).stronglyMeasurable
 
 open Classical in
 /-- The operator `T_ℭ f` defined at the bottom of Section 7.4.
@@ -65,13 +60,8 @@ lemma _root_.MeasureTheory.AEStronglyMeasurable.carlesonOn {p : 𝔓 X} {f : X 
   refine .indicator ?_ measurableSet_E
   refine .integral_prod_right'
     (f := fun z ↦ exp (Complex.I * (Q z.1 z.2 - Q z.1 z.1)) * Ks (𝔰 p) z.1 z.2 * f z.2) ?_
-  refine (AEStronglyMeasurable.mul ?_ aestronglyMeasurable_Ks).mul ?_
-  · apply Measurable.aestronglyMeasurable
-    have : Measurable fun (p : X × X) ↦ (p.1, p.1) := by fun_prop
-    refine ((Measurable.sub ?_ ?_).const_mul I).cexp <;> apply measurable_ofReal.comp
-    · exact measurable_Q₂
-    · exact measurable_Q₂.comp this
-  · exact hf.comp_snd
+  refine (AEStronglyMeasurable.mul (by fun_prop) aestronglyMeasurable_Ks).mul ?_
+  exact hf.comp_snd
 
 lemma _root_.MeasureTheory.AEStronglyMeasurable.carlesonSum {ℭ : Set (𝔓 X)}
     {f : X → ℂ} (hf : AEStronglyMeasurable f) : AEStronglyMeasurable (carlesonSum ℭ f) :=
@@ -156,6 +146,7 @@ theorem BoundedCompactSupport.bddAbove_norm_carlesonOn
       _ = volume.real (closedBall x₀ r₀) * (CK * (eLpNorm f ⊤ volume).toReal) :=
         integral_indicator_const _ measurableSet_closedBall
 
+@[fun_prop]
 theorem BoundedCompactSupport.carlesonOn {f : X → ℂ}
     (hf : BoundedCompactSupport f) : BoundedCompactSupport (carlesonOn p f) where
   memLp_top := by
@@ -175,6 +166,7 @@ theorem BoundedCompactSupport.bddAbove_norm_carlesonSum
   apply BddAbove.range_mono _ fun _ ↦ norm_sum_le ..
   exact .range_finsetSum fun _ _ ↦ hf.bddAbove_norm_carlesonOn _
 
+@[fun_prop]
 theorem BoundedCompactSupport.carlesonSum {ℭ : Set (𝔓 X)} {f : X → ℂ}
     (hf : BoundedCompactSupport f) : BoundedCompactSupport (carlesonSum ℭ f) :=
   .finset_sum (fun _ _ ↦ hf.carlesonOn)
@@ -306,6 +298,7 @@ theorem BoundedCompactSupport.bddAbove_norm_adjointCarleson (hf : BoundedCompact
     · simp only [image_eq_zero_of_notMem_tsupport hy,
         norm_zero, mul_zero, eLpNorm_exponent_top]; positivity
 
+@[fun_prop]
 theorem BoundedCompactSupport.adjointCarleson (hf : BoundedCompactSupport f) :
     BoundedCompactSupport (adjointCarleson p f) where
   memLp_top := by
@@ -342,9 +335,11 @@ theorem BoundedCompactSupport.bddAbove_norm_adjointCarlesonSum
   apply BddAbove.range_mono _ fun _ ↦ norm_sum_le ..
   exact .range_finsetSum fun _ _ ↦ hf.bddAbove_norm_adjointCarleson _
 
+@[fun_prop]
 theorem BoundedCompactSupport.adjointCarlesonSum {ℭ : Set (𝔓 X)}
     (hf : BoundedCompactSupport f) : BoundedCompactSupport (adjointCarlesonSum ℭ f) :=
-  BoundedCompactSupport.finset_sum fun _ _ ↦ hf.adjointCarleson
+  -- TODO: cannot seem to unfold adjointCarlesonSum, so fun_prop cannot apply fully
+  BoundedCompactSupport.finset_sum fun _ _ ↦ by fun_prop
 
 end MeasureTheory
 
@@ -377,7 +372,7 @@ lemma adjointCarleson_adjoint
             gcongr; exact norm_mul_le ..
           _ ≤ ‖g x‖ * 1 * ‖MKD (𝔰 p) x y‖ * ‖f y‖ := by
             gcongr
-            · exact le_of_eq <| RCLike.norm_conj _
+            · exact (RCLike.norm_conj _).le
             · exact norm_indicator_one_le ..
           _ = ‖MKD (𝔰 p) x y‖ * (‖g x‖ * ‖f y‖) := by rw [mul_one, mul_comm ‖g _‖, mul_assoc]
           _ ≤ M₀ *  (‖g x‖ * ‖f y‖) := by gcongr; exact norm_MKD_le_norm_Ks.trans hM₀
@@ -395,13 +390,7 @@ lemma adjointCarleson_adjoint
             .indicator aestronglyMeasurable_const measurableSet_E
           exact this.comp_fst
       · unfold MKD
-        refine .mul ?_ aestronglyMeasurable_Ks
-        apply Measurable.aestronglyMeasurable
-        have : Measurable fun (p : X × X) ↦ (p.1, p.1) :=
-          .prodMk (.fst measurable_id') (.fst measurable_id')
-        refine ((Measurable.sub ?_ ?_).const_mul I).cexp <;> apply measurable_ofReal.comp
-        · exact measurable_Q₂
-        · exact measurable_Q₂.comp this
+        fun_prop
     · apply ae_of_all
       intro z
       refine _root_.trans (hHleH₀ z.1 z.2) ?_
@@ -433,26 +422,25 @@ lemma adjointCarleson_adjoint
           congr; funext; rw [map_mul, ← exp_conj, mul_comm (cexp _)]
           congr; simp; ring
 
+-- Bug: why is `integrable_fun_mul` needed, despite `integrable_mul` existing?
+-- the fun_prop documentation implies it's superfluous. TODO ask on zulip!
+
 /-- `adjointCarlesonSum` is the adjoint of `carlesonSum`. -/
 lemma adjointCarlesonSum_adjoint
     (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (ℭ : Set (𝔓 X)) :
     ∫ x, conj (g x) * carlesonSum ℭ f x = ∫ x, conj (adjointCarlesonSum ℭ g x) * f x := by
   classical calc
     _ = ∫ x, ∑ p with p ∈ ℭ, conj (g x) * carlesonOn p f x := by
       unfold carlesonSum; simp_rw [Finset.mul_sum]
-    _ = ∑ p with p ∈ ℭ, ∫ x, conj (g x) * carlesonOn p f x := by
-      apply integral_finset_sum; intro p _
-      refine hg.conj.mul hf.carlesonOn |>.integrable
+    _ = ∑ p with p ∈ ℭ, ∫ x, conj (g x) * carlesonOn p f x :=
+      integral_finset_sum _ fun p _ ↦ by fun_prop
     _ = ∑ p with p ∈ ℭ, ∫ y, conj (adjointCarleson p g y) * f y := by
       simp_rw [adjointCarleson_adjoint hf hg]
-    _ = ∫ y, ∑ p with p ∈ ℭ, conj (adjointCarleson p g y) * f y := by
-      symm; apply integral_finset_sum; intro p _
-      refine BoundedCompactSupport.mul ?_ hf |>.integrable
-      exact hg.adjointCarleson.conj
+    _ = ∫ y, ∑ p with p ∈ ℭ, conj (adjointCarleson p g y) * f y :=
+      (integral_finset_sum _ fun p _ ↦ by fun_prop).symm
     _ = _ := by congr!; rw [← Finset.sum_mul, ← map_sum]; rfl
 
 lemma integrable_adjointCarlesonSum (s : Set (𝔓 X)) {f : X → ℂ} (hf : BoundedCompactSupport f) :
-    Integrable (adjointCarlesonSum s f ·) :=
-  integrable_finset_sum _ fun i _ ↦ hf.adjointCarleson (p := i).integrable
+    Integrable (adjointCarlesonSum s f ·) := by fun_prop
 
 end Adjoint

Carleson/Psi.lean

@@ -840,6 +840,7 @@ lemma measurable_Ks {s : ℤ} : Measurable (fun x : X × X ↦ Ks s x.1 x.2) :=
   unfold Ks _root_.ψ
   exact measurable_K.mul (by fun_prop)
 
+@[fun_prop]
 lemma aestronglyMeasurable_Ks {s : ℤ} : AEStronglyMeasurable (fun x : X × X ↦ Ks s x.1 x.2) :=
   measurable_Ks.aestronglyMeasurable
 
@@ -850,7 +851,7 @@ lemma integrable_Ks_x {s : ℤ} {x : X} (hD : 1 < (D : ℝ)) : Integrable (Ks s
   rw [← integrableOn_iff_integrable_of_support_subset (s := (ball x r)ᶜ)]
   · refine integrableOn_K_mul ?_ x hr (subset_refl _)
     apply Continuous.integrable_of_hasCompactSupport
-    · exact continuous_ofReal.comp <| continuous_ψ.comp <| (by fun_prop)
+    · unfold «ψ»; fun_prop
     · apply HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall x (D ^ s / 2))
       intro y hy
       rw [mem_support, ne_eq, ofReal_eq_zero, ← ne_eq, ← mem_support, support_ψ (one_lt_realD X)] at hy