-
Notifications
You must be signed in to change notification settings - Fork 6
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' into fix-format
- Loading branch information
Showing
17 changed files
with
3,260 additions
and
286 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
version: 2 # Specifies the version of the Dependabot configuration file format | ||
|
||
updates: | ||
# Configuration for dependency updates | ||
- package-ecosystem: "github-actions" # Specifies the ecosystem to check for updates | ||
directory: "/" # Specifies the directory to check for dependencies; "/" means the root directory | ||
schedule: | ||
# Check for updates to GitHub Actions every month | ||
interval: "monthly" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,14 +1,44 @@ | ||
/build | ||
/lake-packages | ||
/.lake | ||
/.cache | ||
## macOS | ||
.DS_Store | ||
## Lake | ||
.lake/* | ||
.cache/* | ||
.devenv/* | ||
.stfolder/* | ||
/lakefile.olean | ||
/lake-packages/* | ||
/build | ||
## Blueprint | ||
/blueprint/lean_decls | ||
/blueprint/print/print.log | ||
/blueprint/web/ | ||
/blueprint/src/web.paux | ||
/blueprint/src/web.bbl | ||
/blueprint/print/ | ||
## Docs | ||
docs/_includes/sorries.md | ||
## TeX | ||
*.aux | ||
*.fdb_latexmk | ||
*.fls | ||
*.lof | ||
*.log | ||
*.lot | ||
*.fls | ||
*.out | ||
*.toc | ||
*.fmt | ||
*.fot | ||
*.cb | ||
*.cb2 | ||
.*.lb | ||
*.bbl | ||
*.bcf | ||
*.blg | ||
*-blx.aux | ||
*-blx.bib | ||
*.run.xml | ||
*.fdb_latexmk | ||
*.synctex | ||
*.synctex(busy) | ||
*.synctex.gz | ||
# Lean blueprint | ||
/blueprint/lean_decls | ||
/blueprint/src/web.bbl | ||
*.synctex.gz(busy) | ||
*.pdfsync |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,8 +1,15 @@ | ||
import BonnAnalysis.ComplexInterpolation | ||
import BonnAnalysis.ConvergingSequences | ||
import BonnAnalysis.ConvolutionTendsToUniformly | ||
import BonnAnalysis.Distributions | ||
import BonnAnalysis.DistributionsExamples | ||
import BonnAnalysis.DistributionsOfVEndo | ||
import BonnAnalysis.Dual | ||
import BonnAnalysis.Examples | ||
import BonnAnalysis.Hadamard | ||
import BonnAnalysis.LorentzSpace | ||
import BonnAnalysis.Plancherel | ||
import BonnAnalysis.RealInterpolation | ||
import BonnAnalysis.StrongType | ||
import BonnAnalysis.Test | ||
import BonnAnalysis.UniformConvergenceSequences |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,192 @@ | ||
import Mathlib.Topology.Sequences | ||
import Mathlib.Topology.Defs.Filter | ||
import Mathlib.Topology.Order | ||
import Mathlib.Order.Filter.Basic | ||
import Mathlib.Tactic.FunProp | ||
-- import Mathlib.Order | ||
-- noncomputable section | ||
|
||
--open FourierTransform MeasureTheory Real | ||
|
||
|
||
namespace MeasureTheory | ||
|
||
universe u v | ||
open Order Set Filter | ||
open Filter | ||
open scoped Topology | ||
|
||
set_option checkBinderAnnotations false | ||
class SubSequence {X : Type u} (a : ℕ → X) where | ||
φ : ℕ → ℕ | ||
hφ : StrictMono φ | ||
--open SubSequence | ||
--@[coe] def coeSubS {X : Type u} {a : ℕ → X} (σ : SubSequence a): ℕ → X := a ∘ σ.φ -- how to not automatically coerce everywhere? | ||
instance {X : Type u} {a : ℕ → X} : CoeFun (SubSequence a) (fun _ => ℕ → X) where | ||
coe σ := a ∘ σ.φ -- how to not automatically coerce everywhere? | ||
--instance {X Y : Type u} {f : X → Y} {a : ℕ → X} : Coe (SubSequence a) (SubSequence (f ∘ a)) where | ||
-- coe σ := ⟨ σ.φ , σ.hφ⟩ | ||
lemma bndOnStrictMono {φ : ℕ → ℕ} (hφ : StrictMono φ) {a : ℕ} : ¬ (φ a < a) := by | ||
intro ass | ||
induction' a with n hn | ||
· exact Nat.not_succ_le_zero (φ 0) ass | ||
· apply hn | ||
have : φ (n + 1) ≤ n := Nat.le_of_lt_succ ass | ||
apply LE.le.trans_lt' this | ||
apply hφ | ||
exact lt_add_one n | ||
lemma subsequencePreservesTop {φ : ℕ → ℕ} | ||
(hφ : StrictMono φ) : map φ atTop ≤ atTop := by | ||
rw [le_def] | ||
intro U hU | ||
simp at hU | ||
obtain ⟨ a , ha⟩ := hU | ||
have : ∃ a' , φ a' ≥ a := by | ||
by_contra ass | ||
push_neg at ass | ||
specialize ass a | ||
apply bndOnStrictMono hφ ass | ||
simp only [mem_map, mem_atTop_sets, ge_iff_le, mem_preimage] | ||
|
||
use this.choose | ||
intro b hb | ||
apply ha | ||
trans | ||
exact this.choose_spec | ||
apply StrictMono.monotone hφ hb | ||
|
||
lemma subSeqConverges' {X : Type u} {ι : Type v} {q : Filter ι}{p : Filter X} {a : ι → X} | ||
{φ : ι → ι} | ||
(hφ : map φ q ≤ q) (pf : Tendsto a q p) : | ||
Tendsto (a ∘ φ) q p := by | ||
intro U hU | ||
rw [tendsto_def] at pf | ||
specialize pf U hU | ||
rw [mem_map] | ||
exact hφ pf | ||
lemma subSeqConverges {X : Type u} {p : Filter X} {a : ℕ → X} | ||
(pf : Tendsto a atTop p) (a' : SubSequence a) : | ||
Tendsto a' atTop p := subSeqConverges' (subsequencePreservesTop a'.hφ) pf | ||
|
||
class ConvergingSequences (X : Type u) where | ||
seq : (ℕ → X) × X → Prop | ||
seq_cnst : ∀ x : X , seq (fun _ => x , x ) | ||
seq_sub : ∀ {a x} , seq ( a, x) → ∀ a' : SubSequence a , seq (a' , x) | ||
|
||
|
||
variable {X : Type u} [ConvergingSequences X] | ||
--notation (priority := high) P "[" A "]" => obj_over (P:=P.1.hom) A | ||
open ConvergingSequences | ||
scoped notation a " ⟶ " x => seq (a , x) | ||
@[simp] def nbh (x : X) : Filter X := by | ||
use {Y | ∀ a , (a ⟶ x) → Y ∈ map a atTop} | ||
· simp | ||
· simp only [mem_map, mem_atTop_sets, ge_iff_le, mem_preimage, mem_setOf_eq] ; | ||
intro Y Z | ||
intro ass hYZ b (hb : b ⟶ x) | ||
specialize ass b hb | ||
obtain ⟨ a , ha⟩ := ass | ||
use a | ||
intro i hi | ||
apply hYZ | ||
exact ha i hi | ||
· intro Y Z hY hZ | ||
intro a ha | ||
rw [inter_mem_iff] | ||
constructor | ||
apply hY a ha | ||
apply hZ a ha | ||
-- def IsSeqClosed (s : Set X) : Prop := ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, (∀ n, x n ∈ s) ∧ seq (x , p) → p ∈ s | ||
|
||
instance fromSeq : TopologicalSpace X := .mkOfNhds nbh | ||
|
||
lemma tendsToNbh {x : X} (a : ℕ → X) (ha : a ⟶ x) : Tendsto a atTop (nbh x) := by | ||
intro N hN | ||
apply hN | ||
exact ha | ||
lemma nbhdCofinalIn𝓝 {x : X} {U} (hU : U ∈ 𝓝 x) : ∃ V ∈ nbh x , V ⊆ U := by | ||
rw [@mem_nhds_iff] at hU | ||
obtain ⟨ V , hV ⟩ := hU | ||
use V | ||
constructor | ||
· apply hV.2.1 | ||
exact hV.2.2 | ||
· exact hV.1 | ||
lemma tendsTo𝓝 {x : X} (a : ℕ → X) (ha : a ⟶ x) : Tendsto a atTop (𝓝 x) := by | ||
intro U hU | ||
obtain ⟨ V , hV ⟩ := nbhdCofinalIn𝓝 hU | ||
apply mem_of_superset ; swap | ||
· exact hV.2 | ||
· apply hV.1 | ||
exact ha | ||
|
||
lemma subSeqCnstrction {a : ℕ → X} {Y : Set (X)} (as : Y ∉ map a atTop) : | ||
∃ (a' : SubSequence a) , ∀ n , a' n ∉ Y := by | ||
simp at as | ||
let φ : ℕ → ℕ := by | ||
intro n | ||
induction n with | ||
| zero => exact (as 0).choose | ||
| succ _ φn => exact ((as (Nat.succ φn)).choose) | ||
use ⟨ φ , by | ||
intro n b | ||
induction b with | ||
| zero => simp | ||
| succ b hb => | ||
intro as' | ||
have : φ n ≤ φ b := by | ||
by_cases h : n = b | ||
· rw [h] ; | ||
· exact le_of_lt (hb <| Nat.lt_of_le_of_ne (Nat.le_of_lt_succ as') h) | ||
exact Nat.lt_of_le_of_lt this (as (Nat.succ (φ b))).choose_spec.1 | ||
⟩ | ||
intro n | ||
simp | ||
induction n with | ||
| zero => exact (as 0).choose_spec.2 | ||
| succ n _ => exact ((as (Nat.succ (φ n))).choose_spec.2) | ||
|
||
lemma seqInNhd {a : ℕ → X} {N : Set X} (hN : N ∈ map a atTop) : ∃ n , a n ∈ N := by | ||
simp at hN | ||
use hN.choose | ||
apply hN.choose_spec | ||
exact le_rfl | ||
|
||
lemma important (x : X) (N : Set X) (p : N ∈ 𝓝 x) : N ∈ nbh x := by | ||
rw [mem_nhds_iff] at p | ||
|
||
|
||
|
||
obtain ⟨ U , ⟨ q , r , p⟩ ⟩ := p | ||
exact mem_of_superset (r x p) q | ||
@[fun_prop] structure SeqContinuous' {Y : Type v} [TopologicalSpace Y] (f : X → Y) : Prop where | ||
seqCont :∀ {x} {a : X} , (x ⟶ a) → Tendsto (f ∘ x) atTop (𝓝 (f a)) | ||
|
||
open SeqContinuous' | ||
@[fun_prop] structure SeqContinuousStrongly {Y : Type v} [ConvergingSequences Y] (f : X → Y) : Prop where | ||
seqCont :∀ {x} {a : X} , (x ⟶ a) → (f ∘ x) ⟶ (f a) | ||
@[fun_prop] lemma continuous_of_SeqContinuous {Y : Type v} [TopologicalSpace Y] {f : X → Y} | ||
(hf : SeqContinuous' f) : Continuous f := by | ||
apply continuous_iff_isClosed.mpr | ||
intro C hC | ||
rw [← @isOpen_compl_iff] | ||
intro x hx a ha | ||
by_contra φ | ||
obtain ⟨ a' , ha' ⟩ := subSeqCnstrction φ | ||
simp at ha' | ||
apply hx | ||
have hC : IsSeqClosed C := IsClosed.isSeqClosed hC | ||
|
||
apply hC | ||
· exact ha' | ||
· intro N hN | ||
have main : map ((f ∘ a) ∘ a'.φ) atTop ≤ map (f ∘ a) atTop := by calc | ||
map ((f ∘ a) ∘ a'.φ) atTop = map (f ∘ a) (map (a'.φ) atTop) := by rw [← Filter.map_compose] ; rfl | ||
_ ≤ map (f ∘ a) atTop := by apply map_mono ; apply subsequencePreservesTop ; exact a'.hφ | ||
apply main | ||
exact hf.seqCont ha hN; | ||
lemma SeqContinuous'OfStrongly {Y : Type v} [ConvergingSequences Y] (f : X → Y) (hf : SeqContinuousStrongly f) : SeqContinuous' f := by | ||
constructor | ||
intro α a hx | ||
apply tendsTo𝓝 | ||
apply hf.seqCont hx |
Oops, something went wrong.