Skip to content

Commit

Permalink
move some files to subfolders
Browse files Browse the repository at this point in the history
  • Loading branch information
@fpvandoorn
fpvandoorn committed Aug 14, 2024
1 parent c19ce17 commit bf77db2
Show file tree
Hide file tree
Showing 7 changed files with 11 additions and 88 deletions.
12 changes: 6 additions & 6 deletions BonnAnalysis.lean
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
import BonnAnalysis.ComplexInterpolation
import BonnAnalysis.ConvergingSequences
import BonnAnalysis.ConvolutionTendsToUniformly
import BonnAnalysis.Distributions
import BonnAnalysis.DistributionsExamples
import BonnAnalysis.DistributionsOfVEndo
import BonnAnalysis.Distributions.Basic
import BonnAnalysis.Distributions.ConvolutionTendsToUniformly
import BonnAnalysis.Distributions.Examples
import BonnAnalysis.Distributions.OfVEndo
import BonnAnalysis.Dual
import BonnAnalysis.Examples
import BonnAnalysis.Hadamard
import BonnAnalysis.LorentzSpace
import BonnAnalysis.Plancherel
import BonnAnalysis.Preliminaries.ConvergingSequences
import BonnAnalysis.Preliminaries.UniformConvergenceSequences
import BonnAnalysis.RealInterpolation
import BonnAnalysis.StrongType
import BonnAnalysis.Test
import BonnAnalysis.UniformConvergenceSequences
15 changes: 1 addition & 14 deletions BonnAnalysis/Distributions.lean → BonnAnalysis/Distributions/Basic.lean
View file
Original file line number Diff line number Diff line change
@@ -1,17 +1,4 @@
import Mathlib.Topology.Sequences
import Mathlib.Topology.Defs.Filter
import Mathlib.Topology.Order
import Mathlib.Order.Filter.Basic
import BonnAnalysis.ConvergingSequences
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Topology.UniformSpace.UniformConvergence

import BonnAnalysis.UniformConvergenceSequences
import Mathlib
--import Mathlib.Analysis.InnerProductSpace
-- import Mathlib.Order
-- noncomputable section
--open FourierTransform MeasureTheory Real
import BonnAnalysis.Preliminaries.UniformConvergenceSequences

-- set_option profiler true
namespace MeasureTheory
Expand Down
21 changes: 1 addition & 20 deletions ...Analysis/ConvolutionTendsToUniformly.lean → ...ibutions/ConvolutionTendsToUniformly.lean
View file
Original file line number Diff line number Diff line change
@@ -1,23 +1,4 @@
import Mathlib.Topology.Sequences
import Mathlib.Topology.Defs.Filter
import Mathlib.Topology.Order
import Mathlib.Topology.Algebra.ContinuousAffineMap
import Mathlib.Order.Filter.Basic
import Mathlib.Init.Function
import BonnAnalysis.ConvergingSequences
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Topology.UniformSpace.UniformConvergence
import Mathlib.Data.Set.Pointwise.Basic
import BonnAnalysis.UniformConvergenceSequences
import BonnAnalysis.Distributions
import BonnAnalysis.DistributionsOfVEndo
import Mathlib

import Mathlib.Analysis.Convolution
--import Mathlib.Analysis.InnerProductSpace
-- import Mathlib.Order
-- noncomputable section
--open FourierTransform MeasureTheory Real
import BonnAnalysis.Distributions.OfVEndo


namespace MeasureTheory
Expand Down
23 changes: 1 addition & 22 deletions BonnAnalysis/DistributionsExamples.lean → BonnAnalysis/Distributions/Examples.lean
View file
Original file line number Diff line number Diff line change
@@ -1,25 +1,4 @@
import Mathlib.Topology.Sequences
import Mathlib.Topology.Defs.Filter
import Mathlib.Topology.Order
import Mathlib.Topology.Algebra.ContinuousAffineMap
import Mathlib.Order.Filter.Basic
import Mathlib.Init.Function
import BonnAnalysis.ConvergingSequences
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Topology.UniformSpace.UniformConvergence
import Mathlib.Data.Set.Pointwise.Basic
import BonnAnalysis.UniformConvergenceSequences
import BonnAnalysis.Distributions
import BonnAnalysis.DistributionsOfVEndo
import BonnAnalysis.ConvolutionTendsToUniformly
import Mathlib

import Mathlib.Analysis.Convolution
--import Mathlib.Analysis.InnerProductSpace
-- import Mathlib.Order
-- noncomputable section
--open FourierTransform MeasureTheory Real

import BonnAnalysis.Distributions.ConvolutionTendsToUniformly

namespace MeasureTheory
open MeasureTheory
Expand Down
20 changes: 1 addition & 19 deletions BonnAnalysis/DistributionsOfVEndo.lean → BonnAnalysis/Distributions/OfVEndo.lean
View file
Original file line number Diff line number Diff line change
@@ -1,22 +1,4 @@
import Mathlib.Topology.Sequences
import Mathlib.Topology.Defs.Filter
import Mathlib.Topology.Order
import Mathlib.Topology.Algebra.ContinuousAffineMap
import Mathlib.Order.Filter.Basic
import Mathlib.Init.Function
import BonnAnalysis.ConvergingSequences
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Topology.UniformSpace.UniformConvergence
import Mathlib.Data.Set.Pointwise.Basic
import BonnAnalysis.UniformConvergenceSequences
import BonnAnalysis.Distributions
import Mathlib

import Mathlib.Analysis.Convolution
--import Mathlib.Analysis.InnerProductSpace
-- import Mathlib.Order
-- noncomputable section
--open FourierTransform MeasureTheory Real
import BonnAnalysis.Distributions.Basic


namespace MeasureTheory
Expand Down
0 BonnAnalysis/ConvergingSequences.lean → ...is/Preliminaries/ConvergingSequences.lean
View file
File renamed without changes.
8 changes: 1 addition & 7 deletions ...Analysis/UniformConvergenceSequences.lean → ...minaries/UniformConvergenceSequences.lean
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,4 @@
import Mathlib.Topology.Sequences
import Mathlib.Topology.Defs.Filter
import Mathlib.Topology.Order
import Mathlib.Order.Filter.Basic
import BonnAnalysis.ConvergingSequences
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Topology.UniformSpace.UniformConvergence
import BonnAnalysis.Preliminaries.ConvergingSequences
import Mathlib


Expand Down

0 comments on commit bf77db2

Please sign in to comment.