Merge remote-tracking branch 'upstream/master'

.github/workflows/push.yml

@@ -23,6 +23,10 @@ jobs:
     runs-on: ubuntu-latest
     name: Build project
     steps:
+      - name: cleanup
+        run: |
+          find . -name . -o -prune -exec rm -rf -- {} +
+
       - name: Checkout project
         uses: actions/checkout@v2
         with:
@@ -54,8 +58,8 @@ jobs:
             MathlibDoc-
 
 
-      - name: Build documentation
-        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
+      # - name: Build documentation
+      #   run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
 
       - name: Install Python
         uses: actions/setup-python@v4
@@ -76,27 +80,31 @@ jobs:
         run: |
           inv all
 
-      - name: Copy documentation to `docs/docs`
-        run: |
-          sudo chown -R runner docs
-          cp -r .lake/build/doc docs/docs
+      # - name: Copy documentation to `docs/docs`
+      #   run: |
+      #     sudo chown -R runner docs
+      #     cp -r .lake/build/doc docs/docs
 
-      - name: Bundle dependencies
-        uses: ruby/setup-ruby@v1
-        with:
-          working-directory: docs
-          ruby-version: "3.0" # Not needed with a .ruby-version file
-          bundler-cache: true # runs 'bundle install' and caches installed gems automatically
+      # - name: Bundle dependencies
+      #   uses: ruby/setup-ruby@v1
+      #   with:
+      #     working-directory: docs
+      #     ruby-version: "3.0" # Not needed with a .ruby-version file
+      #     bundler-cache: true # runs 'bundle install' and caches installed gems automatically
 
-      - name: Bundle website
-        working-directory: docs
-        run: JEKYLL_ENV=production bundle exec jekyll build
+      # - name: Bundle website
+      #   working-directory: docs
+      #   run: JEKYLL_ENV=production bundle exec jekyll build
 
       - name: Upload docs & blueprint artifact
         uses: actions/upload-pages-artifact@v1
         with:
-          path: docs/_site
+          path: docs/
 
       - name: Deploy to GitHub Pages
         id: deployment
         uses: actions/deploy-pages@v1
+
+      #  - name: Make sure the cache works
+      #    run: |
+          #  mv docs/docs .lake/build/doc

BonnAnalysis/ComplexInterpolation.lean

@@ -1,12 +1,14 @@
 import Mathlib.Analysis.Complex.AbsMax
 import Mathlib.Order.Filter.Basic
+import Mathlib.Order.Filter.Basic
 import BonnAnalysis.Dual
 import Mathlib.Topology.MetricSpace.Sequences
 import Mathlib.Analysis.Complex.HalfPlane
 import Mathlib.Analysis.Complex.ReImTopology
 
 noncomputable section
 
+open NNReal ENNReal NormedSpace MeasureTheory Set Complex Bornology Filter
 open NNReal ENNReal NormedSpace MeasureTheory Set Complex Bornology Filter
 
 variable {α β E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {n : MeasurableSpace β} {p q : ℝ≥0∞}
@@ -175,6 +177,7 @@ theorem DiffContOnCl.norm_le_pow_mul_pow''' {f : ℂ → ℂ}
     (h2f : IsBounded (f '' { z | z.re ∈ Icc 0 1}))
     (h₀f : ∀ y : ℝ, ‖f (I * y)‖ ≤ 1) (h₁f : ∀ y : ℝ, ‖f (1 + I * y)‖ ≤ 1)
     {y t s : ℝ} (ht : 0 ≤ t) (hs : 0 ≤ s) (hts : t + s = 1) (htop: Tendsto (fun y ↦ (sup_at_height f y)) atTop (nhds  0)) (hbot: Tendsto (fun y ↦ (sup_at_height f y)) atBot (nhds 0) ) :
+    {y t s : ℝ} (ht : 0 ≤ t) (hs : 0 ≤ s) (hts : t + s = 1) (htop: Tendsto (fun y ↦ (sup_at_height f y)) atTop (nhds  0)) (hbot: Tendsto (fun y ↦ (sup_at_height f y)) atBot (nhds 0) ) :
     ‖f (t + I * y)‖ ≤ 1 := by{
 
       have ht' : t ≤ 1 := by{
@@ -695,6 +698,12 @@ theorem DiffContOnCl.norm_le_pow_mul_pow'' {f : ℂ → ℂ}
       filter_upwards with ε hε
       simp at hε
       exact perturb_bound_strip hε hf h2f h₀f h₁f ht hs hts
+      have := perturb_pointwise_norm_converge f (t+I*y)
+      apply @le_of_tendsto _ _ _ _ _ (fun ε ↦ Complex.abs (perturb f ε (t + I * y))) _ _ _ _ this
+      rw[eventually_nhdsWithin_iff]
+      filter_upwards with ε hε
+      simp at hε
+      exact perturb_bound_strip hε hf h2f h₀f h₁f ht hs hts
     }
 
 
@@ -715,6 +724,15 @@ theorem DiffContOnCl.norm_le_pow_mul_pow₀₁ {f : ℂ → ℂ}
         exact hts.symm
       }
 
+
+      have hts'' : s = 1-t := by {
+        symm
+        -- Not sure why this is so messed up if I don't make it explicit
+        rw[@sub_eq_of_eq_add ℝ _ (1:ℝ) t s]
+        rw[add_comm]
+        exact hts.symm
+      }
+
       let g:= fun z ↦ M₀ ^ (z-1) * M₁ ^(-z) * (f z)
       let p₁ : ℂ → ℂ := fun z ↦ M₀ ^ (z-1)
       let p₂ : ℂ → ℂ := fun z ↦ M₁ ^(-z)
@@ -775,6 +793,51 @@ theorem DiffContOnCl.norm_le_pow_mul_pow₀₁ {f : ℂ → ℂ}
       }
 
 
+
+      have h2g:  IsBounded (g '' { z | z.re ∈ Icc 0 1}) := by {
+        obtain ⟨R, hR⟩   := (Metric.isBounded_iff_subset_ball 0).mp h2f
+        simp only [subset_def, mem_image] at hR
+        have hR' : ∀ x ∈ {z | z.re ∈ Icc 0 1}, Complex.abs (f x) < R := by{
+          intro x hx
+          specialize hR (f x) (by use x)
+          simp at hR
+          assumption
+        }
+
+        rw[Metric.isBounded_image_iff]
+        let A := max 1 (1/M₀)
+        let B := max 1 (1/M₁)
+        use 2*A*B*R
+        intro z hz z' hz'
+        dsimp at hz
+        dsimp at hz'
+        simp_rw[g]
+        rw[Complex.dist_eq]
+
+        have : Complex.abs (↑M₀ ^ (z - 1) * ↑M₁ ^ (-z) * f z - ↑M₀ ^ (z' - 1) * ↑M₁ ^ (-z') * f z') ≤ Complex.abs (↑M₀ ^ (z - 1) * ↑M₁ ^ (-z) * f z) + Complex.abs (- ↑M₀ ^ (z' - 1) * ↑M₁ ^ (-z') * f z') := by{
+          have := AbsoluteValue.add_le Complex.abs (↑M₀ ^ (z - 1) * ↑M₁ ^ (-z) * f z) (- ↑M₀ ^ (z' - 1) * ↑M₁ ^ (-z') * f z')
+          simp at this
+          simp
+          exact this
+          }
+
+        simp at this
+        calc
+        Complex.abs (↑M₀ ^ (z - 1) * ↑M₁ ^ (-z) * f z - ↑M₀ ^ (z' - 1) * ↑M₁ ^ (-z') * f z') ≤ Complex.abs (↑M₀ ^ (z - 1)) * Complex.abs (↑M₁ ^ (-z)) * Complex.abs (f z) +
+    Complex.abs (↑M₀ ^ (z' - 1)) * Complex.abs (↑M₁ ^ (-z')) * Complex.abs (f z') := this
+      _ ≤ A * B * R + A * B * R := by{
+        gcongr
+        · exact pow_bound₀ hM₀ hz
+        · exact pow_bound₁ hM₁ hz
+        · apply le_of_lt; apply hR' z; exact hz
+        · exact pow_bound₀ hM₀ hz'
+        · exact pow_bound₁ hM₁ hz'
+        · apply le_of_lt; apply hR' z'; exact hz'
+      }
+      _ = 2 * A * B * R := by ring
+      }
+
+
       have h₀g : ∀ y : ℝ, ‖g (I * y)‖ ≤ 1 := by {
         intro y
         simp [g]
@@ -869,6 +932,17 @@ theorem DiffContOnCl.norm_le_pow_mul_pow₀₁ {f : ℂ → ℂ}
       simp
       rw[← mul_assoc]
       exact hgoal
+
+      have hM₁': M₁^(-t)>0 := Real.rpow_pos_of_pos hM₁ (-t)
+      have hM₀': M₀^(t-1)>0 := Real.rpow_pos_of_pos hM₀ (t-1)
+      rw[← mul_le_mul_left hM₁',← mul_le_mul_left hM₀']
+      nth_rewrite 2 [mul_comm (M₁^(-t)), ← mul_assoc]
+      rw[mul_assoc, mul_assoc, ← Real.rpow_add hM₁ t (-t)]
+      simp[hts'']
+      rw[ ← Real.rpow_add hM₀ (t-1) (1-t)]
+      simp
+      rw[← mul_assoc]
+      exact hgoal
     }
 
 theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a<b)
@@ -885,6 +959,7 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a<b
           exact hts.symm
         }
 
+      -- DUPLICATE FROM PREVIOUS PROOF
       -- DUPLICATE FROM PREVIOUS PROOF
       have hts'' : s = 1-t := by {
         symm
@@ -942,6 +1017,22 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a<b
             _ = b := by simp
       }
 
+        let h : ℂ → ℂ := fun z ↦ a + (z.re *(b-a)) + I*z.im
+        have hcomp: g = f ∘ h := rfl
+        rw[hcomp]
+        apply DiffContOnCl.comp (s:={ z | z.re ∈ Ioo a b})
+        · exact hf
+        · sorry --not sure what the quickest way of doing this is supposed to be
+        · simp[h, MapsTo]
+          intro z hz₀ hz₁
+          constructor
+          · apply Real.mul_pos hz₀
+            simp[hab]
+          · calc
+            a + z.re * (b-a) < a + 1 *(b - a) := by gcongr; simp[hab]
+            _ = b := by simp
+      }
+
       have h2g: IsBounded (g '' { z | z.re ∈ Icc 0 1}) := by{
         simp only [g]
         apply IsBounded.subset h2f
@@ -1024,16 +1115,14 @@ theorem DiffContOnCl.norm_le_pow_mul_pow {a b : ℝ} {f : ℂ → ℂ} (hab: a<b
 lemma ENNReal.rpow_add_of_pos {x : ENNReal} (y : ℝ) (z : ℝ) (hy : 0 < y) (hz : 0 < z) :
 x ^ (y + z) = x ^ y * x ^ z := by
   cases x with
-  | top =>
-      simp [hy, hz, add_pos hy hz]
+  | top => simp [hy, hz, add_pos hy hz]
   | coe x =>
       rcases eq_or_ne ↑x 0 with hx0 | hx0'
-      simp [hx0, hy, hz, add_pos hy hz]
-      apply ENNReal.rpow_add
-      <;> simp [hx0']
+      simp only [hx0, coe_zero, add_pos hy hz, zero_rpow_of_pos, hy, hz, mul_zero]
+      apply ENNReal.rpow_add <;> simp [hx0']
 
-lemma ENNReal.essSup_const_rpow (f : α → ℝ≥0∞) {r : ℝ} (hr : 0 < r) : (essSup f μ) ^ r = essSup (fun x ↦ (f x) ^ r) μ := by
-  apply OrderIso.essSup_apply (g := ENNReal.orderIsoRpow r hr)
+lemma ENNReal.essSup_const_rpow (f : α → ℝ≥0∞) {r : ℝ} (hr : 0 < r) : (essSup f μ) ^ r = essSup (fun x ↦ (f x) ^ r) μ :=
+  OrderIso.essSup_apply (g := ENNReal.orderIsoRpow r hr) _ _
 
 def InSegment.toIsConjugateExponent (p₀ p₁ p : ℝ≥0∞) (t s : ℝ≥0)  (hp₀ : 0 < p₀)
 (hp₁ : 0 < p₁) (hp₀₁ : p₀ < p₁) (hp : s * p₀⁻¹ + t * p₁⁻¹ = p⁻¹)
@@ -1102,7 +1191,7 @@ lemma lintegral_mul_le_segment_exponent_aux (p₀ p₁ p : ℝ≥0∞) (t s : 
   rw [toReal_inv, inv_inv, ← mul_assoc, ← mul_assoc, mul_comm _ p.toReal, mul_assoc p.toReal, mul_comm t.toReal, ← mul_assoc, mul_assoc _ t.toReal,
   mul_inv_cancel (ENNReal.toReal_ne_zero.mpr ⟨hp0', hpt'⟩), mul_inv_cancel (by rwa [NNReal.coe_ne_zero]), one_mul, one_mul]
 
-  repeat' simp only [toReal_mul, coe_toReal, mul_inv_rev, one_div, inv_inv, ← mul_assoc, ENNReal.toReal_inv]
+  repeat' simp [← mul_assoc, ENNReal.toReal_inv]
 
 lemma lintegral_mul_le_segment_exponent (p₀ p₁ p : ℝ≥0∞) (t s : ℝ≥0) (hp₀ : 0 < p₀) (hp₁ : 0 < p₁) (hp₀₁ : p₀ < p₁)
 (hp : s * p₀⁻¹ + t * p₁⁻¹ = p⁻¹) (hst : s + t = 1)
@@ -1115,8 +1204,7 @@ lemma lintegral_mul_le_segment_exponent (p₀ p₁ p : ℝ≥0∞) (t s : ℝ≥
 
   rcases eq_or_ne t 0 with ht0 | ht0'
   simp only [ht0, add_zero] at hst
-  simp only [hst, ENNReal.coe_one, one_mul, ht0, ENNReal.coe_zero, zero_mul, add_zero,
-  inv_inj] at hp
+  simp only [hst, ENNReal.coe_one, one_mul, ht0, ENNReal.coe_zero, zero_mul, add_zero, inv_inj] at hp
   simp only [hp, hst, NNReal.coe_one, ENNReal.rpow_one, ht0, NNReal.coe_zero, ENNReal.rpow_zero, mul_one, le_refl]
 
   rcases eq_or_ne s 0 with hs0 | hs0'