From af7cbf573a08dbbb3d370923c68a2a1a2bf0dc36 Mon Sep 17 00:00:00 2001
From: Parcly Taxel <reddeloostw@gmail.com>
Date: Sat, 21 Sep 2024 21:58:58 +0800
Subject: [PATCH] fun_prop

---
 Carleson/Discrete/MainTheorem.lean | 18 +++++++-----------
 Carleson/TileStructure.lean        |  1 +
 2 files changed, 8 insertions(+), 11 deletions(-)

diff --git a/Carleson/Discrete/MainTheorem.lean b/Carleson/Discrete/MainTheorem.lean
index 4dcb35d..5349cca 100644
--- a/Carleson/Discrete/MainTheorem.lean
+++ b/Carleson/Discrete/MainTheorem.lean
@@ -3,8 +3,6 @@ import Carleson.Discrete.ForestComplement
 import Carleson.Discrete.ForestUnion
 
 open MeasureTheory NNReal Set Classical
-noncomputable section
-
 open scoped ShortVariables
 variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X → ℤ} {F G : Set X}
   [MetricSpace X] [ProofData a q K σ₁ σ₂ F G] [TileStructure Q D κ S o]
@@ -13,7 +11,7 @@ variable {X : Type*} {a : ℕ} {q : ℝ} {K : X → X → ℂ} {σ₁ σ₂ : X
 
 /-- The constant used in Proposition 2.0.2,
 which has value `2 ^ (440 * a ^ 3) / (q - 1) ^ 5` in the blueprint. -/
-def C2_0_2 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := C5_1_2 a q + C5_1_3 a q
+noncomputable def C2_0_2 (a : ℝ) (q : ℝ≥0) : ℝ≥0 := C5_1_2 a q + C5_1_3 a q
 
 lemma C2_0_2_pos : C2_0_2 a nnq > 0 := add_pos C5_1_2_pos C5_1_3_pos
 
@@ -28,15 +26,13 @@ theorem discrete_carleson :
   use G', measurable_G', ENNReal.mul_le_of_le_div' exc; intro f measf hf
   calc
     _ ≤ ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖₊ + ‖carlesonSum 𝔓₁ᶜ f x‖₊ := by
-      refine setLIntegral_mono ?_ fun x _ ↦ ?_
-      · exact ((measurable_carlesonSum measf).nnnorm.add
-          (measurable_carlesonSum measf).nnnorm).coe_nnreal_ennreal
-      · norm_cast
-        rw [carlesonSum, ← Finset.sum_filter_add_sum_filter_not _ (· ∈ 𝔓₁ (X := X))]
-        simp_rw [Finset.filter_filter, mem_univ, true_and, carlesonSum, mem_compl_iff]
-        exact nnnorm_add_le ..
+      refine setLIntegral_mono (by fun_prop) fun x _ ↦ ?_
+      norm_cast
+      rw [carlesonSum, ← Finset.sum_filter_add_sum_filter_not _ (· ∈ 𝔓₁ (X := X))]
+      simp_rw [Finset.filter_filter, mem_univ, true_and, carlesonSum, mem_compl_iff]
+      exact nnnorm_add_le ..
     _ = (∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖₊) + ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ᶜ f x‖₊ :=
-      lintegral_add_left ((measurable_carlesonSum measf).nnnorm).coe_nnreal_ennreal _
+      lintegral_add_left (by fun_prop) _
     _ ≤ C5_1_2 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ +
         C5_1_3 a nnq * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ :=
       add_le_add (forest_union hf) (forest_complement hf)
diff --git a/Carleson/TileStructure.lean b/Carleson/TileStructure.lean
index 6e6a06a..6ce99f6 100644
--- a/Carleson/TileStructure.lean
+++ b/Carleson/TileStructure.lean
@@ -126,6 +126,7 @@ We will use this in other places of the formalization as well. -/
 def carlesonSum (ℭ : Set (𝔓 X)) (f : X → ℂ) (x : X) : ℂ :=
   ∑ p ∈ {p | p ∈ ℭ}, carlesonOn p f x
 
+@[fun_prop]
 lemma measurable_carlesonSum {ℭ : Set (𝔓 X)} {f : X → ℂ} (measf : Measurable f) :
     Measurable (carlesonSum ℭ f) :=
   Finset.measurable_sum _ fun _ _ ↦ measurable_carlesonOn measf