Merge branch 'master' into complexinter_pr

.github/workflows/push.yml

@@ -23,25 +23,24 @@ 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:
           fetch-depth: 0
 
       - name: Install elan
-        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0 # Install Lean 4
+
+      - name: Update docgen4
+        run: ~/.elan/bin/lake -R -Kenv=dev update «doc-gen4»
 
       - name: Get cache
         run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
 
       - name: Build project
         run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis
 
-
       - name: Cache mathlib docs
         uses: actions/cache@v3
         with:
@@ -55,56 +54,55 @@ jobs:
             !.lake/build/doc/declarations/declaration-data-BonnAnalysis*
           key: MathlibDoc-${{ hashFiles('lake-manifest.json') }}
           restore-keys: |
-            MathlibDoc-
+            MathlibDoc- # Cache Mathlib documentation to save rebuild time
 
-
-      # - name: Build documentation
-      #   run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs
+      - name: Build documentation
+        run: ~/.elan/bin/lake -Kenv=dev build BonnAnalysis:docs # Build project documentation
 
       - name: Install Python
         uses: actions/setup-python@v4
         with:
           python-version: '3.9'
-          cache: 'pip' # caching pip dependencies
+          cache: 'pip'
 
       - name: Install blueprint apt dependencies
         run: |
           sudo apt-get update
-          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full
+          sudo apt-get install -y graphviz libgraphviz-dev pdf2svg dvisvgm texlive-full # Install necessary system packages for blueprint
 
       - name: Install blueprint dependencies
         run: |
-          cd blueprint && pip install -r requirements.txt
+          cd blueprint && pip install -r requirements.txt # Install Python dependencies for blueprint
 
       - name: Build blueprint and copy to `docs/blueprint`
+        run: inv all
+
+      - name: Remove lake files from documentation
         run: |
-          inv all
+          find .lake/build/doc -name "*.trace" -delete
+          find .lake/build/doc -name "*.hash" -delete
 
-      # - 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 # Copy the built documentation to the correct directory
 
-      # - 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"
+          bundler-cache: true
 
-      # - 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 # Build the Jekyll site for production
 
       - name: Upload docs & blueprint artifact
         uses: actions/upload-pages-artifact@v1
         with:
-          path: docs/
+          path: docs/_site
 
       - 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
+        uses: actions/deploy-pages@v1

BonnAnalysis/ComplexInterpolation.lean

@@ -30,12 +30,9 @@ variable {α β E E₁ E₂ E₃ : Type*} {m : MeasurableSpace α} {n : Measurab
 -- All these names are probably very bad
 lemma Real.pow_le_pow_iff {M:ℝ} (hM: M>0) (a b : ℝ) : M^a ≤ M^b ↔ ((1 ≤ M ∧ a ≤ b ) ∨ (M ≤ 1 ∧ b ≤ a)) := by{
   have hMb : M^(-b) > 0 := Real.rpow_pos_of_pos hM (-b)
-  rw[← mul_le_mul_right hMb, ←Real.rpow_add, ← Real.rpow_add]
+  rw [← mul_le_mul_right hMb, ←Real.rpow_add hM, ← Real.rpow_add hM, add_right_neg, Real.rpow_zero,
+    Real.rpow_le_one_iff_of_pos hM]
   simp
-  rw[Real.rpow_le_one_iff_of_pos hM]
-  · simp
-  · exact hM
-  · exact hM
 }
 
 
@@ -1143,31 +1140,38 @@ lemma lintegral_mul_le_segment_exponent (p₀ p₁ p : ℝ≥0∞) (t s : ℝ≥
       repeat rw [mul_assoc, mul_inv_cancel (ENNReal.toReal_ne_zero.mpr ⟨hp0', hpt'⟩), mul_one]
       repeat' apply ENNReal.rpow_ne_top_of_nonneg (mul_nonneg (NNReal.coe_nonneg _) ENNReal.toReal_nonneg) (by assumption)
 
-variable (E p q μ) in
-/-- The additive subgroup of `α →ₘ[μ] E` consisting of the simple functions in both
-`L^p` and `L^q`. This is denoted `U` in [Ian Tice]. -/
-def Lp.simpleFunc2 : AddSubgroup (α →ₘ[μ] E) :=
-  (Lp.simpleFunc E p μ).map (AddSubgroup.subtype _) ⊓
-  (Lp.simpleFunc E q μ).map (AddSubgroup.subtype _)
+
+/-- An operator has strong type (p, q) if it is bounded as an operator on `L^p → L^q`.
+`HasStrongType T p p' μ ν c` means that `T` has strong type (p, q) w.r.t. measures `μ`, `ν`
+and constant `c`.  -/
+def HasStrongType {E E' α α' : Type*} [NormedAddCommGroup E] [NormedAddCommGroup E']
+    {_x : MeasurableSpace α} {_x' : MeasurableSpace α'} (T : (α → E) → (α' → E'))
+    (p p' : ℝ≥0∞) (μ : Measure α) (ν : Measure α') (c : ℝ≥0) : Prop :=
+  ∀ f : α → E, Memℒp f p μ → AEStronglyMeasurable (T f) ν ∧ snorm (T f) p' ν ≤ c * snorm f p μ
+
+-- variable (E p q μ) in
+-- /-- The additive subgroup of `α →ₘ[μ] E` consisting of the simple functions in both
+-- `L^p` and `L^q`. This is denoted `U` in [Ian Tice]. -/
+-- def Lp.simpleFunc2 : AddSubgroup (α →ₘ[μ] E) :=
+--   (Lp.simpleFunc E p μ).map (AddSubgroup.subtype _) ⊓
+--   (Lp.simpleFunc E q μ).map (AddSubgroup.subtype _)
 
 /- to do: `f ∈ Lp.simpleFunc2 E p q μ` iff
 `snorm f p μ < ∞ ∧ snorm f q μ < ∞ ∧ f is a simple function`. -/
 
-/-- A normed operator `T` is bounded on `Lp.simpleFunc2 p₀ p₁ q` w.r.t. the `L^p₀`
-where the codomain uses the `L^q` norm. -/
-def SBoundedBy (T : (α →ₘ[μ] E₁) → β →ₘ[ν] E₂) (p₀ p₁ q : ℝ≥0∞) (C : ℝ) : Prop :=
-  ∀ (f : α →ₘ[μ] E₁), f ∈ Lp.simpleFunc2 E₁ p₀ p₁ μ →
-  snorm (T f) q ν ≤ ENNReal.ofReal C * snorm f p₀ μ
+-- /-- A normed operator `T` is bounded on `Lp.simpleFunc2 p₀ p₁ q` w.r.t. the `L^p₀`
+-- where the codomain uses the `L^q` norm. -/
+-- def SBoundedBy (T : (α →ₘ[μ] E₁) → β →ₘ[ν] E₂) (p₀ p₁ q : ℝ≥0∞) (C : ℝ) : Prop :=
+--   ∀ (f : α →ₘ[μ] E₁), f ∈ Lp.simpleFunc2 E₁ p₀ p₁ μ →
+--   snorm (T f) q ν ≤ ENNReal.ofReal C * snorm f p₀ μ
 
 /-- Riesz-Thorin interpolation theorem -/
-theorem exists_lnorm_le_of_subadditive_of_lbounded {p₀ p₁ q₀ q₁ : ℝ≥0∞} {M₀ M₁ : ℝ}
+theorem exists_lnorm_le_of_subadditive_of_lbounded {p₀ p₁ q₀ q₁ : ℝ≥0∞} {M₀ M₁ : ℝ≥0}
     (hM₀ : 0 < M₀) (hM₁ : 0 < M₁)
     (hν : q₀ = ∞ → q₁ = ∞ → SigmaFinite ν)
-    (T : Lp.simpleFunc2 E p q μ)
-    (T : (α →ₘ[μ] E₁) →ₗ[ℂ] β →ₘ[ν] E₂)
-    (h₀T : SBoundedBy T p₀ p₁ q₀ M₀)
-    (h₁T : SBoundedBy T p₁ p₀ q₁ M₁)
+    (T : (α → E₁) →ₗ[ℂ] β → E₂)
+    (h₀T : HasStrongType T p₀ q₀ μ ν M₀)
+    (h₁T : HasStrongType T p₁ q₁ μ ν M₁)
     {θ η : ℝ≥0} (hθη : θ + η = 1)
-    {p q : ℝ≥0∞} (hp : p⁻¹ = (1 - θ) / p₀ + θ / p₁) (hr : q⁻¹ = (1 - θ) / q₀ + θ / q₁)
-    (f : α →ₘ[μ] E₁) (hf : f ∈ Lp.simpleFunc2 E₁ p₀ p₁ μ) :
-    snorm (T f) q ν ≤ ENNReal.ofReal (M₀ ^ (η : ℝ) * M₁ ^ (θ : ℝ)) * snorm f p μ := by sorry
+    {p q : ℝ≥0∞} (hp : p⁻¹ = (1 - θ) / p₀ + θ / p₁) (hr : q⁻¹ = (1 - θ) / q₀ + θ / q₁) :
+    HasStrongType T p q μ ν (M₀ ^ (η : ℝ) * M₁ ^ (θ : ℝ)) := by sorry