Merge branch 'LL/dotNotation' into TestLeanCopilot

LorenzoLuccioli · Aug 30, 2024 · 0cb5329 · 0cb5329
2 parents 63c3a31 + afa0751
commit 0cb5329
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 21 deletions.
diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean
@@ -541,23 +541,18 @@ lemma fDiv_add_measure_le (μ₁ μ₂ ν : Measure α) [IsFiniteMeasure μ₁]
   calc fDiv f (ν.withDensity (∂μ₁/∂ν) + ν.withDensity (∂μ₂/∂ν)) ν +
       derivAtTop f * (↑(μ₁.singularPart ν .univ) + ↑(μ₂.singularPart ν .univ))
     = fDiv f (ν.withDensity (∂μ₁/∂ν) + ν.withDensity (∂μ₂/∂ν)) ν
-      + derivAtTop f * μ₁.singularPart ν .univ
-      + derivAtTop f * μ₂.singularPart ν .univ := by
+      + derivAtTop f * μ₁.singularPart ν .univ + derivAtTop f * μ₂.singularPart ν .univ := by
         simp_rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)]
         rw [add_assoc, EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg]
   _ ≤ fDiv f (ν.withDensity (∂μ₁/∂ν)) ν + derivAtTop f * ν.withDensity (∂μ₂/∂ν) .univ
-      + derivAtTop f * μ₁.singularPart ν .univ
-      + derivAtTop f * μ₂.singularPart ν .univ := by
+      + derivAtTop f * μ₁.singularPart ν .univ + derivAtTop f * μ₂.singularPart ν .univ := by
         gcongr
         exact fDiv_add_measure_le_of_ac (withDensity_absolutelyContinuous _ _)
           (withDensity_absolutelyContinuous _ _) hf hf_cvx
-  _ = fDiv f (ν.withDensity (∂μ₁/∂ν)) ν
-      + derivAtTop f * μ₁.singularPart ν .univ
-      + derivAtTop f * μ₂.singularPart ν .univ
-      + derivAtTop f * ν.withDensity (∂μ₂/∂ν) .univ := by
+  _ = fDiv f (ν.withDensity (∂μ₁/∂ν)) ν + derivAtTop f * μ₁.singularPart ν .univ
+      + derivAtTop f * μ₂.singularPart ν .univ + derivAtTop f * ν.withDensity (∂μ₂/∂ν) .univ := by
         abel
-  _ = fDiv f (ν.withDensity (∂μ₁/∂ν)) ν
-      + derivAtTop f * μ₁.singularPart ν .univ
+  _ = fDiv f (ν.withDensity (∂μ₁/∂ν)) ν + derivAtTop f * μ₁.singularPart ν .univ
       + derivAtTop f * (↑(μ₂.singularPart ν .univ) + ↑(ν.withDensity (∂μ₂/∂ν) .univ)) := by
         simp_rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)]
         rw [add_assoc, EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg]
@@ -600,13 +595,13 @@ lemma fDiv_le_zero_add_top [IsFiniteMeasure μ] [IsFiniteMeasure ν]
       + derivAtTop f * μ.singularPart ν .univ := by
         gcongr
         exact fDiv_le_zero_add_top_of_ac (withDensity_absolutelyContinuous _ _) hf hf_cvx
-  _ ≤ f 0 * ν .univ + derivAtTop f * μ .univ := by
-        rw [add_assoc]
-        gcongr
-        conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
-        simp only [Measure.coe_add, Pi.add_apply, EReal.coe_ennreal_add]
-        simp_rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)]
-        rw [EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg]
+    _ ≤ f 0 * ν .univ + derivAtTop f * μ .univ := by
+      rw [add_assoc]
+      gcongr
+      conv_rhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
+      simp only [Measure.coe_add, Pi.add_apply, EReal.coe_ennreal_add]
+      simp_rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)]
+      rw [EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg]
 
 section derivAtTopTop
 

diff --git a/TestingLowerBounds/FDiv/CompProd.lean b/TestingLowerBounds/FDiv/CompProd.lean
@@ -321,8 +321,7 @@ lemma integral_f_rnDeriv_mul_le_integral [CountableOrCountablyGenerated α β]
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0))
     (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η))
     (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) :
-    ∫ x, f ((∂μ/∂ν) x * κ x .univ).toReal ∂ν
-      ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η) := by
+    ∫ x, f ((∂μ/∂ν) x * κ x .univ).toReal ∂ν ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η) := by
   rw [Measure.integral_compProd h_int]
   refine integral_mono_ae ?_ ?_ ?_
   · exact integrable_f_rnDeriv_mul_kernel μ ν κ η hf hf_cvx hf_cont h_int hκη
@@ -524,8 +523,7 @@ lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α
         congr
         rw [singularPart_compProd]
         simp only [Measure.coe_add, Pi.add_apply]
-        rw [Measure.compProd_apply .univ]
-        rw [Measure.compProd_apply .univ]
+        simp_rw [Measure.compProd_apply .univ]
         simp only [Measure.singularPart_singularPart, Set.preimage_univ]
         rw [← lintegral_add_right]
         · rw [← lintegral_one]