diff --git a/meta/src/main/java/org/arend/lib/error/LinearSolverError.java b/meta/src/main/java/org/arend/lib/error/LinearSolverError.java index d0a0f047..498329a3 100644 --- a/meta/src/main/java/org/arend/lib/error/LinearSolverError.java +++ b/meta/src/main/java/org/arend/lib/error/LinearSolverError.java @@ -16,26 +16,38 @@ public class LinearSolverError extends TypecheckingError { private final ExpressionPrettifier prettifier; + private final Equation equation; private final List> equations; - public LinearSolverError(ExpressionPrettifier prettifier, boolean isContradiction, List> equations, @Nullable ConcreteSourceNode cause) { - super(isContradiction ? "Cannot infer a contradiction" : "Cannot solve the equation", cause); + public LinearSolverError(ExpressionPrettifier prettifier, Equation equation, List> equations, @Nullable ConcreteSourceNode cause) { + super(equation == null ? "Cannot infer a contradiction" : "Cannot solve the equation", cause); + this.equation = equation; this.prettifier = prettifier; this.equations = equations; } + private Doc getEquationDoc(Equation equation, PrettyPrinterConfig ppConfig) { + String op = switch (equation.operation) { + case LESS -> "<"; + case LESS_OR_EQUALS -> "<="; + case EQUALS -> "="; + }; + return hang(termDoc(equation.lhsTerm, prettifier, ppConfig), hang(text(op), termDoc(equation.rhsTerm, prettifier, ppConfig))); + } + @Override public Doc getBodyDoc(PrettyPrinterConfig ppConfig) { - if (equations.isEmpty()) return nullDoc(); + if (equations.isEmpty() && equation == null) return nullDoc(); List docs = new ArrayList<>(equations.size()); for (Equation equation : equations) { - String op = switch (equation.operation) { - case LESS -> "<"; - case LESS_OR_EQUALS -> "<="; - case EQUALS -> "="; - }; - docs.add(hang(termDoc(equation.lhsTerm, prettifier, ppConfig), hang(text(op), termDoc(equation.rhsTerm, prettifier, ppConfig)))); + docs.add(getEquationDoc(equation, ppConfig)); } - return hang(text("Assumptions:"), vList(docs)); + Doc result = hang(text("Assumptions:"), vList(docs)); + return equation == null ? result : vList(hang(text("Equation:"), getEquationDoc(equation, ppConfig)), result); + } + + @Override + public boolean hasExpressions() { + return !(equations.isEmpty() && equation == null); } } diff --git a/meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java b/meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java index f372239f..240485af 100644 --- a/meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java +++ b/meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java @@ -48,10 +48,14 @@ public LinearSolver(ExpressionTypechecker typechecker, ConcreteSourceNode marker factory = ext.factory.withData(marker); } + private CoreClassDefinition getInstanceClass() { + return ext.equationMeta.LinearlyOrderedSemiring; + } + private CoreExpression findInstance(CoreExpression type, boolean reportError) { - TypedExpression instance = typechecker.findInstance(ext.equationMeta.LinearlyOrderedSemiring, type, null, marker); + TypedExpression instance = type == null ? null : typechecker.findInstance(getInstanceClass(), type, null, marker); if (instance == null) { - if (reportError) errorReporter.report(new InstanceInferenceError(typechecker.getExpressionPrettifier(), ext.equationMeta.LinearlyOrderedSemiring.getRef(), type, marker)); + if (reportError) errorReporter.report(new InstanceInferenceError(typechecker.getExpressionPrettifier(), getInstanceClass().getRef(), type, marker)); return null; } return instance.getExpression(); @@ -97,13 +101,13 @@ private Hypothesis typeToEquation(CoreExpression type, CoreBindi if (field == ext.equationMeta.less || field == ext.equationMeta.lessOrEquals) { CoreExpression arg = fieldCall.getArgument(); CoreExpression argType = arg.computeType().normalize(NormalizationMode.WHNF); - if (argType instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(ext.equationMeta.LinearlyOrderedSemiring)) { + if (argType instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(getInstanceClass())) { return new Hypothesis<>(expr, arg, field == ext.equationMeta.less ? Equation.Operation.LESS : Equation.Operation.LESS_OR_EQUALS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE); } else { if (reportError) errorReporter.report(new TypeError(typechecker.getExpressionPrettifier(), "", argType, marker) { @Override public LineDoc getShortHeaderDoc(PrettyPrinterConfig ppConfig) { - return DocFactory.hList(DocFactory.text("The type of the equation should be "), DocFactory.refDoc(ext.equationMeta.LinearlyOrderedSemiring.getRef())); + return DocFactory.hList(DocFactory.text("The type of the equation should be "), DocFactory.refDoc(getInstanceClass().getRef())); } }); return null; @@ -118,14 +122,21 @@ public LineDoc getShortHeaderDoc(PrettyPrinterConfig ppConfig) { } if (relationData.defCall.getDefinition() == ext.equationMeta.addGroupLess) { - return new Hypothesis<>(expr, relationData.defCall.getDefCallArguments().get(0), Equation.Operation.LESS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE); + CoreExpression instance = relationData.defCall.getDefCallArguments().get(0); + TypedExpression typedInstance = instance.computeTyped(); + CoreExpression instanceType = typedInstance.getType().normalize(NormalizationMode.WHNF); + if (!(instanceType instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(getInstanceClass()))) { + instance = findInstance(instanceType instanceof CoreClassCallExpression classCall ? Utils.getClassifyingExpression(classCall, typedInstance) : null, reportError); + if (instance == null) return null; + } + return new Hypothesis<>(expr, instance, Equation.Operation.LESS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE); } var pair = instanceCache.computeIfAbsent(relationData.defCall.getDefinition(), def -> { DefImplInstanceSearchParameters parameters = new DefImplInstanceSearchParameters(def) { @Override protected List getRelationFields(CoreClassDefinition classDef) { - return classDef.isSubClassOf(ext.equationMeta.LinearlyOrderedSemiring) ? Arrays.asList(ext.equationMeta.less, ext.equationMeta.lessOrEquals) : Collections.emptyList(); + return classDef.isSubClassOf(getInstanceClass()) ? Arrays.asList(ext.equationMeta.less, ext.equationMeta.lessOrEquals) : Collections.emptyList(); } }; TypedExpression instance = typechecker.findInstance(parameters, null, null, marker); @@ -583,7 +594,7 @@ public TypedExpression solve(CoreExpression expectedType, ConcreteExpression hin } } - errorReporter.report(new LinearSolverError(typechecker.getExpressionPrettifier(), resultEquation == null, rules, marker)); + errorReporter.report(new LinearSolverError(typechecker.getExpressionPrettifier(), resultEquation, rules, marker)); return null; } } diff --git a/meta/src/main/java/org/arend/lib/util/Utils.java b/meta/src/main/java/org/arend/lib/util/Utils.java index 60edeede..03936212 100644 --- a/meta/src/main/java/org/arend/lib/util/Utils.java +++ b/meta/src/main/java/org/arend/lib/util/Utils.java @@ -481,4 +481,9 @@ public static ArendRef getReference(ConcreteExpression expr, ErrorReporter error errorReporter.report(new TypecheckingError("Expected a reference", expr)); return null; } + + public static CoreExpression getClassifyingExpression(CoreClassCallExpression classCall, TypedExpression thisExpr) { + CoreClassField field = classCall.getDefinition().getClassifyingField(); + return field == null ? null : classCall.getImplementation(field, thisExpr); + } } diff --git a/src/Algebra/Field.ard b/src/Algebra/Field.ard index e4daecdb..02f26eda 100644 --- a/src/Algebra/Field.ard +++ b/src/Algebra/Field.ard @@ -130,6 +130,9 @@ \lemma decideZeroOrInv (x : E) : (x = 0) `Or` Inv x => aux zro/=ide x (eitherZeroOrInv x) + + \lemma finv-diff {x : E} (xi : x /= 0) (x+1i : x + 1 /= 0) : finv x - finv (x + 1) = finv (x * (x + 1)) + => equation {usingOnly (finv-right xi, finv-right x+1i, finv-right $ nonZero_* xi x+1i)} } \where { \private \lemma aux {R : CRing} (p : zro /= {R} ide) (x : R) (q : (x = 0) || Inv x) : (x = 0) `Or` Inv x \level Or.levelProp (\lam x=0 (j : Inv x) => p $ inv zro_*-left *> pmap (`* _) (inv x=0) *> j.inv-right) diff --git a/src/Algebra/Field/Algebraic.ard b/src/Algebra/Field/Algebraic.ard index 4e085e49..5be59a3b 100644 --- a/src/Algebra/Field/Algebraic.ard +++ b/src/Algebra/Field/Algebraic.ard @@ -6,6 +6,7 @@ \import Algebra.Monoid \import Algebra.Monoid.Category \import Algebra.Monoid.PermSet +\import Algebra.Ordered \import Algebra.Pointed \import Algebra.Pointed.Category \import Algebra.Ring @@ -132,7 +133,7 @@ {d : Nat} (pd : \Pi (j : Fin pl.len) -> permSet-length (pl j) < d) (a : Array R n) (pl/=0 : pl.len /= 0) {p : MPoly (Fin n) R} (pp : p = BigSum \lam j => msMonomial (pc j) (pl j)) : ∃ (m : Nat) (degree<= (change-vars p d a) m) (Inv (polyCoef (change-vars p d a) m)) \elim pp | idp => - \let | pow>0 {n} : 0 < pow d n => NatSemiring.pow>0 $ zero<=_ <∘r pd (transport Fin (suc_pred pl/=0) 0) + \let | pow>0 {n} : 0 < pow d n => NatSemiring.pow>0 $ zero<=_ <-transitive-right pd (transport Fin (suc_pred pl/=0) 0) | (m,rd,ri) => poly-degrees {_} {\lam j => change-vars (msMonomial 1 (pl j)) d a} pc (\lam j => permSet-univ {_} {AbMonoid.toCMonoid NatSemiring} (later \lam i => pow d i) (pl j)) (\lam j => rewrite (change-vars_monomial {_} {_} {pl j}) $ permSet-univ_monic {_} {\lam j => padd pzero (a j) + pow (padd 1 0) (pow d j)} {\lam j => pow d j} diff --git a/src/Algebra/Group.ard b/src/Algebra/Group.ard index 6b6dd9eb..dda1673a 100644 --- a/src/Algebra/Group.ard +++ b/src/Algebra/Group.ard @@ -212,6 +212,12 @@ \lemma BigSum_negative {l : Array E} : negative (BigSum l) = BigSum (map negative l) \elim l | nil => negative_zro | a :: l => negative_+ *> +-comm *> pmap (_ +) BigSum_negative + + \lemma sum-cancel-left {x y z : E} : x + z - (x + y) = z - y + => pmap (_ +) negative_+ *> pmap2 (+) +-comm +-comm *> +-assoc *> pmap (z +) (inv +-assoc *> pmap (`- y) negative-right *> zro-left) + + \lemma diff-cancel-left {x y z : E} : x - z - (x - y) = y - z + => sum-cancel-left *> +-comm *> pmap (`- z) negative-isInv } \where { \use \coerce fromCGroup (G : CGroup) => \new AbGroup G.E G.ide (G.*) G.ide-left G.ide-right G.*-assoc G.inverse G.inverse-left G.*-comm \use \coerce toCGroup (G : AbGroup) => \new CGroup G.E G.zro (G.+) G.zro-left G.zro-right G.+-assoc G.negative G.negative-left G.+-comm diff --git a/src/Algebra/Ordered.ard b/src/Algebra/Ordered.ard index 3dc3b345..7f7e5acb 100644 --- a/src/Algebra/Ordered.ard +++ b/src/Algebra/Ordered.ard @@ -2,6 +2,7 @@ \import Algebra.Domain \import Algebra.Field \import Algebra.Group +\import Algebra.Meta \import Algebra.Monoid \import Algebra.Ring \import Algebra.Semiring @@ -17,7 +18,7 @@ \import Order.StrictOrder \import Paths \import Paths.Meta - +\import Set \open Monoid(Inv) \class OrderedAddMonoid \extends StrictPoset, AddMonoid { @@ -181,6 +182,14 @@ \lemma negative_<= {x y : E} (x<=y : x <= y) : negative y <= negative x => \lam -x<-y => x<=y $ repeat {2} (rewrite negative-isInv in) (negative_< -x<-y) + \lemma meet_negative {x y : E} : negative (x ∧ y) = negative x ∨ negative y + => <=-antisymmetric (\lam p => <-irreflexive $ join-right <∘r (rewrite (LinearOrder.meet/=left $ <_/= $ negative_<-inv $ join-left <∘r p) in p)) $ + join-univ (negative_<= meet-left) (negative_<= meet-right) + + \lemma join_negative {x y : E} : negative (x ∨ y) = negative x ∧ negative y + => <=-antisymmetric (meet-univ (negative_<= join-left) (negative_<= join-right)) \lam p => + <-irreflexive $ (rewrite (LinearOrder.join/=left $ <_/= $ negative_<-inv $ p <∘l meet-left) in p) <∘l meet-right + \func abs (x : E) => x ∨ negative x \lemma abs>=id {x : E} : x <= abs x @@ -207,11 +216,14 @@ \lemma abs_+ {x y : E} : abs (x + y) <= abs x + abs y => join-univ (<=_+ join-left join-left) $ rewrite (negative_+,+-comm) $ <=_+ join-right join-right - \lemma abs_- {x y : E} : abs x - abs y <= abs (x - y) + \lemma abs_- {x y : E} : abs (x - y) = abs (y - x) + => pmap abs (inv negative-isInv) *> abs_negative *> simplify + + \lemma abs_-left {x y : E} : abs x - abs y <= abs (x - y) => transport (_ <=) (+-assoc *> pmap (_ +) negative-right *> zro-right) $ <=_+ (transport (abs __ <= _) (+-assoc *> pmap (x +) negative-left *> zro-right) abs_+) <=-refl - \lemma abs_-' {x y : E} : abs y - abs x <= abs (x - y) - => transport (_ <=) (simplify *> abs_negative) abs_- + \lemma abs_-right {x y : E} : abs y - abs x <= abs (x - y) + => transport (_ <=) abs_- abs_-left \lemma abs_zro : abs zro = zro => <=-antisymmetric (join-univ <=-refl $ rewrite negative_zro <=-refl) abs>=0 @@ -219,6 +231,9 @@ \lemma abs_zro-ext {x : E} (p : abs x = zro) : x = zro => <=-antisymmetric (transport (_ <=) p join-left) $ transport2 (<=) negative_zro negative-isInv $ negative_<= $ transport (_ <=) p join-right + \lemma abs>=_- {x y : E} : y - x <= abs (x - y) + => transportInv (_ <=) negative_+ (later $ rewrite negative-isInv <=-refl) <=∘ abs>=neg + \lemma abs_-_< {x y z : E} (p : x - y < z) (q : y - x < z) : abs (x - y) < z => LinearOrder.<_join-univ p (simplify q) } @@ -246,6 +261,15 @@ \lemma <_*_negative_positive {x y : E} (x<0 : x < 0) (y>0 : 0 < y) : x * y < 0 => transport (_ <) zro_*-left (<_*_positive-left x<0 y>0) + + \lemma pow>0 {a : E} (p : 0 < a) {k : Nat} : 0 < pow a k \elim k + | 0 => zro <_*_positive_positive (pow>0 p) p + + \lemma pow0 : 0 < a) (a<1 : a < 1) {k : Nat} (k>1 : 1 NatSemiring.< k) : pow a k < a \elim k, k>1 + | 1, NatSemiring.suc transport2 (__ * a < __) (inv ide-left) ide-right $ <_*_positive-right a>0 a<1 + | suc (suc (suc k)), _ => transport (_ <) ide-right (<_*_positive-right (pow>0 a>0 {suc (suc k)}) a<1) <∘ pow0 a<1 {suc (suc k)} (NatSemiring.suc <_*_negative_negative p p }) - \lemma inv-positive (t : Inv {\this}) (p : t > 0) : t.inv > 0 + \lemma >0_Inv (t : Inv {\this}) (p : t > 0) : t.inv > 0 => \case <_*-cancel-left (transport2 (<) (inv zro_*-right) (inv t.inv-right) zro q.2 | byRight q => absurd (<-irreflexive (p <∘ q.1)) } + \lemma <0_Inv (t : Inv {\this}) (p : t < 0) : t.inv < 0 + => \case <_*-cancel-left (transport2 (<) (inv zro_*-right) (inv t.inv-right) zro absurd (<-irreflexive (p <∘ q.1)) + | byRight q => q.2 + } + + \lemma >=0_Inv (t : Inv {\this}) (p : 0 <= t) : 0 <= t.inv + => \lam q => p (<0_Inv t.op q) + + \lemma <=0_Inv (t : Inv {\this}) (p : t <= 0) : t.inv <= 0 + => \lam q => p (>0_Inv t.op q) + + \lemma <=_Inv-cancel-left {x y z : E} (xi : Inv x) (x>=0 : 0 <= x) (p : x * y <= x * z) : y <= z + => transport2 (<=) (inv *-assoc *> pmap (`* y) xi.inv-left *> ide-left) (inv *-assoc *> pmap (`* z) xi.inv-left *> ide-left) $ <=_*_positive-right (>=0_Inv xi x>=0) p + + \lemma <=_Inv-cancel-right {x y z : E} (xi : Inv x) (p : y * x <= z * x) (x>=0 : 0 <= x) : y <= z + => transport2 (<=) (*-assoc *> pmap (y *) xi.inv-right *> ide-right) (*-assoc *> pmap (z *) xi.inv-right *> ide-right) $ <=_*_positive-left p (>=0_Inv xi x>=0) + \func mid_inv (t : Inv (1 + 1)) (a b : E) => (a + b) * t.inv \lemma mid_inv>left (t : Inv (1 + 1)) {a b : E} (p : a < b) : a < mid_inv t a b - => \have | t>0 : t.inv > 0 => inv-positive t $ zro \have | t>0 : t.inv > 0 => >0_Inv t $ zro rewrite (ldistr,ide-right) (<_+-right a p) \in transport (`< _) (*-assoc *> pmap (a *) t.inv-right *> ide-right) $ <_*_positive-left a20 \lemma mid_inv \have | t>0 : t.inv > 0 => inv-positive t $ zro \have | t>0 : t.inv > 0 => >0_Inv t $ zro rewrite (ldistr,ide-right) (<_+-left b p) \in transport (_ <) (*-assoc *> pmap (b *) t.inv-right *> ide-right) (<_*_positive-left a+b0) @@ -357,9 +399,25 @@ \lemma natCoef_<= {n m : Nat} (p : n NatSemiring.<= m) : natCoef n <= natCoef m => rewrite (inv (<=_exists p), natCoef_+) $ transport (`<= _) zro-right $ <=_+ <=-refl natCoef>=0 - \lemma pow>0 {a : E} {k : Nat} (p : 0 < a) : 0 < pow a k \elim k - | 0 => zro <_*_positive_positive (pow>0 p) p + \lemma pow>=0 {a : E} {k : Nat} (a>=0 : 0 <= a) : 0 <= pow a k \elim k + | 0 => <_<= zro <=_*_positive_positive (pow>=0 a>=0) a>=0 + + \lemma pow_<=-monotone {a b : E} {k : Nat} (a>=0 : 0 <= a) (a<=b : a <= b) : pow a k <= pow b k \elim k + | 0 => <=-refl + | suc k => <=_*_positive-right (pow>=0 a>=0) a<=b <=∘ <=_*_positive-left (pow_<=-monotone a>=0 a<=b) (a>=0 <=∘ a<=b) + + \lemma pow<=id {a : E} (a>=0 : 0 <= a) (a<=1 : a <= 1) {k : Nat} (k/=0 : k /= 0) : pow a k <= a \elim k + | 0 => \case k/=0 idp + | 1 => transportInv (`<= _) ide-left <=-refl + | suc (suc k) => transport (_ <=) ide-right $ <=_*_positive-right (pow>=0 {_} {a} {suc k} a>=0) a<=1 <=∘ <=_*_positive-left (pow<=id a>=0 a<=1 suc/=0) (a>=0 <=∘ a<=1) + + \lemma pow<=1 {a : E} (a>=0 : 0 <= a) (a<=1 : a <= 1) {k : Nat} : pow a k <= 1 \elim k + | 0 => <=-refl + | suc k => pow<=id a>=0 a<=1 {suc k} (\case __) <=∘ a<=1 + + \lemma pow_<=-degree {a : E} (a>=0 : 0 <= a) (a<=1 : a <= 1) {n k : Nat} (n<=k : n NatSemiring.<= k) : pow a k <= pow a n + => rewrite (inv (<=_exists n<=k), pow_+) $ transport (_ <=) ide-right $ <=_*_positive-right (pow>=0 a>=0) $ pow<=1 a>=0 a<=1 \lemma meet_*-left {a b c : E} (a>=0 : 0 <= a) : a * (b ∧ c) = (a * b) ∧ (a * c) => <=-antisymmetric (meet-univ (<=_*_positive-right a>=0 meet-left) (<=_*_positive-right a>=0 meet-right)) @@ -523,19 +581,31 @@ \default negative=>#0 \as negative=>#0Impl {x} : isNeg x -> #0 x => byRight \default #0=>eitherPosOrNeg \as #0=>eitherPosOrNegImpl {x} (x#0 : #0 x) => x#0 - \lemma positive_*-cancel-left {x y : E} (x*y>0 : isPos (x * y)) (y>0 : isPos y) : isPos x + \lemma pos#0 {x : E} (x>0 : 0 < x) : x AddGroup.`#0 + => positive=>#0 (>0_pos x>0) + + \lemma pos_*-cancel-left {x y : E} (x*y>0 : isPos (x * y)) (y>0 : isPos y) : isPos x => \case positive_*-cancel x*y>0 \with { | byLeft (x>0, _) => x>0 | byRight (_, -y>0) => absurd (zro/>0 (transport isPos negative-right (positive_+ y>0 -y>0))) } + \lemma positive_*-cancel-left {x y : E} (x*y>0 : 0 < x * y) (y>0 : 0 < y) : 0 < x + => pos_>0 $ pos_*-cancel-left (>0_pos x*y>0) (>0_pos y>0) + + \lemma positive_*-cancel-right {x y : E} (xy>0 : 0 < x * y) (x>0 : 0 < x) : 0 < y + => \case positive_*-cancel (>0_pos xy>0) \with { + | byLeft (_, y>0) => pos_>0 y>0 + | byRight (-x>0, _) => absurd (zro/>0 (transport isPos negative-right (positive_+ (>0_pos x>0) -x>0))) + } + \func denseOrder (t : Inv (1 + 1)) : UnboundedDenseLinearOrder \cowith | DenseLinearOrder => LinearlyOrderedSemiring.denseOrder t | withoutUpperBound x => inP (x + 1, transport (`< _) zro-right $ <_+-right x zro inP (x - 1, transport (_ <) zro-right $ <_+-right x (positive_negative zro transport2 (<) negative-isInv negative_zro $ negative_< $ inv-positive (negative_inv t) (rewrite negative_zro in negative_< p) + => transport2 (<) negative-isInv negative_zro $ negative_< $ >0_Inv (negative_inv t) (rewrite negative_zro in negative_< p) \lemma abs_* {x y : E} : abs (x * y) = abs x * abs y => \have | lem1 {x : E} : x * y <= abs x * abs y => \lam p => @@ -548,6 +618,13 @@ } \in <=-antisymmetric (join-univ lem1 $ rewriteI negative_*-left $ rewrite abs_negative in lem1 {negative x}) (rewrite (join_*-right abs>=0) $ join-univ lem2 $ transport (_ <=) (later $ rewrite negative_*-left abs_negative) lem2) + + \lemma abs_ide : abs 1 = 1 + => abs-ofPos (LinearOrder.<_<= zro abs_ide + | suc n => abs_* *> pmap (`* _) abs_pow } \where { \class Dec \extends Domain.Dec, OrderedRing, LinearlyOrderedSemiring.Dec { \field +_trichotomy (x : E) : Tri x zro @@ -588,18 +665,6 @@ | equals x=0 => absurd (transport (`/= zro) x=0 x#0 idp) | greater x>0 => byLeft (>0_pos x>0) } - - \lemma join_negative {x y : E} : negative x ∨ negative y = negative (x ∧ y) - => \case totality x y \with { - | byLeft x<=y => rewrite (meet_<= x<=y) $ join-comm *> join_<= (negative_<= x<=y) - | byRight y<=x => rewrite (meet-comm *> meet_<= y<=x) $ join_<= (negative_<= y<=x) - } - - \lemma meet_negative {x y : E} : negative x ∧ negative y = negative (x ∨ y) - => \case totality x y \with { - | byLeft x<=y => rewrite (join_<= x<=y) $ meet-comm *> meet_<= (negative_<= x<=y) - | byRight y<=x => rewrite (join-comm *> join_<= y<=x) $ meet_<= (negative_<= y<=x) - } } } @@ -621,6 +686,46 @@ | byRight x<0, byRight y<0 => byRight (x<0, y<0) } | negative=>#0 x<0 => transport #0 negative-isInv (Ring.negative_inv (positive=>#0 x<0)) + + \func pos-inv {x : E} (x>0 : 0 < x) : E + => Inv.inv {pos#0 x>0} + + \lemma pos-inv-left {x : E} (x>0 : 0 < x) : pos-inv x>0 * x = 1 + => Inv.inv-left {pos#0 x>0} + + \lemma pos-inv-right {x : E} (x>0 : 0 < x) : x * pos-inv x>0 = 1 + => Inv.inv-right {pos#0 x>0} + + \lemma pos-inv_pos-inv {x : E} (x>0 : 0 < x) : pos-inv (pos-inv>0 x>0) = x + => inv $ Inv.inv-isUnique (Inv.op {pos#0 x>0}) (pos#0 $ pos-inv>0 x>0) idp + + \lemma pos-inv_< {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) (x0 < pos-inv x>0 + => pos-inv_<-conv (pos-inv>0 y>0) (pos-inv>0 x>0) $ transport2 (<) (inv $ pos-inv_pos-inv x>0) (inv $ pos-inv_pos-inv y>0) x0 : 0 < x) (y>0 : 0 < y) (p : pos-inv y>0 < pos-inv x>0) : x < y + => transport2 (<) (inv *-assoc *> pmap (`* x) (pos-inv-right y>0) *> ide-left) ide-right $ <_*_positive-right y>0 $ transport (_ <) (pos-inv-left x>0) (<_*_positive-left p x>0) + + \lemma pos-inv_<= {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) (x<=y : x <= y) : pos-inv y>0 <= pos-inv x>0 + => \lam q => x<=y (pos-inv_<-conv y>0 x>0 q) + + \lemma pos-inv_<=-conv {x y : E} (x>0 : 0 < x) (y>0 : 0 < y) (p : pos-inv y>0 <= pos-inv x>0) : x <= y + => \lam q => p (pos-inv_< y>0 x>0 q) + + \lemma pos-inv>0 {x : E} (x>0 : 0 < x) : 0 < pos-inv x>0 + => positive_*-cancel-right (transportInv (0 <) (pos-inv-right x>0) zro0 + + \lemma pos-inv>1 {x : E} (x>0 : 0 < x) (x<1 : x < 1) : 1 < pos-inv x>0 + => transport (`< _) pos-inv_ide $ pos-inv_< x>0 zro inv ide-left *> pos-inv-right zro0 : 0 < x) (y>0 : 0 < y) : pos-inv x>0 * pos-inv y>0 = pos-inv (<_*_positive_positive x>0 y>0) + => Inv.inv-isUnique (Inv.lmake _ $ *-assoc *> pmap (_ *) (inv *-assoc *> pmap (`* x) (pos-inv-left y>0) *> ide-left) *> pos-inv-left x>0) (pos#0 $ <_*_positive_positive x>0 y>0) *-comm + + \lemma pos-inv_pow {x : E} (x>0 : 0 < x) {n : Nat} : pow (pos-inv x>0) n = pos-inv (pow>0 x>0 {n}) \elim n + | 0 => inv pos-inv_ide + | suc n => pmap (`* _) (pos-inv_pow x>0) *> pos-inv_* (pow>0 x>0) x>0 } \class DiscreteOrderedField \extends OrderedCRing.Dec, OrderedField, DiscreteField { @@ -637,7 +742,7 @@ } \lemma finv>0 {x : E} (x>0 : 0 < x) : 0 < finv x - => inv-positive (nonZero-Inv (>_/= x>0)) x>0 + => >0_Inv (nonZero-Inv (>_/= x>0)) x>0 \lemma finv<0 {x : E} (x<0 : x < 0) : finv x < 0 => inv-negative (nonZero-Inv (<_/= x<0)) x<0 @@ -652,6 +757,9 @@ \lemma finv_< {x y : E} (x>0 : 0 < x) (x rewrite (finv-right $ >_/= x>0, ide-right, inv *-assoc, finv-left $ >_/= $ x>0 <∘ x0 $ x>0 <∘ x0 x>0)) + \lemma finv_<-conv {x y : E} (x>0 : 0 < x) (p : finv x < finv y) : y < x + => transport2 (<) finv_finv finv_finv $ finv_< (finv>0 x>0) p + \lemma finv_<-left {x y : E} (x>0 : 0 < x) (p : finv x < y) : finv y < x => transport (_ <) finv_finv $ finv_< (finv>0 x>0) p @@ -663,6 +771,12 @@ \lemma <_rotate-left {x y z : E} (y>0 : 0 < y) (p : x < y * z) : finv y * x < z => transport (_ <) (inv *-assoc *> pmap (`* z) (finv-left (>_/= y>0)) *> ide-left) (<_*_positive-right (finv>0 y>0) p) + + \lemma finv_<= {x y : E} (x>0 : 0 < x) (x<=y : x <= y) : finv y <= finv x + => \lam p => x<=y (finv_<-conv x>0 p) + + \lemma finv>0-diff {x : E} (x>0 : 0 < x) : finv x - finv (x + 1) = finv (x * (x + 1)) + => finv-diff (\lam x=0 => linarith) (\lam x+1=0 => linarith) } \class OrderedAAlgebra \extends AAlgebra, OrderedRing { diff --git a/src/Algebra/Ring.ard b/src/Algebra/Ring.ard index 063c5caa..f38066c7 100644 --- a/src/Algebra/Ring.ard +++ b/src/Algebra/Ring.ard @@ -75,6 +75,13 @@ | inv-right => negative_* *> j.inv-right } + \lemma geometric-partial-sum {n : Nat} {x : E} (xi : Monoid.Inv (1 - x)) : xi.inv - BigSum (\new Array E n (\lam j => Monoid.pow x j)) = Monoid.pow x n * xi.inv + => inv (rdistr_- *> pmap2 (-) ide-left (*-assoc *> pmap (_ *) xi.inv-right *> ide-right)) *> pmap (`* _) (pmap (1 -) ldistr_- *> simplify \case \elim n \with { + | 0 => simplify + | suc n => rewrite {1} (BigSum_suc,rdistr) $ simplify $ pmap (`+ _) +-comm *> +-assoc *> + pmap2 (+) (later rewrite (toFin'=id id negative-right) *> zro-right + }) + \func IsNilpotent (x : E) => ∃ (n : Nat) (pow x n = 0) \lemma pow_-1_+2 {n : Nat} : pow -1 (n Nat.+ 2) = pow -1 n diff --git a/src/Algebra/Ring/Local.ard b/src/Algebra/Ring/Local.ard index 030c3f83..554a7aea 100644 --- a/src/Algebra/Ring/Local.ard +++ b/src/Algebra/Ring/Local.ard @@ -1,9 +1,11 @@ +\import Algebra.Group \import Algebra.Monoid \import Algebra.Ring \import Algebra.Semiring \import Function.Meta \import Logic \import Logic.Meta +\import Meta \import Paths \import Paths.Meta \open Monoid(Inv,LInv) @@ -11,6 +13,12 @@ \class LocalRing \extends Ring, NonZeroRing { | locality (x : E) : Inv x || Inv (x + ide) + \lemma locality_- (x : E) : Inv x || Inv (ide - x) + => \case locality (negative x) \with { + | byLeft p => byLeft $ transport Inv negative-isInv (Ring.negative_inv p) + | byRight p => byRight $ transport Inv +-comm p + } + \lemma sum1=>eitherInv {x y : E} (x+y=1 : x + y = ide) : Inv x || Inv y => \case locality (negative x) \with { | byLeft -x_inv => byLeft (rewriteI negative-isInv (Ring.negative_inv -x_inv)) | byRight [-x+1]_inv => byRight (rewriteEq (pmap (negative x +) x+y=1) [-x+1]_inv) diff --git a/src/Algebra/Ring/Localization/Field.ard b/src/Algebra/Ring/Localization/Field.ard index b1d654b0..f655b46e 100644 --- a/src/Algebra/Ring/Localization/Field.ard +++ b/src/Algebra/Ring/Localization/Field.ard @@ -82,7 +82,7 @@ | zro/>0 => zro/>0 | positive_+ {in~ x} {in~ y} x>0 y>0 => positive_+ (positive_* x>0 y.3) (positive_* y>0 x.3) | ide>zro => ide>zro - | <_+-comparison (in~ x) (in~ y) x+y>0 => ||.map (OrderedRing.positive_*-cancel-left __ y.3) (OrderedRing.positive_*-cancel-left __ x.3) (<_+-comparison _ _ x+y>0) + | <_+-comparison (in~ x) (in~ y) x+y>0 => ||.map (OrderedRing.pos_*-cancel-left __ y.3) (OrderedRing.pos_*-cancel-left __ x.3) (<_+-comparison _ _ x+y>0) | <_+-connectedness {in~ x} x/>0 -x/>0 => localization-zro (positiveSubset R) x ide ide>zro (ide-right *> <_+-connectedness x/>0 -x/>0) | positive_* {in~ x} {in~ y} => positive_* {_} {x.1} {y.1} | positive=>#0 {in~ x} x>0 => localization-inv (positiveSubset R) x ide (simplify x>0) @@ -152,8 +152,8 @@ \func isPositive {R : OrderedCRing} (x : Type {R} {positiveSubset R}) : \Prop \elim x | in~ x => isPos x.1 | ~-equiv x y x~y => propExt - (\lam x>0 => OrderedRing.positive_*-cancel-left (transport isPos x~y (positive_* x>0 y.3)) x.3) - (\lam y>0 => OrderedRing.positive_*-cancel-left (transport isPos (inv x~y) (positive_* y>0 x.3)) y.3) + (\lam x>0 => OrderedRing.pos_*-cancel-left (transport isPos x~y (positive_* x>0 y.3)) x.3) + (\lam y>0 => OrderedRing.pos_*-cancel-left (transport isPos (inv x~y) (positive_* y>0 x.3)) y.3) } -- | The localization of a decidable ordered commutative ring at the set of positive elements is a discrete ordered field. diff --git a/src/Analysis/FuncLimit.ard b/src/Analysis/FuncLimit.ard new file mode 100644 index 00000000..343d338b --- /dev/null +++ b/src/Analysis/FuncLimit.ard @@ -0,0 +1,127 @@ +\import Algebra.Group +\import Analysis.Limit +\import Arith.Real +\import Function.Meta +\import Logic +\import Logic.Meta +\import Meta +\import Operations +\import Order.Directed +\import Order.PartialOrder +\import Order.StrictOrder +\import Paths +\import Paths.Meta +\import Set.Subset +\import Topology.CoverSpace +\import Topology.CoverSpace.Complete +\import Topology.CoverSpace.Directed +\import Topology.CoverSpace.Product +\import Topology.MetricSpace +\import Topology.TopAbGroup +\import Topology.TopSpace +\import Topology.UniformSpace +\open ProductCoverSpace +\open CoverMap + +\func IsFuncConvergent {I : DirectedSet} {X Y : CoverSpace} (f : I -> X -> Y) : \Prop + => CoverMap (DirectedCoverSpace I ⨯ X) Y \lam s => f s.1 s.2 + +\lemma funcConv-pointwise {I : DirectedSet} {X Y : CoverSpace} (f : I -> X -> Y) (fc : IsFuncConvergent f) {x : X} : IsConvergent (f __ x) + => fc ∘ tuple id (const x) + +\lemma funcLimit {I : DirectedSet} {X : CoverSpace} {Y : CompleteCoverSpace} (f : I -> X -> Y) (fc : IsFuncConvergent f) + : CoverMap X Y \lam x => limit (f __ x) (funcConv-pointwise f fc) + => \have | de => prod.isDenseEmbedding completion.isDenseEmbedding id-denseEmbedding + | lift => dense-lift (prod completion id) de fc + \in transport (CoverMap X Y) (ext \lam x => dense-lift-unique completion completion.isDenseEmbedding.1 (lift ∘ tuple id (const x)) (completion-lift $ funcConv-pointwise f fc) (\lam n => dense-lift-char de {fc} (n,x) *> inv (completion-lift-char {_} {_} {funcConv-pointwise f fc} n)) limit.infPoint) $ lift ∘ tuple (const limit.infPoint) id + +\lemma funcConvergent-char {I : DirectedSet} {X Y : CoverSpace} (f : I -> CoverMap X Y) + (fc : ∀ {D : Y.isCauchy} (X.isCauchy \lam U => ∃ (N : I) (V : D) ∀ {n} {x} (N <= n -> U x -> V (f n x)))) + : IsFuncConvergent (\lam n => f n) + => regPrecoverSpace-extend-coverMap {DirectedCoverSpace.precover ⨯ X} \new PrecoverMap { + | func s => f s.1 s.2 + | func-cover Dc => directedProdCover-char.2 + (cauchy-subset (fc Dc) \lam (inP (N,V,DV,h)) => inP $ later (N, _, inP (V, DV, idp), h), + \lam n => cauchy-subset (func-cover {f n} Dc) \lam {_} (inP (V,DV,idp)) => inP $ later (_, inP (V, DV, idp), \lam s => s)) + } + \where { + \protected \lemma conv {I : DirectedSet} {X Y : CoverSpace} (f : I -> CoverMap X Y) (fc : IsFuncConvergent (\lam n => f n)) + : ∀ {D : Y.isCauchy} (X.isCauchy \lam U => ∃ (N : I) (V : D) ∀ {n} {x} (N <= n -> U x -> V (f n x))) + => \lam Dc => cauchy-subset (directedProdCover-char.1 $ func-cover {tuple.precover (regPrecoverSpace PrecoverMap.∘ ProductPrecoverSpace.proj1) ProductPrecoverSpace.proj2} $ fc.func-cover Dc).1 + \lam (inP (N, _, inP (_, inP (V,DV,idp), idp), h)) => inP $ later (N, V, DV, h) + } + +\lemma funcConvergent-uniform-char {I : DirectedSet} {X : CoverSpace} {Y : UniformSpace} (f : I -> CoverMap X Y) + (fc : ∀ {E : Y.isUniform} (X.isCauchy \lam U => ∃ (N : I) ∀ {x : U} ∃ (W : E) ∀ {n} (N <= n -> W (f n x)))) + : IsFuncConvergent (\lam n => f n) + => split f \lam Eu => \case uniform-star Eu \with { + | inP (E',E'u,E' inP (_, fc E'u , \lam (inP (N,h)) => inP (N, _, func-cover {f N} $ Y.makeCauchy E'u, \lam {_} (inP (W',E'W',idp)) => \case E' inP (W, EW, \lam N<=n {x} Ux (W'fNx) => \case h Ux \with { + | inP (W'',E'W'',c) => g E'W'' (f N x, (W'fNx, c <=-refl)) (c N<=n) + }) + })) + } + \where { + \protected \lemma split {I : DirectedSet} {X : CoverSpace} {Y : UniformSpace} (f : I -> CoverMap X Y) + (fc : ∀ {E : Y.isUniform} ∃ (C : X.isCauchy) ∀ {U : C} ∃ (N : I) (D : X.isCauchy) + ∀ {V : D} ∃ (W : E) ∀ {n} (N <= n) ∀ {x} (U x -> V x -> W (f n x))) + : IsFuncConvergent (\lam n => f n) + => regPrecoverSpace-extend-coverMap {DirectedCoverSpace.precover ⨯ X} \new PrecoverMap { + | func s => f s.1 s.2 + | func-cover Dc => ClosurePrecoverSpace.closure-univ-cover {_} {_} {DirectedCoverSpace.precover ⨯ X} (\lam {E} Eu => \case fc Eu \with { + | inP (C,Cc,h) => directedProdCover-char.2 + (cauchy-subset (cauchy-glue Cc {\lam U V => ∃ (N : I) (W : E) ∀ {n} (N <= n) ∀ {x} (U x -> V x -> W (f n x))} \lam CU => \case h CU \with { + | inP (N,D,Dc,Dg) => cauchy-subset Dc \lam {V} DV => \case Dg DV \with { + | inP (W,EW,Eg) => inP $ later (N,W,EW,Eg) + } + }) \lam {_} (inP (U, V, CU, inP (N,W,EW,g), idp)) => inP $ later (N, _, inP (W, EW, idp), \lam p (Ux,Vx) => g p Ux Vx), + \lam n => cauchy-subset (func-cover {f n} $ Y.makeCauchy Eu) \lam {_} (inP (V,DV,idp)) => inP $ later (_, inP (V, DV, idp), \lam s => s)) + }) (uniform-cauchy.1 Dc) + } + + \protected \lemma conv {I : DirectedSet} {X : CoverSpace} {Y : UniformSpace} (f : I -> CoverMap X Y) (fc : IsFuncConvergent \lam n => f n) + : ∀ {E : Y.isUniform} (X.isCauchy \lam U => ∃ (N : I) ∀ {x : U} ∃ (W : E) ∀ {n} (N <= n -> W (f n x))) + => \lam Eu => cauchy-subset (funcConvergent-char.conv f fc $ Y.makeCauchy Eu) \lam (inP (N,V,EV,h)) => inP $ later (N, \lam Ux => inP (V, EV, h __ Ux)) + } + +\lemma funcCovergent-metric-char {I : DirectedSet} {X : CoverSpace} {Y : PseudoMetricSpace} (f : I -> CoverMap X Y) + (fc : \Pi {eps : Real} -> 0 < eps -> X.isCauchy \lam U => ∃ (N : I) ∀ {x : U} ∀ {n} (N <= n -> dist (f n x) (f N x) < eps)) + : IsFuncConvergent (\lam n => f n) + => funcConvergent-uniform-char f \lam Eu => \case dist-uniform.1 Eu \with { + | inP (eps,eps>0,h) => cauchy-subset (fc eps>0) \lam (inP (N,g)) => inP $ later (N, \lam {x} Ux => \case h (f N x) \with { + | inP (U,EU,dU) => inP (U, EU, \lam p => dU $ rewrite dist-symm $ g Ux p) + }) + } + \where { + \protected \lemma conv {I : DirectedSet} {X : CoverSpace} {Y : PseudoMetricSpace} (f : I -> CoverMap X Y) (fc : IsFuncConvergent (\lam n => f n)) + : \Pi {eps : Real} -> 0 < eps -> X.isCauchy \lam U => ∃ (N : I) ∀ {x : U} ∀ {n} (N <= n -> dist (f n x) (f N x) < eps) + => \lam eps>0 => cauchy-subset (funcConvergent-uniform-char.conv f fc $ Y.makeUniform $ RealAbGroup.half>0 eps>0) \lam (inP (N,g)) => inP $ later (N, \lam Ux p => \case g Ux \with { + | inP (_, inP (y,idp), h) => Y.halving (h p) (h <=-refl) + }) + } + +\lemma funcCovergent-topAb-char {I : DirectedSet} {X : CoverSpace} {Y : TopAbGroup} (f : I -> CoverMap X Y) + (fc : ∀ {U : Y.isOpen} (U 0) (X.isCauchy \lam V => ∃ (N : I) ∀ {x : V} ∀ {n} (N <= n -> U (f n x - f N x)))) + : IsFuncConvergent (\lam n => f n) + => funcConvergent-uniform-char f \lam Eu => \case neighborhood-uniform.1 Eu \with { + | inP (U,Uo,U0,h) => cauchy-subset (fc (negative-cont.func-cont Uo) $ simplify U0) \lam {V} (inP (N,g)) => inP $ later (N, \lam {x} Vx => \case h (f N x) \with { + | inP (W,EW,dW) => inP (W, EW, \lam p => dW $ simplify in g Vx p) + }) + } + \where { + \protected \lemma conv {I : DirectedSet} {X : CoverSpace} {Y : TopAbGroup} (f : I -> CoverMap X Y) (fc : IsFuncConvergent (\lam n => f n)) + : ∀ {U : Y.isOpen} (U 0) (X.isCauchy \lam V => ∃ (N : I) ∀ {x : V} ∀ {n} (N <= n -> U (f n x - f N x))) + => \lam {U} Uo U0 => \case Y.shrink Uo U0 \with { + | inP (U',U'o,U'0,h) => cauchy-subset (funcConvergent-uniform-char.conv f fc $ Y.makeUniform U'o U'0) \lam {V} (inP (N,g)) => inP $ later (N, \lam Vx p => \case g Vx \with { + | inP (_, inP (y,idp), dW) => transport U Y.diff-cancel-left $ h (dW <=-refl) (dW p) + }) + } + } + +\func IsUniFuncConvergent {I : DirectedSet} {X : \Set} {Y : UniformSpace} (f : I -> X -> Y) : \Prop + => ∀ {D : Y.isUniform} ∃ (N : I) ∀ x ∃ (V : D) ∀ {n} (N <= n -> V (f n x)) + +\lemma funcCovergent-uni {I : DirectedSet} {X : CoverSpace} {Y : UniformSpace} (f : I -> CoverMap X Y) (fc : IsUniFuncConvergent \lam n => f n) : IsFuncConvergent \lam n => f n + => funcConvergent-uniform-char f \lam Eu => top-cauchy \case fc Eu \with { + | inP (N,h) => inP $ later (N, \lam {x} _ => h x) + } \ No newline at end of file diff --git a/src/Analysis/Limit.ard b/src/Analysis/Limit.ard new file mode 100644 index 00000000..0364aa26 --- /dev/null +++ b/src/Analysis/Limit.ard @@ -0,0 +1,150 @@ +\import Algebra.Group +\import Algebra.Meta +\import Algebra.Ordered +\import Arith.Rat +\import Arith.Real +\import Arith.Real.Field +\import Function.Meta +\import Logic +\import Logic.Meta +\import Meta +\import Order.Directed +\import Order.LinearOrder +\import Order.PartialOrder +\import Order.StrictOrder +\import Paths +\import Paths.Meta +\import Set.Filter +\import Set.Partial +\import Topology.CoverSpace +\import Topology.CoverSpace.Complete +\import Topology.CoverSpace.Directed +\import Topology.MetricSpace +\import Topology.NormedAbGroup +\import Topology.NormedAbGroup.Real +\import Topology.TopAbGroup +\import Topology.TopSpace +\import Topology.UniformSpace + +\func IsConvergent {I : DirectedSet} {X : CoverSpace} (f : I -> X) : \Prop + => CoverMap (DirectedCoverSpace I) X f + +\lemma convergent-char {I : DirectedSet} {X : CoverSpace} {f : I -> X} (p : ∀ {C : X.isCauchy} ∃ (U : C) (N : I) ∀ {n} (N <= n -> U (f n))) : IsConvergent f + => regPrecoverSpace-extend-coverMap \new PrecoverMap { + | func => f + | func-cover Dc => \case p Dc \with { + | inP (U,DU,N,g) => later (inP (_, inP (U, DU, idp), N, g), \lam n => \case cauchy-cover Dc (f n) \with { + | inP (V,DV,Vfn) => inP (_, inP (V, DV, idp), Vfn) + }) + } + } + \where + \protected \lemma conv {I : DirectedSet} {X : CoverSpace} {f : I -> X} (fc : IsConvergent f) : ∀ {C : X.isCauchy} ∃ (U : C) (N : I) ∀ {n} (N <= n -> U (f n)) + => \lam Cc => \case (func-cover {regPrecoverSpace} $ func-cover {fc} Cc).1 \with { + | inP (_, inP (_, inP (U, CU, idp), idp), N, g) => inP (U, CU, N, g) + } + +\lemma limit-conv {I : DirectedSet} {X : CoverSpace} {f : I -> X} {l : X} (fl : X.IsLimit f l) : IsConvergent f + => convergent-char \lam Cc => \case X.cauchy-regular-cover Cc l \with { + | inP (U,CU,l<= \case fl (X.interior {U}) l<= inP (U, CU, N, \lam p => <=<_<= (g p) idp) + } + } + +\func limit {I : DirectedSet} {X : CompleteCoverSpace} (f : I -> X) : Partial X \cowith + | isDefined => IsConvergent f + | value fc => completion-lift fc infPoint + \where { + \func infPoint {I : DirectedSet} : Completion (DirectedCoverSpace I) + => CompleteCoverSpace.filter-point $ completion.func-cauchy EventualityFilter + + \protected \lemma char (fc : CoverMap (DirectedCoverSpace I) X) + : limit fc fc = CompleteCoverSpace.filter-point (fc.func-cauchy EventualityFilter) + => completion-lift-natural EventualityFilter + } + +\lemma limit-isLimit {I : DirectedSet} {X : CompleteCoverSpace} (fc : CoverMap (DirectedCoverSpace I) X) : X.IsLimit fc (limit fc fc) + => rewrite limit.char \lam Uo Ul => CompleteCoverSpace.filter-point-sub (X.open-char.1 Uo Ul) + +\lemma limit-char {I : DirectedSet} {X : CompleteCoverSpace} {f : I -> X} {l : X} : (limit f = defined l) <-> X.IsLimit f l + => (\lam p => rewriteI (defined-ext.value {_} {limit f} p) $ limit-isLimit (defined-ext.isDefined {_} {limit f} p), + \lam fl => defined-ext {_} {limit f} (limit-conv fl) $ inv $ isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char 4 7 \lam {U} l<= \case <=<-inter l<= \case fl X.interior l<= transportInv U (limit.char (limit-conv fl)) $ <=<_<= (CompleteCoverSpace.filter-point-elem U'<= <=<_<= (g p) idp)) idp + } + }) + +\lemma convergent-uniform-char {I : DirectedSet} {X : UniformSpace} {f : I -> X} (p : ∀ {C : X.isUniform} ∃ (U : C) (N : I) ∀ {n} (N <= n -> U (f n))) : IsConvergent f + => convergent-char \lam Cc => \case ClosurePrecoverSpace.closure-filter (\new SetFilter X { + | F U => ∃ (N : I) ∀ {n} (N <= n -> U (f n)) + | filter-mono p (inP (N,g)) => inP (N, \lam q => p (g q)) + | filter-top => \case I.isInhabitted \with { + | inP N => inP (N, \lam _ => ()) + } + | filter-meet (inP (N,g)) (inP (M,h)) => \case isDirected N M \with { + | inP (L,N<=L,M<=L) => inP (L, \lam L<=n => (g $ N<=L <=∘ L<=n, h $ M<=L <=∘ L<=n)) + } + }) (\lam Cu => \case p Cu \with { + | inP (U,CU,N,g) => inP (U, CU, inP (N,g)) + }) (uniform-cauchy.1 Cc) \with { + | inP (U, CU, inP (N,g)) => inP (U, CU, N, g) + } + \where + \protected \lemma conv {I : DirectedSet} {X : UniformSpace} {f : I -> X} (fc : IsConvergent f) : ∀ {C : X.isUniform} ∃ (U : C) (N : I) ∀ {n} (N <= n -> U (f n)) + => \lam Cu => convergent-char.conv fc (X.makeCauchy Cu) + +\lemma convergent-topAbGruop-char {I : DirectedSet} {X : TopAbGroup} {f : I -> X} : TFAE ( + IsConvergent f, + ∀ {U : X.isOpen} (U 0) ∃ (N : I) ∀ {n m} (N <= n -> n <= m -> U (f m - f n)), + ∀ {U : X.isOpen} (U 0) ∃ (N : I) ∀ {n} (N <= n -> U (f n - f N)) + ) => TFAE.cycle ( + \lam fc {U} Uo U0 => \case X.shrink Uo U0 \with { + | inP (V,Vo,V0,g) => \case convergent-uniform-char.conv fc $ X.makeUniform (negative-cont.func-cont Vo) (simplify V0) \with { + | inP (_, inP (x, idp), N, h) => inP (N, \lam p q => transport U simplify $ g (h $ p <=∘ q) (h p)) + } + }, + \lam fc Uo U0 => \case fc Uo U0 \with { + | inP (N,g) => inP (N, \lam p => g <=-refl p) + }, + \lam fc => convergent-uniform-char \lam Cu => \case neighborhood-uniform.1 Cu \with { + | inP (U,Uo,U0,h) => \case fc (negative-cont.func-cont Uo) (simplify U0) \with { + | inP (N,g) => \case h (f N) \with { + | inP (V,CV,UV) => inP (V, CV, N, \lam p => UV $ simplify in g p) + } + } + }) + +\lemma convergent-metric-char {I : DirectedSet} {X : PseudoMetricSpace} {f : I -> X} : TFAE ( + IsConvergent f, + ∀ {eps : Real} (0 < eps) ∃ (N : I) ∀ {n} (N <= n -> dist (f n) (f N) < eps), + ∀ {eps : Rat } (0 < eps) ∃ (N : I) ∀ {n} (N <= n -> dist (f n) (f N) < eps) + ) => TFAE.cycle ( + \lam fc eps>0 => \case convergent-uniform-char.conv fc $ X.makeUniform (RealAbGroup.half>0 eps>0) \with { + | inP (_, inP (x, idp), N, g) => inP (N, \lam p => X.halving (g p) (g <=-refl)) + }, + \lam fc eps>0 => fc $ real_<_L.2 eps>0, + \lam fc => convergent-uniform-char \lam Cu => \case X.dist-uniform-rat.1 Cu \with { + | inP (eps,eps>0,h) => \case fc eps>0 \with { + | inP (N,g) => \case h (f N) \with { + | inP (V,CV,dV) => inP (V, CV, N, \lam p => dV $ rewrite dist-symm $ g p) + } + } + } + ) + +\lemma limit-metric-char {I : DirectedSet} {X : PseudoMetricSpace} {f : I -> X} {l : X} + : X.IsLimit f l <-> ∀ {eps} (0 < eps) ∃ (N : I) ∀ {n} (N <= n -> dist l (f n) < eps) + => (\lam fl eps>0 => fl OBall-open (OBall-center eps>0), + \lam fl Uo U0 => \case dist_open.1 Uo U0 \with { + | inP (eps,eps>0,q) => \case fl eps>0 \with { + | inP (N,g) => inP (N, \lam p => q (g p)) + } + }) + +\lemma convergent-compose {I : DirectedSet} {X Y : CoverSpace} {f : I -> X} (fc : IsConvergent f) (g : CoverMap X Y) : IsConvergent \lam n => g (f n) + => g CoverMap.∘ fc + +\lemma limit-bound {I : DirectedSet} {f : I -> Real} {b : Real} (fb : \Pi (n : I) -> b <= f n) {l : Real} (fl : RealNormed.IsLimit f l) : b <= l + => \lam l \case fl (OBall-open {_} {b - l} {l}) (rewrite dist-refl linarith) \with { + | inP (N,g) => linarith $ LinearlyOrderedAbGroup.abs>=_- <∘r (rewrite norm-dist in g <=-refl) + } diff --git a/src/Analysis/PowerSeries.ard b/src/Analysis/PowerSeries.ard new file mode 100644 index 00000000..57b39dae --- /dev/null +++ b/src/Analysis/PowerSeries.ard @@ -0,0 +1,101 @@ +\import Algebra.Meta +\import Algebra.Monoid +\import Algebra.Ordered +\import Algebra.Ring +\import Analysis.FuncLimit +\import Analysis.Series +\import Arith.Nat +\import Arith.Rat +\import Arith.Real +\import Arith.Real.Field +\import Combinatorics.Factorial +\import Data.Or +\import Function.Meta +\import Logic +\import Logic.Meta +\import Meta +\import Order.LinearOrder +\import Order.PartialOrder +\import Order.StrictOrder +\import Paths +\import Paths.Meta +\import Set.Subset +\import Topology.CoverSpace.Complete +\import Topology.CoverSpace.Product +\import Topology.NormedAbGroup +\import Topology.NormedAbGroup.Real +\import Topology.NormedAbGroup.Real.Functions +\import Topology.NormedRing +\import Topology.TopSpace +\open Monoid(pow) +\open LinearlyOrderedSemiring + +\func powerSeries {X : PseudoNormedRing} (cs : Nat -> X) (n : Nat) (x : X) + => cs n * pow x n + +\lemma powerSeries_0 {X : PseudoNormedRing} {cs : Nat -> X} : IsConvSeries (powerSeries cs __ 0) + => series-shift-conv.2 $ transport IsConvSeries (ext \lam n => inv $ pmap (_ *) Ring.zro_*-right *> Ring.zro_*-right) (seriesSum-conv zeroSeries-sum) + +\func convRadius {X : PseudoNormedRing} (cs : Nat -> X) : LowerReal \cowith + | L a => ∃ (b : Real) (b.L a) (IsConvSeries \lam j => norm (cs j) * pow b j) + | L-inh => inP (-1, inP (0, idp, powerSeries_0)) + | L-closed (inP (b,q inP (b, L-closed q \case L-rounded a inP (a', inP (b, a' X) {x : Real} (x>=0 : 0 <= x) (p : x norm (cs j) * pow x j) \elim p + | inP (a, |x| series_<= (\lam j => <=_*_positive_positive norm>=0 (pow>=0 x>=0)) (\lam j => <=_*_positive-right norm>=0 (pow_<=-monotone x>=0 $ LinearOrder.<_<= $ real_<_U.2 |x| X) {x : X} (p : norm x series_<= (\lam j => norm>=0) (\lam j => norm_*_<= <=∘ later (<=_*_positive-right norm>=0 norm_<=_pow)) (convRadius-conv cs norm>=0 p) + +\lemma convRadius-div {X : PseudoValuedRing} (cs : Nat -> X) {x : X} (p : IsConvSeries (powerSeries cs __ x)) : norm x <=L convRadius cs + => \lam {a} a<|x| => \case LinearOrder.dec<_<= a 0, L-rounded a<|x| \with { + | inl a<0, _ => inP (0, a<0, powerSeries_0) + | inr a>=0, inP (b,b<|x|,a + \have |x|>0 => rat_real_<=.1 a>=0 <∘r real_<_L.2 a<|x| + \in inP (b, a norm (powerSeries cs j x) * pow (Real.fromRat b * RealField.pos-inv |x|>0) j} + (ext \lam j => pmap2 (*) norm_* CMonoid.pow_*-comm *> *-assoc *> pmap (_ *) (pmap (_ *) *-comm *> inv *-assoc *> pmap (`* _) (pmap (`* _) norm_pow *> inv CMonoid.pow_*-comm *> pmap (pow __ j) (RealField.pos-inv-right |x|>0) *> Monoid.pow_ide) *> ide-left)) $ + absConv-isConv $ series_*_lim (cont-limit (series-limit p) norm-metric) $ geometric-series-absConv $ later $ + rewrite (RealField.abs-ofPos $ <=_*_positive_positive (rat_real_<=.1 $ a>=0 <=∘ LinearOrder.<_<= a0 |x|>0) $ + rewrite OrderedField.pos-inv-right in <_*_positive-left (real_<_L.2 b<|x|) (OrderedField.pos-inv>0 |x|>0)) + } + +\type IsPowerSeriesConv {X : PseudoNormedRing} (cs : Nat -> X) : \Prop + => \Pi {a : Real} -> 0 <= a -> IsConvSeries (\lam n => norm (cs n) * pow a n) + +\lemma powerSeriesConv-absConv {X : PseudoNormedRing} {cs : Nat -> X} (p : IsPowerSeriesConv cs) {x : X} : IsAbsConvSeries (powerSeries cs __ x) + => series_<= {_} {\lam j => norm (cs j) * pow (norm x) j} (\lam j => norm>=0) (\lam j => norm_*_<= <=∘ <=_*_positive-right norm>=0 norm_<=_pow) (p norm>=0) + +\lemma powerSeriesConv-funcConv {X : PseudoNormedRing} {cs : Nat -> X} (p : IsPowerSeriesConv cs) + : IsFuncConvergent \lam n x => partialSum (powerSeries cs __ x) n + => funcCovergent-metric-char (partialSum-cover \lam j => *-locally-uniform CoverMap.∘ ProductCoverSpace.tuple (CoverMap.const (cs j)) (pow-cover j)) \lam {eps} eps>0 => + X.makeCauchy $ X.uniform-refine (X.makeUniform eps>0) \lam {_} (inP (x,idp)) => + \case MTest {\Sigma (y : X) (norm y < norm x + eps)} (\lam n s => powerSeries cs n s.1) (\lam n => norm (cs n) * pow (norm x + eps) n) + (\lam n s => norm_*_<= <=∘ <=_*_positive-right norm>=0 (norm_<=_pow <=∘ pow_<=-monotone norm>=0 (LinearOrder.<_<= s.2))) + (p $ linarith norm>=0) (X.makeUniform $ half>0 eps>0) \with { + | inP (N,h) => inP (_, inP $ later (N, \lam {y} d N<=n => \case h (y, linarith $ norm_-right <∘r (rewrite norm-dist in d)) \with { + | inP (_, inP (z,idp), g) => halving (g N<=n) (g <=-refl) + }), <=-refl) + } + +\lemma powerSeries-unbounded-conv {X : PseudoValuedRing} (Xu : X.IsUnbounded) {cs : Nat -> X} (Sc : \Pi (x : X) -> IsConvSeries (powerSeries cs __ x)) : IsPowerSeriesConv cs + => \lam {a} a>=0 => \case Real.natBounded {a} \with { + | inP (B,a \case Xu B \with { + | inP (x,B<|x|) => convRadius-conv cs a>=0 $ =0 : \Pi (j : Nat) -> 0 <= c j) (bp : \Pi (n : Nat) -> c (suc n) <= c n * b n) {l : Real} + (bl : RealNormed.IsLimit b l) {x : Real} (x>=0 : 0 <= x) (lx : l * x < 1) : IsConvSeries \lam j => c j * pow x j + => absConv-isConv $ ratio-test (\lam j => b j * x) (\lam j => later $ rewrite + (RealField.abs-ofPos $ <=_*_positive_positive (c>=0 (suc j)) (pow>=0 {_} {_} {suc j} x>=0), + RealField.abs-ofPos (<=_*_positive_positive (c>=0 j) (pow>=0 x>=0))) $ + <=_*_positive-left (bp j) (pow>=0 {_} {_} {suc j} x>=0) <=∘ Preorder.=_<= (equation {CRing})) lx $ + cont-limit bl $ RealField.*-cover CoverMap.∘ ProductCoverSpace.tuple CoverMap.id (CoverMap.const x) + +\lemma power-ratio-test-inf {X : PseudoNormedRing} (cs : Series X) (b : Series Real) + (bp : \Pi (n : Nat) -> norm (cs (suc n)) <= norm (cs n) * b n) (bl : RealNormed.IsLimit b 0) : IsPowerSeriesConv cs + => \lam a>=0 => power-ratio-test (\lam j => norm>=0) bp bl a>=0 $ rewrite Ring.zro_*-left zro Nat -> A + +\sfunc partialSum {A : AddMonoid} (S : Series A) (n : Nat) : A + => A.BigSum \new Array A n \lam j => S j + +\func IsConvSeries {A : TopAbGroup} (S : Series A) : \Prop + => IsConvergent (partialSum S) + +\func IsSeriesSum {A : TopAbGroup} (S : Series A) (l : A) : \Prop + => A.IsLimit (partialSum S) l + +\lemma seriesSum-conv {A : TopAbGroup} {S : Series A} {l : A} (Sl : IsSeriesSum S l) : IsConvSeries S + => limit-conv Sl + +\func seriesSum {A : CompleteTopAbGroup} (S : Series A) : Partial A + => limit (partialSum S) + +\lemma seriesConv-sum {A : CompleteTopAbGroup} {S : Series A} (Sc : IsConvSeries S) : IsSeriesSum S (seriesSum S Sc) + => limit-isLimit Sc + +\lemma seriesSum-char {A : CompleteTopAbGroup} {S : Series A} {l : A} : (seriesSum S = defined l) <-> IsSeriesSum S l + => limit-char + +\func IsAbsConvSeries {A : PseudoNormedAbGroup} (S : Series A) : \Prop + => IsConvSeries \lam j => norm (S j) + +\lemma zeroSeries-sum {A : TopAbGroup} : IsSeriesSum (\lam _ => A.zro) 0 + => \lam {U} _ U0 => inP (0, \lam _ => rewrite (\peval partialSum _ _) $ transportInv U A.BigSum_replicate0 U0) + +\lemma series-shift-conv {A : TopAbGroup} {S : Series A} : IsConvSeries S <-> IsConvSeries \lam n => S (suc n) + => (\lam Sc => convergent-topAbGruop-char 2 0 \lam {U} Uo U0 => \case convergent-topAbGruop-char 0 1 Sc Uo U0 \with { + | inP (N,g) => inP (N, \lam p => transport U (inv (midSum-diff $ suc<=suc p) *> midSum-diff p) $ g id<=suc $ suc<=suc p) + }, \lam Sc => convergent-topAbGruop-char 2 0 \lam {U} Uo U0 => \case convergent-topAbGruop-char 0 1 Sc Uo U0 \with { + | inP (N, g) => inP (suc N, \lam {n} => \case \elim n \with { + | 0 => \lam p => absurd $ p NatSemiring.zero \lam p => transport U (inv (midSum-diff $ suc<=suc.conv p) *> midSum-diff p) $ g <=-refl (suc<=suc.conv p) + }) + }) + +\lemma series-shifts-conv {A : TopAbGroup} {S : Series A} (N : Nat) : IsConvSeries S <-> IsConvSeries \lam n => S (n + N) \elim N + | 0 => <->refl + | suc N => <->trans (series-shifts-conv N) series-shift-conv + +\func midSum {A : AddMonoid} (S : Series A) (n m : Nat) : A \elim n, m + | 0, m => partialSum S m + | suc n, 0 => 0 + | suc n, suc m => midSum (\lam j => S (suc j)) n m + +\lemma midSum_suc {A : AddMonoid} {S : Series A} {n : Nat} : midSum S n (suc n) = S n \elim n + | 0 => (\peval partialSum _ _) *> zro-right + | suc n => midSum_suc + +\lemma midSum-diff {A : AbGroup} {S : Series A} {n m : Nat} (p : n <= m) : midSum S n m = partialSum S m - partialSum S n \elim n, m + | 0, m => inv $ rewrite (\peval partialSum S _, \peval partialSum S _) $ pmap (_ +) A.negative_zro *> zro-right + | suc n, 0 => absurd $ p NatSemiring.zero midSum-diff (suc<=suc.conv p) *> rewrite (\peval partialSum S _, \peval partialSum S _, \peval partialSum _ _, \peval partialSum _ _) (inv A.sum-cancel-left) + +\lemma midSum_norm {A : PseudoNormedAbGroup} {S : Series A} {n m : Nat} : norm (midSum S n m) <= midSum (\lam j => norm (S j)) n m \elim n, m + | 0, m => rewrite (\peval partialSum _ _, \peval partialSum _ _) A.norm_BigSum + | suc n, 0 => A.norm_BigSum {nil} + | suc n, suc m => midSum_norm + +\lemma midSum-ldistr {R : Ring} {x : R} {b : Series R} {n m : Nat} : x * midSum b n m = midSum (\lam j => x * b j) n m \elim n, m + | 0, m => rewrite (\peval partialSum _ _, \peval partialSum _ _) R.BigSum-ldistr + | suc n, 0 => zro_*-right + | suc n, suc m => midSum-ldistr + +\lemma midSum-split {A : AddMonoid} {b : Series A} {n m k : Nat} (p : n <= m) (q : m <= k) : midSum b n k = midSum b n m + midSum b m k \elim n, m, k + | 0, 0, k => rewrite (\peval partialSum _ _, \peval partialSum _ _) (inv zro-left) + | _, suc m, 0 => absurd (q NatSemiring.zero (\peval partialSum _ _) *> pmap (_ +) (inv \peval partialSum (\lam j => b (suc j)) _) *> pmap (_ +) (midSum-split zero<=_ $ suc<=suc.conv q) *> pmap (_ + (__ + _)) (\peval partialSum (\lam j => b (suc j)) _) *> inv +-assoc *> pmap (`+ _) (inv \peval partialSum _ _) + | suc n, 0, _ => absurd (p NatSemiring.zero midSum-split (suc<=suc.conv p) (suc<=suc.conv q) + +\lemma midSum_<= {A : LinearlyOrderedAbMonoid} {b c : Series A} {n m : Nat} (s : \Pi {j : Nat} -> n <= j -> j < m -> b j <= c j) : midSum b n m <= midSum c n m \elim n, m + | 0, m => rewrite (\peval partialSum _ _, \peval partialSum _ _) $ A.BigSum_<= \lam j => s zero<=_ (fin_< j) + | suc n, 0 => <=-refl + | suc n, suc m => midSum_<= \lam p q => s (suc<=suc p) (NatSemiring.suc A.zro) n m = 0 \elim n, m + | 0, m => (\peval partialSum _ _) *> A.BigSum_replicate0 + | suc n, 0 => idp + | suc n, suc m => midSum_0 + +\lemma midSum>=0 {A : LinearlyOrderedAbMonoid} {b : Series A} {n m : Nat} (s : \Pi (j : Nat) -> 0 <= b j) : 0 <= midSum b n m + => transport (`<= _) midSum_0 (midSum_<= \lam _ _ => s _) + +\lemma series-conv {A : PseudoNormedAbGroup} {S : Series A} + (p : ∀ {eps : Real} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> norm (midSum S N n) < eps)) + : IsConvSeries S + => convergent-metric-char 1 0 \lam eps>0 => \case p eps>0 \with { + | inP (N,g) => inP (N, \lam q => rewrite (norm-dist, inv (midSum-diff q)) (g q)) + } + \where { + \protected \lemma conv (p : IsConvSeries S) : ∀ {eps : Real} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> norm (midSum S N n) < eps) + => \lam eps>0 => \case convergent-metric-char 0 1 p eps>0 \with { + | inP (N,g) => inP (N, \lam q => rewrite (midSum-diff q, inv norm-dist) (g q)) + } + } + +\lemma seriesSum_defined {A : CompleteNormedAbGroup} {S : Series A} {a : A} + (p : ∀ {eps : Real} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> norm (a - partialSum S n) < eps)) + : seriesSum S = defined a + => seriesSum-char.2 \lam Uo Ua => \case dist_open.1 Uo Ua \with { + | inP (eps,eps>0,h) => \case p eps>0 \with { + | inP (N,g) => inP (N, \lam q => h $ rewriteI norm-dist in g q) + } + } + \where { + \lemma conv (p : seriesSum S = defined a) : ∀ {eps : Real} (0 < eps) ∃ (N : Nat) ∀ {n} (N <= n -> norm (a - partialSum S n) < eps) + => \lam eps>0 => \case seriesConv-sum (defined-ext.isDefined {_} {seriesSum S} p) OBall-open $ unfold OBall $ rewrite (defined-ext.value {_} {seriesSum S} p, dist-refl) eps>0 \with { + | inP (N,g) => inP (N, \lam q => rewriteI norm-dist (g q)) + } + } + +\lemma absConv-isConv {A : PseudoNormedAbGroup} {S : Series A} (Sc : IsAbsConvSeries S) : IsConvSeries S + => series-conv \lam eps>0 => \case series-conv.conv Sc eps>0 \with { + | inP (N,g) => inP (N, \lam p => midSum_norm <∘r RealAbGroup.abs>=id <∘r g p) + } + +\lemma series-limit {A : TopAbGroup} {S : Series A} (Sc : IsConvSeries S) : A.IsLimit S 0 + => \lam {U} Uo U0 => \case convergent-topAbGruop-char 0 1 Sc Uo U0 \with { + | inP (N,g) => inP (N, \lam {n} p => transport U (inv (midSum-diff {_} {S} id<=suc) *> midSum_suc) (g p id<=suc)) + } + +\lemma series_<= {b c : Series Real} (b>=0 : \Pi (j : Nat) -> 0 <= b j) (s : \Pi (j : Nat) -> b j <= c j) (cc : IsConvSeries c) : IsConvSeries b + => series-conv \lam eps>0 => \case series-conv.conv cc eps>0 \with { + | inP (N,g) => inP (N, \lam p => transport2 (<=) + (inv $ RealField.abs-ofPos $ midSum>=0 b>=0) + (inv $ RealField.abs-ofPos $ midSum>=0 \lam j => b>=0 j <=∘ s j) + (midSum_<= \lam {j} _ _ => s j) <∘r g p) + } + +\lemma series_<=-abs {A : PseudoNormedAbGroup} {b c : Series A} (s : \Pi (j : Nat) -> norm (b j) <= norm (c j)) (cc : IsAbsConvSeries c) : IsAbsConvSeries b + => series_<= (\lam j => norm>=0) s cc + +\lemma series_*_lim {A : PseudoNormedRing} {b c : Series A} {l : A} (bl : A.IsLimit b l) (cc : IsAbsConvSeries c) : IsAbsConvSeries \lam n => b n * c n + => series-conv \lam {eps} eps>0 => + \have | delta1>0 : 0 < norm l + 1 => linarith norm>=0 + | delta2>0 : 0 < pos-inv delta1>0 * eps => OrderedSemiring.<_*_positive_positive (pos-inv>0 delta1>0) eps>0 + \in \case limit-metric-char.1 bl RealAbGroup.zro0 \with { + | inP (N,g), inP (M,h) => inP (N ∨ M, \lam p => midSum_norm {_} {_} {N ∨ M} <∘r + transport2 (<=) zro-left (inv $ midSum-split join-right p) (RealField.<=_+ (midSum>=0 \lam j => <=_*_positive_positive (LinearOrder.<_<= delta1>0) norm>=0) $ + midSum_<= \lam {j} p' _ => transportInv (`<= _) (RealField.abs-ofPos norm>=0) (A.norm_*_<= <=∘ <=_*_positive-left (linarith $ norm_-right <∘r transport (`< 1) A.norm-dist (g $ join-left <=∘ p')) norm>=0)) <∘r + (rewrite (pos-inv-right,ide-left,midSum-ldistr) in transportInv (_ <) RealField.*-assoc (RealField.<_*_positive-right delta1>0 $ RealField.abs>=id <∘r h (join-right <=∘ p)))) + } + +\lemma geometric-series-conv {x : Real} (p : RealAbGroup.abs x < 1) : seriesSum (pow x) = defined (pos-inv (diff-pos p)) + => generalized (RealField.pos#0 $ linarith $ RealField.abs>=id <∘r p) p + \where { + \lemma pow_+1-bound {e : Real} (e>=0 : 0 <= e) {n : Nat} : 1 + e * n <= pow (e + 1) n \elim n + | 0 => simplify <=-refl + | suc n => later (rewrite (inv (RealAbGroup.+-rat {n} {1}), ldistr, ldistr, rdistr) $ + linarith (<=_*_positive_positive (<=_*_positive_positive e>=0 $ rat_real_<=.1 $ fromInt_<= $ pos<=pos zero<=_) e>=0 : 0 <= e * n * e)) <=∘ <=_*_positive-left (pow_+1-bound e>=0) linarith + + \lemma pow_>1-bound {b : Real} (b>1 : 1 < b) (B : Nat) : ∃ (n : Nat) ((B : Real) < pow b n) \elim B + | 0 => inP (0, RealAbGroup.zro inP (1, rewrite ide-left b>1) + | 2 => \have b-1>0 : 0 < b - 1 => linarith + \in \case Real.natBounded {pos-inv b-1>0} \with { + | inP (n,nb) => inP (n, rewrite (linarith : b = (b - 1) + 1, linarith : Real.fromRat 2 = (1 : Real) + 1) $ + <_+-right 1 (transport (`< _) (pos-inv-right b-1>0) $ later $ <_*_positive-right b-1>0 $ real_<_U.2 nb) <∘l pow_+1-bound (LinearOrder.<_<= b-1>0)) + } + | suc (suc (suc B)) => \case pow_>1-bound b>1 (suc (suc B)) \with { + | inP (N,p) => inP (N + N, rewrite pow_+ $ later (rewrite RealField.*-rat $ real_<_L.2 $ fromInt_< linarith) <∘ + <_*_positive-right (real_<_L.2 $ later idp) p <∘ <_*_positive-left p (RealField.pow>0 linarith)) + } + + \lemma pow_1/2-bound {n : Nat} : RealField.pow (ratio 1 2) n <= RealField.pos-inv {suc n} (real_<_L.2 $ later idp) \elim n + | 0 => transportInv (_ <=) pos-inv_ide <=-refl + | suc n => <=_*_positive-left pow_1/2-bound linarith <=∘ + \have zro<2 : RealField.zro < Real.fromRat 2 => linarith + \in rewrite (inv (RealField.pos-inv_rat zro<2), pos-inv_*) $ pos-inv_<= (real_<_L.2 $ later idp) (RealField.<_*_positive_positive (real_<_L.2 $ later idp) zro<2) $ + later $ rewrite RealField.*-rat $ rat_real_<=.1 linarith + + \lemma pow_<1-bound {a : Real} (a<1 : a < 1) {eps : Real} (eps>0 : 0 < eps) : ∃ (n : Nat) (pow a n < eps) + => \case Real.natBounded {pos-inv eps>0} \with { + | inP (B,Bb) => \case real-located {a} {0} {ratio 1 2} (real_<_L.2 $ later idp) \with { + | byLeft a>0 => \case pow_>1-bound {pos-inv a>0} (pos-inv>1 a>0 a<1) B \with { + | inP (n,p) => inP (n, pos-inv_<-conv (RealField.pow>0 a>0) eps>0 $ real_<_U.2 Bb <∘ transport (_ <) (pos-inv_pow a>0) p) + } + | byRight a<1/2 => \case real-located {a} {RealField.negative (ratio 1 2)} {0} linarith \with { + | byLeft a>-1/2 => inP (B, RealField.abs>=id <∘r transportInv (`< _) OrderedRing.abs_pow + (pow_<=-monotone RealField.abs>=0 (join-univ (LinearOrder.<_<= a<1/2) (LinearOrder.<_<= $ RealField.negative_<-left a>-1/2)) <∘r + pow_1/2-bound <∘r transport (_ <) (pos-inv_pos-inv eps>0) + (pos-inv_< (pos-inv>0 eps>0) (real_<_L.2 $ later idp) $ real_<_U.2 Bb <∘ real_<_L.2 (fromInt_< $ pos inP (1, transportInv (`< _) ide-left $ a<0 <∘ eps>0) + } + } + } + + \protected \lemma generalized {X : CompleteValuedRing} {x : X} (xi : Inv (1 - x)) (|x|<1 : norm x < 1) : seriesSum (pow x) = defined xi.inv + => seriesSum_defined {_} {pow x} \lam {eps} eps>0 => + \have |1-x|>0 : 0 < norm (1 - x) => linarith norm_ide <∘l norm_-left + \in \case pow_<1-bound |x|<1 {eps * norm (1 - x)} $ RealField.<_*_positive_positive eps>0 |1-x|>0 \with { + | inP (N,q) => inP (N, later \lam N<=n => rewrite (\peval partialSum _ _, X.geometric-partial-sum) $ norm_*_<= <∘r <=_*_positive-left norm_<=_pow norm>=0 <∘r + transport (_ <) (*-assoc *> pmap (_ *) (inv norm_* *> pmap norm xi.inv-right *> norm_ide) *> ide-right) (<_*_positive-left (pow_<=-degree norm>=0 (LinearOrder.<_<= |x|<1) N<=n <∘r q) $ + <_*_positive-cancel-right (LinearOrder.<_<= |1-x|>0) $ transport2 (<) (inv zro_*-left) (inv norm_ide *> pmap norm (inv xi.inv-left) *> norm_*) zro linarith $ RealAbGroup.abs>=id {x} + } + +\lemma geometric-series-absConv {X : PseudoNormedRing} {x : X} (p : norm x < 1) : IsAbsConvSeries (pow x) + => series_<= (\lam j => norm>=0) (\lam j => norm_<=_pow) $ defined-ext.isDefined $ geometric-series-conv $ rewrite (RealField.abs-ofPos norm>=0) p + +\lemma ratio-test {X : PseudoNormedAbGroup} {S : Series X} (b : Series Real) (bp : \Pi (n : Nat) -> norm (S (suc n)) <= norm (S n) * b n) + {l : Real} (l<1 : l < 1) (bl : RealNormed.IsLimit b l) : IsAbsConvSeries S + => \case real_<-char.1 (LinearOrder.<_join-univ l<1 zro \case bl (OBall-open {_} {r - l} {l}) (rewrite dist-refl $ linarith (usingOnly (join-left <∘r lz (series-shifts-conv N).2 + \have r>=0 => join-right <=∘ LinearOrder.<_<= lz norm>=0) (iter-bound (\lam j => norm>=0) r>=0 (\lam j => bp (j + N)) + (\lam j => linarith (usingOnly (RealAbGroup.abs>=_- <=∘ LinearOrder.<_<= (rewrite norm-dist in g (NatSemiring.<=_+ zero<=_ <=-refl)))))) $ + absConv-isConv $ series_*_lim const-limit $ geometric-series-absConv $ later $ rewrite (RealAbGroup.abs-ofPos r>=0) r<1 + } + } + \where { + \lemma iter-bound {f b : Nat -> Real} (f>=0 : \Pi (j : Nat) -> 0 <= f j) {r : Real} (r>=0 : 0 <= r) + (bp : \Pi (n : Nat) -> f (suc n) <= f n * b n) (bb : \Pi (n : Nat) -> b n <= r) (j : Nat) : f j <= f 0 * pow r j \elim j + | 0 => rewrite ide-right <=-refl + | suc j => bp j <=∘ <=_*_positive-right (f>=0 j) (bb j) <=∘ transport (_ <=) *-assoc (<=_*_positive-left (iter-bound f>=0 r>=0 bp bb j) r>=0) + } + +\lemma MTest {X : \Set} {Y : PseudoNormedAbGroup} (f : Nat -> X -> Y) (M : Nat -> Real) + (Mp : \Pi (n : Nat) (x : X) -> norm (f n x) <= M n) (Mc : IsConvSeries M) : IsUniFuncConvergent \lam n x => partialSum (f __ x) n + => \lam Du => \case dist-uniform.1 Du \with { + | inP (eps,eps>0,h) => \case series-conv.conv Mc eps>0 \with { + | inP (N,g) => inP (N, \lam x => \case h (partialSum (f __ x) N) \with { + | inP (V,DV,Vg) => inP (V, DV, \lam p => Vg $ rewrite (norm-dist, norm_-, inv $ midSum-diff {_} {f __ x} p) $ + rewrite (RealAbGroup.abs-ofPos $ midSum>=0 \lam j => norm>=0 <=∘ Mp j x) (midSum_norm <=∘ midSum_<= \lam _ _ => Mp _ x) <∘r g p) + }) + } + } + +\lemma partialSum-cover {X : CoverSpace} {Y : TopAbGroup} (f : Nat -> CoverMap X Y) (n : Nat) : CoverMap X Y \lam x => partialSum (f __ x) n + => transportInv (CoverMap X Y) (ext \lam x => \peval partialSum _ _) $ BigSum-cover \lam (j : Fin n) => f j \ No newline at end of file diff --git a/src/Arith/Int.ard b/src/Arith/Int.ard index 59ae566b..f4edfcde 100644 --- a/src/Arith/Int.ard +++ b/src/Arith/Int.ard @@ -320,6 +320,10 @@ | neg (suc n) => idp } +\lemma iabs=abs {x : Int} : pos (iabs x) = IntRing.abs x \elim x + | pos n => inv $ IntRing.abs-ofPos $ pos<=pos zero<=_ + | neg n => inv $ IntRing.abs-ofNeg neg<=pos + \lemma iabs_* {x y : Int} : iabs (x * y) = iabs x * iabs y \elim x, y | pos n, pos m => idp | pos n, neg m => idp diff --git a/src/Arith/Real.ard b/src/Arith/Real.ard index 9fde77e1..d4346185 100644 --- a/src/Arith/Real.ard +++ b/src/Arith/Real.ard @@ -127,6 +127,11 @@ | inl q U-closed Uq q transport U q=r Uq } + + \lemma natBounded : ∃ (n : Nat) (U n) + => \case U-inh \with { + | inP (a,Ua) => inP (iabs $ rat_ceiling a, U_<= Ua $ rat_ceiling>id <=∘ later (rewrite iabs=abs $ fromInt_<= LinearlyOrderedAbGroup.abs>=id)) + } } \instance UpperRealAbMonoid : AbMonoid UpperReal @@ -215,6 +220,15 @@ => rewrite (\peval join x y) <->refl } +\func \infix 4 ∃ (a : Rat) (x.U a) (y.L a) + +\func \infix 4 <=L (x y : LowerReal) : \Prop + => \Pi {a : Rat} -> x.L a -> y.L a + +\lemma inP (a, x U q -> Empty | LU-located {q r : Rat} : q < r -> L q || U r @@ -528,7 +542,7 @@ => transport2 (RealAbGroup.<) zro-left half+half $ <_+-left (half x) (half>0 x>0) \lemma zro real_<-char.2 $ inP $ later (ratio 1 2, idp, idp) + => real_<-rat-char.2 $ inP $ later (ratio 1 2, idp, idp) {- \lemma *'-char {x y : Real} {a : Rat} {b : Rat} (b=0 : 0 <= b) (c>=0 : 0 <= c) (a<=bc : a <= b * c) @@ -603,7 +617,7 @@ \open RealAbGroup(negative_L,+_L) -\lemma real_<-char {x y : Real} : x < y <-> ∃ (a : Rat) (x.U a) (y.L a) +\lemma real_<-rat-char {x y : Real} : x < y <-> ∃ (a : Rat) (x.U a) (y.L a) => (\case +_L.1 __ \with { | inP (b,b0) => inP (b, x.U-closed (negative_L.1 x<-c) linarith, b +_L.2 $ inP (b, b ∃ (a : Real) (x < a) (a < y) + => (\lam x \case real_<-rat-char.1 x inP (a, real_<_U.2 x x x.L a - => <->trans real_<-char (\lam (inP (b,a x.L-closed b \case x.L-rounded a <->trans real_<-rat-char (\lam (inP (b,a x.L-closed b \case x.L-rounded a inP (b, a x.U a - => <->trans real_<-char (\lam (inP (b,x x.U-closed x <->trans real_<-rat-char (\lam (inP (b,x x.U-closed x Real.fromRat a < Real.fromRat b => <->sym real_<_L @@ -642,7 +661,7 @@ \instance RealDenseOrder : UnboundedDenseLinearOrder | LinearOrder => RealAbGroup - | isDense x \case real_<-char.1 x \case real_<-rat-char.1 x inP (a, real_<_U.2 x \case U-inh {x} \with { @@ -656,24 +675,24 @@ => (\lam h a \case L-rounded a \case y.LU-located a a absurd $ h $ real_<-char.2 $ inP (b,y absurd $ h $ real_<-rat-char.2 $ inP (b,y \case real_<-char.1 p \with { + }, \lam f p => \case real_<-rat-char.1 p \with { | inP (a,y y.LU-disjoint (f a \case real_<-char.1 p \with { + => \case real_<-rat-char.1 p \with { | inP (a',a \case L-rounded a' \case x.LU-located a' byLeft $ real_<-char.2 $ inP (a', a byRight $ real_<-char.2 $ inP (b', x byLeft $ real_<-rat-char.2 $ inP (a', a byRight $ real_<-rat-char.2 $ inP (b', x0 : 0 < eps) : ∃ (a : Real) (a < x) (x < a + eps) - => \case real_<-char.1 eps>0 \with { + => \case real_<-rat-char.1 eps>0 \with { | inP (eps',eps'>0,eps' \case x.LU-focus eps' eps'>0 \with { | inP (a,a inP (a, real_<_L.2 a funcLimit (\lam n x => partialSum (powerSeries (\lam n => Real.fromRat $ RatField.finv (fac n)) __ x) n) (powerSeriesConv-funcConv exp-series-conv) + \where { + \lemma exp-series-conv : IsPowerSeriesConv \lam n => Real.fromRat $ RatField.finv (fac n) + => power-ratio-test-inf _ (\lam n => Real.fromRat $ RatField.finv (suc n)) (\lam n => later $ + rewrite (RealAbGroup.abs-ofPos $ rat_real_<=.1 $ LinearOrder.<_<= $ RatField.finv>0 $ fromInt_< $ pos0 {suc n}, + RealAbGroup.abs-ofPos $ rat_real_<=.1 $ LinearOrder.<_<= $ RatField.finv>0 $ fromInt_< $ pos0) $ + RealAbGroup.=_<= $ pmap Real.fromRat (pmap (\lam x => finv (Rat.fromInt (pos x))) *-comm *> RatField.finv_* {fac n} {suc n} *> *-comm) *> inv RealField.*-rat) inv-limit + + \lemma inv-limit : RealNormed.IsLimit (\lam n => RatField.finv (suc n)) 0 + => \lam Uo U0 => \case (dist_open {RealNormed}).1 Uo U0 \with { + | inP (eps,eps>0,h) => \case UpperReal.natBounded {OrderedField.pos-inv eps>0} \with { + | inP (N,p) => inP (N, \lam N<=n => h $ transportInv (`< _) (norm-dist *> norm_-) $ unfold (-) $ + \have lem => real_<_L.2 $ RatField.<-char $ pos pmap (`* _) (RealField.*-rat *> pmap Real.fromRat (RatField.finv-left \lam p => suc/=0 $ unpos $ pmap ratNom p)) *> ide-left) $ + RealField.<_*_positive-right lem $ transport (`< _) (RealField.pos-inv-left eps>0) $ <_*_positive-left (real_<_U.2 p <∘ real_<_U.2 (fromInt_< (pos0) + } + } + } \ No newline at end of file diff --git a/src/Arith/Real/Field.ard b/src/Arith/Real/Field.ard index 846af18d..b26469c9 100644 --- a/src/Arith/Real/Field.ard +++ b/src/Arith/Real/Field.ard @@ -26,6 +26,7 @@ \import Topology.NormedAbGroup \import Topology.TopAbGroup.Product \import Topology.TopSpace +\import Topology.TopSpace.Product \import Topology.UniformSpace \import Topology.UniformSpace.Product \open LinearlyOrderedAbGroup @@ -43,8 +44,8 @@ | *c-comm-left => inv RealField.*-assoc | coefMap => Real.fromRat | coefMap_*c => inv RealField.ide-right - | coef_< p => real_<-char.2 (isDense p) - | coef_<-inv p => \case real_<-char.1 p \with { + | coef_< p => real_<-rat-char.2 (isDense p) + | coef_<-inv p => \case real_<-rat-char.1 p \with { | inP (a,x x0 y>0 => (*_positive-L x>0 y>0).2 \case L-rounded x>0, L-rounded y>0 \with { | inP (a,a0), inP (a',a'0) => inP (a, a', a>0, a'>0, a0 a'>0) } - | positive=>#0 {x : Real} x>0 => Monoid.Inv.lmake (pos-inv x>0) $ exts - (\lam c => ext (\lam l => \case (*_positive-L (pos-inv>0 x>0) x>0).1 l \with { + | positive=>#0 {x : Real} x>0 => Monoid.Inv.lmake (real-pos-inv x>0) $ exts + (\lam c => ext (\lam l => \case (*_positive-L (real-pos-inv>0 x>0) x>0).1 l \with { | inP (a, a', a>0, a'>0, byLeft a<=0, a' absurd linarith | inP (a, a', a>0, a'>0, byRight x c_/= a>0) (<_*_positive-right a>0 $ Real.LU-less a' (*_positive-L (pos-inv>0 x>0) x>0).2 $ unfold LowerReal.L \case Real.LU_*-focus-left x>0 c<1 \with { + }, \lam c<1 => (*_positive-L (real-pos-inv>0 x>0) x>0).2 $ unfold LowerReal.L \case Real.LU_*-focus-left x>0 c<1 \with { | inP (b,bc \case L-rounded bc0 \with { | inP (a',a'0) => \have b>0 => Real.LU-less x>0 x0 b>0, a''>0 <∘l join-right, byRight $ transportInv x.U RatField.finv_finv x pmap (`*' c) (RatField.finv-left $ RatField.>_/= b>0) *> ide-left) (RatField.<_*_positive-right (finv>0 b>0) bc0 b>0) join-left) } }), - \lam d => ext (\lam u => \case (*_positive-U (pos-inv>0 x>0) x>0).1 u \with { + \lam d => ext (\lam u => \case (*_positive-U (real-pos-inv>0 x>0) x>0).1 u \with { | inP (b,b',(b>0,b1 transport (`< _) (finv-right $ RatField.>_/= b>0) (RatField.<_*_positive-right b>0 $ Real.LU-less b11 => (*_positive-U (pos-inv>0 x>0) x>0).2 \case Real.LU_*-focus-right x>0 d>1 \with { + }, \lam d>1 => (*_positive-U (real-pos-inv>0 x>0) x>0).2 \case Real.LU_*-focus-right x>0 d>1 \with { | inP (a,a>0,a \case U-rounded x inP (finv a, b', (finv>0 a>0, transportInv x.L RatField.finv_finv a pmap (`*' _) (RatField.finv-left $ RatField.>_/= a>0) *> ide-left) $ <_*_positive-right (finv>0 a>0) b' dense-lift-unique rat_real rat_real.dense f g p x \lemma unique2 {X : SeparatedCoverSpace} (f g : CoverMap (RealNormed ⨯ RealNormed) X) (p : \Pi (x y : Rat) -> f (x,y) = g (x,y)) {x y : Real} : f (x,y) = g (x,y) - => dense-lift-unique (prod rat_real rat_real) (prod.isDense rat_real.dense rat_real.dense) f g (\lam s => p s.1 s.2) (x,y) + => dense-lift-unique (prod rat_real rat_real) (ProductTopSpace.prod.isDense rat_real.dense rat_real.dense) f g (\lam s => p s.1 s.2) (x,y) \lemma unique3 {X : SeparatedCoverSpace} (f g : CoverMap (RealNormed ⨯ RealNormed ⨯ RealNormed) X) (p : \Pi (x y z : Rat) -> f ((x,y),z) = g ((x,y),z)) {x y z : Real} : f ((x,y),z) = g ((x,y),z) - => dense-lift-unique (prod (prod rat_real rat_real) rat_real) (prod.isDense (prod.isDense rat_real.dense rat_real.dense) rat_real.dense) f g (\lam s => p s.1.1 s.1.2 s.2) ((x,y),z) + => dense-lift-unique (prod (prod rat_real rat_real) rat_real) (ProductTopSpace.prod.isDense (ProductTopSpace.prod.isDense rat_real.dense rat_real.dense) rat_real.dense) f g (\lam s => p s.1.1 s.1.2 s.2) ((x,y),z) \lemma *-rat-locally-uniform : LocallyUniformMap (RatNormed ⨯ RatNormed) RatNormed (\lam s => s.1 *' s.2) => LocallyUniformMetricMap.makeLocallyUniformMap2 (*') \lam eps>0 => \case L-rounded (real_<_L.1 eps>0) \with { @@ -118,7 +119,7 @@ rewrite norm-dist $ real_<_L.2 $ L-closed eps'=0 $ <_<= yy'=0 $ <_<= xx'0 <∘l + transport (`< _) rdistr (<_*_positive-left (linarith (abs_-right {_} {x0} {x}, abs_-right {_} {y0} {y}, abs_-right {_} {y} {y'}, meet-right : gamma <= 1) : abs x + abs y' < abs x0 + abs y0 + 3) gamma>0 <∘l RatField.<=_*_positive-right (<_<= lem) meet-left <=∘ Preorder.=_<= (inv *-assoc *> pmap (`*' _) (finv-right $ StrictPoset.>_/= $ later lem) *> ide-left))))) } @@ -130,7 +131,7 @@ => *-cover-def (x,y) \lemma *-rat {x y : Rat} : x * y = {Real} x *' y - => (\peval x * y) *> dense-lift-char {_} {_} {_} {_} {prod.isDenseEmbedding rat_real.dense-coverEmbedding rat_real.dense-coverEmbedding} {rat_real ∘ *-rat-locally-uniform} (x,y) + => (\peval x * y) *> dense-lift-char (prod.isDenseEmbedding rat_real.dense-coverEmbedding rat_real.dense-coverEmbedding) {rat_real ∘ *-rat-locally-uniform} (x,y) \lemma *-cover : CoverMap (ProductCoverSpace RealNormed RealNormed) RealNormed (\lam s => s.1 * s.2) => transportInv (CoverMap _ _) (ext \lam s => \peval s.1 * s.2) *-cover-def @@ -166,7 +167,7 @@ | inP (a,a0), inP (a',a'0) => ((*_positive-char x>0 y>0 {a *' a' - 1} {d}).2 $ inP (a, b, a', b', a>0, a'>0, (a0 : x.L 0) : Real \cowith + \func real-pos-inv {x : Real} (x>0 : x.L 0) : Real \cowith | L a => a <= 0 || x.U (finv a) | L-inh => inP (0, byLeft <=-refl) | L-closed {a} {b} p b \case dec<_<= 0 b, \elim p \with { @@ -203,6 +204,31 @@ | inr a<=0 => byLeft (byLeft a<=0) } - \lemma pos-inv>0 {x : Real} (x>0 : x.L 0) : LowerReal.L {pos-inv x>0} 0 + \lemma real-pos-inv>0 {x : Real} (x>0 : x.L 0) : LowerReal.L {real-pos-inv x>0} 0 => byLeft <=-refl - } \ No newline at end of file + + \lemma pos-inv_rat {x : Rat} (x>0 : 0 < Real.fromRat x) : RealField.pos-inv x>0 = Real.fromRat (finv x) + => Monoid.Inv.inv-isUnique (RealField.pos#0 x>0) (Monoid.Inv.lmake _ $ *-rat *> pmap Real.fromRat (RatField.finv-left \lam x=0 => <-irreflexive $ rewrite x=0 in x>0)) idp + } + +\func half (x : Real) => x * ratio 1 2 + +\lemma half>0 {x : Real} (x>0 : 0 < x) : 0 < half x + => linarith + +\lemma half0 : 0 < x) : half x < x + => linarith + +\func halfs (n : Nat) (x : Real) : Real \elim n + | 0 => x + | suc n => half (halfs n x) + +\lemma halfs>0 (n : Nat) {x : Real} (x>0 : 0 < x) : 0 < halfs n x \elim n + | 0 => x>0 + | suc n => half>0 (halfs>0 n x>0) + +\lemma half+half {x : Real} : half x + half x = x + => linarith + +\lemma halving {X : PseudoMetricSpace} {z x y : X} {eps : Real} (d1 : dist z x < half eps) (d2 : dist z y < half eps) : dist x y < eps + => dist-triang <∘r OrderedAddMonoid.<_+ (rewrite dist-symm in d1) d2 <∘l Preorder.=_<= half+half diff --git a/src/Arith/Real/Root.ard b/src/Arith/Real/Root.ard new file mode 100644 index 00000000..9394dcf6 --- /dev/null +++ b/src/Arith/Real/Root.ard @@ -0,0 +1,71 @@ +{- TODO +\import Algebra.Meta +\import Algebra.Monoid +\import Algebra.Ordered +\import Algebra.Ring +\import Arith.Rat +\import Arith.Real +\import Arith.Real.Field +\import Data.Or +\import Function.Meta +\import Logic +\import Logic.Meta +\import Meta +\import Order.Lattice +\import Order.LinearOrder +\import Order.PartialOrder +\import Order.StrictOrder +\import Paths +\import Paths.Meta +\open Monoid(pow) +\open LinearlyOrderedSemiring +\open LinearOrder \hiding (<=, Dec) + +\func rootR (n : Nat) (x : Real) (x>=0 : 0 <= x) : Real \cowith + | L a => (a < 0) || x.L (pow a n) + | L-inh => inP (-1, byLeft idp) + | L-closed {q} {q'} e q' \case dec<_<= q' 0, \elim e \with { + | inl q'<0, _ => byLeft q'<0 + | inr q'>=0, byLeft q<0 => absurd linarith + | inr q'>=0, byRight q^n byRight $ x.L_<= q^n=0 $ <_<= q' \case dec<_<= q 0, \elim __ \with { + | inl q<0, _ => inP (RatField.mid q 0, byLeft $ RatField.midleft q<0) + | inr q>=0, byLeft q<0 => absurd (q>=0 q<0) + | inr q>=0, byRight q^n \case L-rounded q^n \case pow-L-rounded q>=0 q^n inP (r, byRight $ L-closed b x.U (pow b n) + | U-inh => {?} + | U-closed => {?} + | U-rounded => {?} + | LU-disjoint => {?} + | LU-located => {?} + | LU-focus => {?} + \where { + \sfunc pow>0-rounded {b : Rat} {n : Nat} (n/=0 : n /= 0) (b>0 : 0 < b) : \Sigma (a : Rat) (0 < a) (pow a n < b) + => ((b ∧ 1) * ratio 1 2, RatField.<_*_positive_positive (<_meet-univ b>0 idp) idp, transport2 (<) (inv CMonoid.pow_*-comm) ide-right $ + <_*_positive-right {_} {pow (b ∧ 1) n} {pow (ratio 1 2) n} {1} (RatField.pow>0 $ <_meet-univ b>0 idp) (pow<=id (<_<= $ later idp) (<_<= $ later idp) n/=0 <∘r idp) <∘l {_} {_} {_} {b * 1} + transport2 (<=) (inv ide-right) (inv ide-right) (pow<=id (meet-univ (<_<= b>0) $ <_<= zro=0 : 0 <= a) {n : Nat} (a^n inP (a + 1, linarith, a^n \case dec<_<= 0 a \with { + | inl a>0 => \case (RealField.*_positive-U (RatField.pow>0 a>0) a>0).1 $ rewrite RealField.*-rat a^n \case pow-L-rounded a>=0 a^n + \have a'a''>0 : 0 < a' ∧ a'' => <_meet-univ (a>=0 <∘r a=0 <∘r a0 $ a'a''>0) meet-left <∘r + <=_*_positive-left (pow_<=-monotone (<_<= a'a''>0) meet-right <=∘ <_<= a''^n=0 <∘r a + \have | a=0 : a = 0 => <=-antisymmetric a<=0 a>=0 + | r => pow>0-rounded {b} {suc n} (\case __) $ rewrite (a=0,Algebra.Ring.Ring.zro_*-right) in a^n 1 - | suc n => suc n Nat.* fac n \ No newline at end of file + | suc n => suc n Nat.* fac n + +\lemma fac>0 {n : Nat} : 0 < fac n \elim n + | 0 => NatSemiring.zero rewrite NatSemiring.*-comm $ LinearlyOrderedAbMonoid.<=_+-left zero<=_ fac>0 \ No newline at end of file diff --git a/src/Order/Directed.ard b/src/Order/Directed.ard new file mode 100644 index 00000000..3cb0caac --- /dev/null +++ b/src/Order/Directed.ard @@ -0,0 +1,20 @@ +\import Logic +\import Logic.Meta +\import Operations +\import Order.PartialOrder + +\class DirectedSet \extends Preorder + | isInhabitted : ∃ E + | isDirected (x y : E) : ∃ (z : E) (x <= z) (y <= z) + +\instance ProductDirectedSet (X Y : DirectedSet) : DirectedSet (\Sigma X Y) + | Preorder => ProductPreorder X Y + | isInhabitted => \case X.isInhabitted, Y.isInhabitted \with { + | inP x, inP y => inP (x,y) + } + | isDirected s t => \case isDirected s.1 t.1, isDirected s.2 t.2 \with { + | inP (x,p,q), inP (y,p',q') => inP ((x,y), (p,p'), (q,q')) + } + +\instance DirectedSetHasProduct : HasProduct DirectedSet + | Product => ProductDirectedSet \ No newline at end of file diff --git a/src/Order/Lattice.ard b/src/Order/Lattice.ard index e484fb46..3734f8b7 100644 --- a/src/Order/Lattice.ard +++ b/src/Order/Lattice.ard @@ -10,6 +10,7 @@ \import Logic \import Logic.Meta \import Meta +\import Order.Directed \import Paths \import Order.PartialOrder \import Paths.Meta @@ -172,6 +173,17 @@ \lemma top-right {x : E} : x ∧ top = x => <=-antisymmetric meet-left (meet-univ <=-refl top-univ) + + \func BigMeet (l : Array E) : E + => Big (∧) top l + + \lemma BigMeet-cond {l : Array E} (j : Fin l.len) : BigMeet l <= l j \elim l, j + | a :: l, 0 => meet-left + | a :: l, suc j => meet-right <=∘ BigMeet-cond j + + \lemma BigMeet-univ {l : Array E} {x : E} (p : \Pi (j : Fin l.len) -> x <= l j) : x <= BigMeet l \elim l + | nil => top-univ + | a :: l => meet-univ (p 0) $ BigMeet-univ \lam j => p (suc j) } \where { \use \coerce toMonoid (L : MeetSemilattice) : CMonoid L \cowith | ide => top @@ -181,10 +193,13 @@ | *-comm => meet-comm } - \class JoinSemilattice \extends Order.Lattice.JoinSemilattice { + \class JoinSemilattice \extends Order.Lattice.JoinSemilattice, DirectedSet { | bottom : E | bottom-univ {x : E} : bottom <= x + | isInhabitted => inP bottom + | isDirected x y => inP (x ∨ y, join-left, join-right) + \func BigJoin (l : Array E) : E => Big (∨) bottom l diff --git a/src/Order/PartialOrder.ard b/src/Order/PartialOrder.ard index c8ba6563..71f8868e 100644 --- a/src/Order/PartialOrder.ard +++ b/src/Order/PartialOrder.ard @@ -74,10 +74,13 @@ } \instance ProductPoset (P Q : Poset) : Poset (\Sigma P Q) + | Preorder => ProductPreorder P Q + | <=-antisymmetric (p,q) (p',q') => ext (<=-antisymmetric p p', <=-antisymmetric q q') + +\instance ProductPreorder (P Q : Preorder) : Preorder (\Sigma P Q) | <= (x,y) (x',y') => \Sigma (x <= x') (y <= y') | <=-refl => (<=-refl, <=-refl) | <=-transitive (p,q) (p',q') => (<=-transitive p p', <=-transitive q q') - | <=-antisymmetric (p,q) (p',q') => ext (<=-antisymmetric p p', <=-antisymmetric q q') \func subPoset {P : Poset} (S : P -> \Prop) : Poset (\Sigma (x : P) (S x)) \cowith | <= x y => x.1 <= y.1 diff --git a/src/Set/Partial.ard b/src/Set/Partial.ard new file mode 100644 index 00000000..38eade6e --- /dev/null +++ b/src/Set/Partial.ard @@ -0,0 +1,34 @@ +\import Logic +\import Meta +\import Paths +\import Paths.Meta +\import Set + +\record Partial \extends BaseSet + | isDefined : \Prop + | \coerce value : isDefined -> E + \where { + \lemma partial-ext {X : \Set} {u v : Partial X} (d : u.isDefined <-> v.isDefined) (e : \Pi (p : u.isDefined) -> u p = v (d.1 p)) : u = v + => exts (<->_=.1 d, \lam p => e p *> pmap v prop-pi) + } + +\func defined {X : \Set} (x : X) : Partial X \cowith + | isDefined => \Sigma + | value _ => x + +\func undefined {X : \Set} : Partial X \cowith + | isDefined => Empty + | value => \case __ + +\lemma defined-ext {X : \Set} {u : Partial X} {x : X} (d : u.isDefined) (p : u d = x) : u = defined x + => Partial.partial-ext (\lam _ => (), \lam _ => d) \lam q => pmap u prop-pi *> p + \where { + \protected \lemma isDefined (p : u = defined x) : u.isDefined + => transportInv (\lam x => Partial.isDefined {x}) p () + + \protected \lemma value (p : u = defined x) : u (isDefined p) = x + => transportInv (\lam (v : Partial X) => \Pi (p : v.isDefined) -> v p = x) p (\lam _ => idp) (isDefined p) + } + +\lemma undefined-ext {X : \Set} {u : Partial X} (d : Not u.isDefined) : u = undefined + => Partial.partial-ext (d,absurd) \lam p => absurd (d p) \ No newline at end of file diff --git a/src/Set/Subset.ard b/src/Set/Subset.ard index 25b1ab61..b510afc8 100644 --- a/src/Set/Subset.ard +++ b/src/Set/Subset.ard @@ -1,6 +1,8 @@ +\import Data.Array \import Function.Meta \import Logic \import Logic.Meta +\import Meta \import Order.Lattice \import Order.PartialOrder \import Paths @@ -26,20 +28,23 @@ \func CoverInter {X : \hType} (C : Set (Set X)) (D : Set (Set X)) : Set (Set X) => \lam W => ∃ (U : C) (V : D) (W = U ∧ {SetLattice X} V) + + \func CoverInterBig {X : \hType} (Cs : Array (Set (Set X))) : Set (Set X) + => Big CoverInter (single (top {SetLattice X})) Cs } -\func single {A : \Set} (a : A) : Set A +\func single {X : \Set} (a : X) : Set X => a = -\lemma single_<= {A : \Set} {a : A} {U : Set A} (Ua : U a) : single a ⊆ U +\lemma single_<= {X : \Set} {a : X} {U : Set X} (Ua : U a) : single a ⊆ U => \lam p => rewriteI p Ua -\func \infix 8 ^-1 {A B : \hType} (f : A -> B) (S : Set B) : Set A +\func \infix 8 ^-1 {X Y : \hType} (f : X -> Y) (S : Set Y) : Set X => \lam a => S (f a) -\type Subset \alias \infix 4 ⊆ {A : \hType} (U V : Set A) => \Pi {x : A} -> U x -> V x +\type Subset \alias \infix 4 ⊆ {X : \hType} (U V : Set X) => \Pi {x : X} -> U x -> V x -\func Compl {A : \hType} (U : Set A) : Set A +\func Compl {X : \hType} (U : Set X) : Set X => \lam x => Not (U x) \instance SetLattice (A : \hType) : Locale (Set A) @@ -85,21 +90,40 @@ \lemma Refines-inter-right {X : \hType} {C D : Set (Set X)} : Refines (Set.CoverInter C D) D => \lam {_} (inP (_,_,V,DV,idp)) => inP (V, DV, meet-right) +\lemma Refines-inter-big {X : \hType} (Cs : Array (Set (Set X))) (j : Fin Cs.len) : Refines (Set.CoverInterBig Cs) (Cs j) \elim Cs, j + | C :: Cs, 0 => Refines-inter-left + | C :: Cs, suc j => Refines-trans Refines-inter-right (Refines-inter-big Cs j) + \lemma Refines-inter {X : \hType} {C D C' D' : Set (Set X)} (r : Refines C D) (r' : Refines C' D') : Refines (Set.CoverInter C C') (Set.CoverInter D D') => \lam {W} (inP (U,CU,U',C'U',W=UU')) => \case r CU, r' C'U' \with { | inP (V,DV,U<=V), inP (V',D'V',U'<=V') => inP (V ∧ V', inP (V, DV, V', D'V', idp), rewrite W=UU' $ MeetSemilattice.meet-monotone U<=V U'<=V') } -\func extend {A : \Type} {U : Set A} (V : Set (Set.Total U)) : Set A +\lemma CoverInterBig-char {X : \hType} {Cs : Array (Set (Set X))} : Set.CoverInterBig Cs = \lam W => ∃ (Us : Array (Set X) Cs.len) (\Pi (j : Fin Cs.len) -> Cs j (Us j)) (W = Big {Set X} (∧) top Us) \elim Cs + | nil => exts \lam W => ext (\lam p => inP (nil, \case __ \with {}, inv p), \lam (inP t) => inv t.3) + | C :: Cs => pmap (Set.CoverInter C) CoverInterBig-char *> exts \lam W => ext ( + \lam (inP (U, CU, V, inP (Us,CsUs,q), p)) => inP (U :: Us, \case \elim __ \with { + | 0 => CU + | suc j => CsUs j + }, p *> pmap (U ∧) q), + \lam (inP (Us,CsUs,p)) => inP (Us 0, CsUs 0, _, inP (\lam j => Us (suc j), \lam j => CsUs (suc j), idp), p)) + +\func extend {X : \Type} {U : Set X} (V : Set (Set.Total U)) : Set X => \lam x => \Sigma (Ux : U x) (V (x,Ux)) -\lemma extend-mono {A : \Type} {U : Set A} {V W : Set (Set.Total U)} (p : V ⊆ W) : extend V ⊆ extend W +\lemma extend-sub {X : \Type} {U : Set X} {V : Set (Set.Total U)} : extend V ⊆ U + => __.1 + +\lemma extend-mono {X : \Type} {U : Set X} {V W : Set (Set.Total U)} (p : V ⊆ W) : extend V ⊆ extend W => \lam {x} (Ux,Vx) => (Ux, p Vx) -\lemma extend_meet {A : \Type} {U : Set A} {V W : Set (Set.Total U)} : extend (V ∧ W) = extend V ∧ extend W +\lemma extend_meet {X : \Type} {U : Set X} {V W : Set (Set.Total U)} : extend (V ∧ W) = extend V ∧ extend W => <=-antisymmetric (\lam e => ((e.1, e.2.1), (e.1, e.2.2))) (\lam e => (e.1.1, (e.1.2, transport W (ext idp) e.2.2))) -\lemma extend_restrict {A : \Type} {U : Set A} {V : Set A} : extend (Set.restrict {A} {U} V) ⊆ V +\lemma restrict_extend {X : \Type} {U : Set X} {V : Set (Set.Total U)} : Set.restrict (extend V) = V + => <=-antisymmetric (\lam r => transport V (ext idp) r.2) (\lam {x} Vx => (x.2,Vx)) + +\lemma extend_restrict {X : \Type} {U : Set X} {V : Set X} : extend (Set.restrict {X} {U} V) ⊆ V => __.2 \lemma ^-1_<= {A B : \hType} (f : A -> B) {U V : Set B} (p : U ⊆ V) : f ^-1 U ⊆ f ^-1 V diff --git a/src/Topology/Compact.ard b/src/Topology/Compact.ard new file mode 100644 index 00000000..2be6f9e8 --- /dev/null +++ b/src/Topology/Compact.ard @@ -0,0 +1,177 @@ +\import Arith.Nat +\import Arith.Real +\import Data.Or +\import Equiv +\import Function +\import Function.Meta \hiding (#) +\import Logic +\import Logic.Meta +\import Meta +\import Order.Lattice +\import Order.PartialOrder +\import Paths +\import Paths.Meta +\import Set +\import Set.Fin +\import Set.Subset +\import Topology.CoverSpace +\import Topology.CoverSpace.Complete +\import Topology.MetricSpace +\import Topology.UniformSpace +\open ClosurePrecoverSpace +\open Bounded(top,top-univ) + +\func IsTotallyBounded (X : CoverSpace) : \Prop + => Cond X.isCauchy isCauchy + \where { + \protected \func Cond {X : CoverSpace} (P Q : Set (Set (Set X))) => ∀ {C : P} ∃ (U : Array (Set X)) (Q \lam V => ∃ (W : U) (W = V)) (∀ (V : U) (C V)) + + \lemma cond-char {X : CoverSpace} (Q : Set (Set (Set X))) (C : Set (Set X)) + : ∃ (U : Array (Set X)) (Q \lam V => ∃ (W : U) (W = V)) (∀ (V : U) (C V)) <-> ∃ (D : Q) (n : Nat) (f : Fin n -> Set.Total D) (isSurj f) (D ⊆ C) + => (\case \elim __ \with { + | inP (U : Array, QU, h) => inP (\lam V => ∃ (W : U) (W = V), QU, U.len, \lam j => (U j, inP (j,idp)), \lam (_, inP (j,idp)) => inP (j,idp), \lam {V} (inP (j,p)) => rewriteI p (h j)) + }, \case \elim __ \with { + | inP (D, QD, n, g, gs, D<=C) => inP (\lam j => (g j).1, transport Q (later $ <=-antisymmetric (\lam {V} DV => \case gs (V,DV) \with { + | inP (j,p) => inP (j, pmap __.1 p) + }) (\lam {_} (inP (j,idp)) => (g j).2)) QD, \lam j => D<=C (g j).2) + }) + } + +\func IsCompact (X : CompleteCoverSpace) : \Prop + => IsTotallyBounded X + +\func IsTotallyBoundedSet {X : CoverSpace} (U : Set X) : \Prop + => IsTotallyBounded $ CoverTransfer {\Sigma (x : X) (U x)} __.1 + +\lemma totallyBoundedSet-char {X : CoverSpace} {U : Set X} + : IsTotallyBoundedSet U <-> ∀ {C : isCauchy} ∃ (D : Array (Set X)) (isCauchy \lam W => ∃ (V : D) (U ∧ W ⊆ V)) (∀ (V : D) (C V)) + => (\lam f Cc => \case f $ func-cover {PrecoverTransfer-map {Set.Total U} __.1} Cc \with { + | inP (D,Dc,Dp) => \case FinSet.finiteAC Dp \with { + | inP g => inP (\lam j => (g j).1, cauchy-subset Dc \lam {V} (inP (_, inP (j,idp), q)) => inP $ later (j, \lam {x} (Ux,Vx) => transport (_ ⊆) (g j).3 q {x,Ux} Vx), \lam j => (g j).2) + } + }, \lam f Cc => \case f Cc \with { + | inP (D,Dc,Dp) => \case FinSet.finiteAC Dp \with { + | inP g => inP (\lam j => (g j).1, cauchy-subset Dc \lam {V} (inP (j,q)) => inP $ later (_, inP (j,idp), (\lam {x} Vx => q (x.2,Vx)) <=∘ (g j).3), \lam j => (g j).2) + } + }) + +\lemma totallyBoundedSet-uniform-char {X : UniformSpace} {S : Set X} + : IsTotallyBoundedSet S <-> ∀ {C : isUniform} ∃ (D : Array (Set X)) (isCauchy \lam W => ∃ (V : D) (S ∧ W ⊆ V)) (∀ (V : D) (C V)) + => <->trans totallyBoundedSet-char $ later (\lam f Cu => f (X.makeCauchy Cu), \lam f {C} Cc => \case totallyBounded-uniform-char.totallyBounded-closure {UniformTransfer {Set.Total S} __.1} (\lam Cu => \case f Cu \with { + | inP (V,Vc,Vh) => \case FinSet.finiteAC Vh \with { + | inP h => inP (\lam j => (h j).1, cauchy-subset Vc \lam {W} (inP (j,p)) => inP $ later (_, inP (j,idp), (\lam {x} Wx => p (x.2, Wx)) <=∘ (h j).3), \lam j => (h j).2) + } + }) {\lam U => ∃ (V : C) (U = Set.restrict V)} (uniform-cauchy.1 $ later $ cauchy-subset Cc \lam {V} CV => inP $ later (_, inP (V, CV, idp), <=-refl)) \with { + | inP (D,Dc,h) => \case FinSet.finiteAC h \with { + | inP g => inP (\lam j => (g j).1, cauchy-subset Dc \lam {W} (inP (_, inP (j,idp), p)) => inP $ later (j, \lam {x} (Sx,Wx) => transport (__ (x,Sx)) (g j).3 $ p Wx), \lam j => (g j).2) + } + }) + +\lemma totallyBounded-cauchy-uniform {X : UniformSpace} (Xp : X.IsProperUniform) (Xtb : IsTotallyBounded X) {C : Set (Set X)} (Cc : isCauchy C) : isUniform C + => \case Xtb $ X.<=*-cauchy-regular Cc \with { + | inP (D,Dc,f) => \case FinSet.finiteAC f \with { + | inP g => \case FinSet.finiteAC (\lam j => (g j).3) \with { + | inP h => uniform-refine (Xp $ X.uniform-inter-big (\lam j => (h j).1) (\lam j => (h j).2)) \lam {W'} (EW', inP (x,W'x)) => \case cauchy-cover Dc x \with { + | inP (_, inP (j,idp), Dx) => inP ((g j).1, (g j).2, \case Refines-inter-big (\lam j => (h j).1) j EW' \with { + | inP (W,hW,W'<=W) => W'<=W <=∘ Set.Union-cond (later (hW, (x, (Dx, W'<=W W'x)))) <=∘ (h j).3 + }) + } + } + } + } + +\lemma totallyBounded-cauchy-uniform-strong {X : StronglyRegularUniformSpace} (Xp : X.IsWeaklyProperUniform) (Xtb : IsTotallyBounded X) {C : Set (Set X)} (Cc : isCauchy C) : isUniform C + => \case Xtb $ X.s<=*-cauchy-regular Cc \with { + | inP (V,Vc,g) => \case FinSet.finiteAC g \with { + | inP h => Xp $ uniform-refine (X.uniform-inter-big (\lam j W => (W = Compl (V j)) || (W = (h j).1)) (\lam j => (h j).3)) + \lam {W} c => \case rewrite CoverInterBig-char in c \with { + | inP (Ws,We,W=Ws) => \case FinSet.searchFin (\lam j => \Sigma (p : Ws j = (h j).1) (We j = byRight p)) (\lam j => cases (We j) \with { + | byLeft _ => no \lam q => \case q.2 + | byRight p => yes (p,idp) + }) \with { + | inl (j,(p,_),_) => inP ((h j).1, byRight (h j).2, rewrite (W=Ws, inv p) $ Bounded.MeetSemilattice.BigMeet-cond {_} {Ws} j) + | inr f => inP (_, byLeft idp, \lam {x} Wx => \case cauchy-cover Vc x \with { + | inP (_, inP (j,idp), Vjx) => \case f j (cases (We j) \with { + | byLeft q => \case (rewrite q in Bounded.MeetSemilattice.BigMeet-cond {_} {Ws} j (rewrite W=Ws in Wx)) Vjx + | byRight p => (p,idp) + }) + }) + } + } + } + } + +\lemma totallyBounded-uniform-char {X : UniformSpace} (Xp : X.IsProperUniform) : TFAE ( + IsTotallyBounded X, + IsTotallyBounded.Cond X.isUniform isUniform, + IsTotallyBounded.Cond X.isUniform isCauchy + ) => TFAE.cycle ( + \lam tb => transport (\lam P => IsTotallyBounded.Cond P P) (exts \lam C => ext (totallyBounded-cauchy-uniform Xp tb, X.makeCauchy)) tb, + \lam c Cu => \case c Cu \with { + | inP (U,Uu,h) => inP (U, X.makeCauchy Uu, h) + }, + \lam c Cc => totallyBounded-closure c (uniform-cauchy.1 Cc) + ) + \where { + \lemma totallyBounded-closure {X : UniformSpace} (base : IsTotallyBounded.Cond X.isUniform isCauchy) {C : Set (Set X)} (Cc : Closure isUniform C) + : ∃ (D : Array (Set X)) (isCauchy \lam V => ∃ (W : D) (W = V)) (∀ (V : D) (C V)) \elim Cc + | closure Cu => base Cu + | closure-top idp => inP (top :: nil, top-cauchy $ inP $ later (0,idp), \lam (0) => idp) + | closure-refine Dc D \case totallyBounded-closure base Dc \with { + | inP (U,Uc,DU) => \case FinSet.finiteAC (\lam j => D inP (\lam j => (V j).1, cauchy-refine Uc \lam {_} (inP (j,idp)) => inP ((V j).1, inP (j,idp), (V j).3), \lam j => (V j).2) + } + } + | closure-trans {D} Dc {E} Ec idp => (IsTotallyBounded.cond-char isCauchy C).2 \case (IsTotallyBounded.cond-char isCauchy D).1 $ totallyBounded-closure base Dc \with { + | inP (D', D'c, n, V, Vs, D'<=D) => \case FinSet.finiteAC (\lam i => (IsTotallyBounded.cond-char isCauchy (E (V i).1)).1 $ totallyBounded-closure base $ Ec $ D'<=D (V i).2) \with { + | inP E' => \have e : Equiv => SigmaFin.aux {_} {\lam i => (E' i).3} \in inP ( + \lam U => ∃ (i : Fin n) (j : Fin (E' i).3) ((V i).1 ∧ ((E' i).4 j).1 = U), + cauchy-subset (cauchy-glue D'c {\lam V' W' => ∃ (i : Fin n) ((V i).1 = V') ((E' i).1 W')} \lam {V'} D'V' => \case Vs (V',D'V') \with { + | inP (i,p) => cauchy-subset (E' i).2 \lam {W'} E'W' => inP $ later (i, pmap __.1 p, E'W') + }) \lam {_} (inP (V', W', D'V', inP (i,p,E'W'), idp)) => \case (E' i).5 (W',E'W') \with { + | inP (j,q) => inP $ later (i, j, pmap2 (∧) p $ pmap __.1 q) + }, + NatSemiring.BigSum \lam i => (E' i).3, + \lam k => (_, inP ((e k).1, (e k).2, idp)), + \lam (U, inP (i,j,p)) => inP (e.ret (i,j), ext $ pmap (\lam x => (V x.1).1 ∧ ((E' x.1).4 x.2).1) (e.f_ret (i,j)) *> p), + \lam {U} (inP (i,j,p)) => inP (_, _, D'<=D (V i).2, (E' i).6 ((E' i).4 j).2, inv p)) + } + } + } + +\lemma totallyBounded-uniform-strong-char {X : StronglyRegularUniformSpace} (Xp : X.IsWeaklyProperUniform) : TFAE ( + IsTotallyBounded X, + IsTotallyBounded.Cond X.isUniform isUniform, + IsTotallyBounded.Cond X.isUniform isCauchy + ) => TFAE.cycle ( + \lam tb => transport (\lam P => IsTotallyBounded.Cond P P) (exts \lam C => ext (totallyBounded-cauchy-uniform-strong Xp tb, X.makeCauchy)) tb, + \lam c Cu => \case c Cu \with { + | inP (U,Uu,h) => inP (U, X.makeCauchy Uu, h) + }, + \lam c Cc => totallyBounded-uniform-char.totallyBounded-closure c (uniform-cauchy.1 Cc) + ) + +\func IsLocallyUniform {X : UniformSpace} (C : Set (Set X)) (E : Set (Set X)) : \Prop + => ∀ {U : C} (isUniform \lam V => ∃ (W : E) (U ∧ V ⊆ W)) + +\func IsLocallyUniformSpace (X : UniformSpace) : \Prop + => ∃ (C : X.isUniform) ∀ {E : X.isCauchy} (IsLocallyUniform C E) + +\lemma locallyUniform-cauchy {X : UniformSpace} {C : Set (Set X)} (Cc : isCauchy C) (E : Set (Set X)) (lu : IsLocallyUniform C E) : isCauchy E + => cauchy-refine (cauchy-glue Cc {\lam U V => ∃ (W : E) (U ∧ V ⊆ W)} \lam CU => X.makeCauchy $ lu CU) (\lam {_} (inP (U, V, CU, inP (W,EW,p), idp)) => inP (W, EW, p)) + +\lemma locallyUniform-cover-char {X : StronglyRegularUniformSpace} {C : Set (Set X)} (Cb : ∀ {U : C} (IsTotallyBoundedSet U)) (Cp : ∀ {U : C} ∃ U) {E : Set (Set X)} (Ec : isCauchy E) : IsLocallyUniform C E + => \lam {U} CU => + \have Du => totallyBounded-cauchy-uniform-strong {StronglyRegularUniformTransfer {Set.Total U} __.1} (UniformSpace.inhabited_weaklyProper $ Cp CU) (Cb CU) (PrecoverTransfer.makeCauchy Ec) + \in uniform-subset Du \lam {V} (inP (_, inP (W,EW,idp), p)) => inP $ later (W, EW, \lam {x} (Ux,Vx) => p {x,Ux} Vx) + +\lemma locallyTotallyBounded-locallyUniform {X : StronglyRegularUniformSpace} (Xltb : X.isUniform IsTotallyBoundedSet) (Xd : X.IsProperUniform) : IsLocallyUniformSpace X + => inP (\lam U => \Sigma (IsTotallyBoundedSet U) (∃ U), Xd Xltb, locallyUniform-cover-char (later __.1) (later __.2)) + +\lemma metric-cover-char {X : PseudoMetricSpace} (Xbtb : \Pi {S : Set X} -> IsBoundedSet S -> IsTotallyBoundedSet S) : IsLocallyUniformSpace X + => locallyTotallyBounded-locallyUniform (uniform-subset (X.makeUniform (RealAbGroup.half>0 RealAbGroup.zro Xbtb $ inP (1, RealAbGroup.zro PseudoMetricSpace.halving)) X.properUniform + +\lemma locallyUniformMapFromCover {X Y : UniformSpace} (Xlu : IsLocallyUniformSpace X) (f : CoverMap X Y) : LocallyUniformMap X Y f \cowith + | func-locally-uniform Eu => \case Xlu \with { + | inP (C,Cu,h) => inP (C, Cu, \lam CU => uniform-subset (h (f.func-cover (Y.makeCauchy Eu)) CU) \lam {V} (inP (_, inP (W,EW,idp), p)) => inP $ later (W, EW, p)) + } \ No newline at end of file diff --git a/src/Topology/CoverSpace.ard b/src/Topology/CoverSpace.ard index 049f2405..d570cb6f 100644 --- a/src/Topology/CoverSpace.ard +++ b/src/Topology/CoverSpace.ard @@ -20,12 +20,12 @@ | cauchy-cover {C : Set (Set E)} : isCauchy C -> \Pi (x : E) -> ∃ (U : C) (U x) | cauchy-top : isCauchy (single top) | cauchy-refine {C D : Set (Set E)} : isCauchy C -> Refines C D -> isCauchy D - | cauchy-trans {C : Set (Set E)} : isCauchy C -> \Pi {D : Set E -> Set (Set E)} -> (\Pi {U : Set E} -> C U -> isCauchy (D U)) + | cauchy-glue {C : Set (Set E)} : isCauchy C -> \Pi {D : Set E -> Set (Set E)} -> (\Pi {U : Set E} -> C U -> isCauchy (D U)) -> isCauchy (\lam U => ∃ (V W : Set E) (C V) (D V W) (U = V ∧ W)) | cauchy-open {S : Set E} : isOpen S <-> ∀ {x : S} (isCauchy \lam U => U x -> U ⊆ S) \default open-top => cauchy-open.2 \lam _ => cauchy-refine cauchy-top \lam {U} _ => inP (U, \lam _ _ => (), <=-refl) - \default open-inter Uo Vo => cauchy-open.2 $ later \lam {x} (Ux,Vx) => cauchy-refine (cauchy-trans (cauchy-open.1 Uo Ux) (\lam _ => cauchy-open.1 Vo Vx)) + \default open-inter Uo Vo => cauchy-open.2 $ later \lam {x} (Ux,Vx) => cauchy-refine (cauchy-glue (cauchy-open.1 Uo Ux) (\lam _ => cauchy-open.1 Vo Vx)) \lam (inP (U',V',Uc,Vc,W=U'V')) => inP (U' ∧ V', \lam (U'x,V'x) {y} (U'y,V'y) => (Uc U'x U'y, Vc V'x V'y), Preorder.=_<= W=U'V') \default open-Union So => cauchy-open.2 $ later \lam {x} (inP (U,SU,Ux)) => cauchy-refine (cauchy-open.1 (So SU) Ux) \lam {V} Vc => inP (V, \lam Vx => Vc Vx <=∘ Set.Union-cond SU, <=-refl) @@ -34,7 +34,7 @@ \lemma cauchy-trans-dep {C : Set (Set E)} {D : \Pi {U : Set E} -> C U -> Set (Set E)} (Cc : isCauchy C) (Dc : \Pi {U : Set E} (c : C U) -> isCauchy (D c)) : isCauchy (\lam U => ∃ (V W : Set E) (c : C V) (D c W) (U = V ∧ W)) - => transport isCauchy (ext \lam U => ext (\lam (inP (V,W,CV,DW,p)) => inP (V, W, CV, transport (D __ W) prop-pi DW.2, p), \lam (inP (V,W,c,DW,p)) => inP (V, W, c, (c,DW), p))) $ cauchy-trans Cc {\lam U V => \Sigma (c : C U) (D c V)} \lam CU => transport isCauchy (ext \lam V => ext (\lam d => (CU,d), \lam s => transport (D __ V) prop-pi s.2)) (Dc CU) + => transport isCauchy (ext \lam U => ext (\lam (inP (V,W,CV,DW,p)) => inP (V, W, CV, transport (D __ W) prop-pi DW.2, p), \lam (inP (V,W,c,DW,p)) => inP (V, W, c, (c,DW), p))) $ cauchy-glue Cc {\lam U V => \Sigma (c : C U) (D c V)} \lam CU => transport isCauchy (ext \lam V => ext (\lam d => (CU,d), \lam s => transport (D __ V) prop-pi s.2)) (Dc CU) \lemma open-char {S : Set E} : TopSpace.isOpen S <-> ∀ {x : S} (single x <=< S) => (\lam So Sx => cauchy-subset (cauchy-open.1 So Sx) $ later \lam f (y,(p,q)) => f $ rewrite p q, @@ -44,7 +44,7 @@ \func HasDensePoints => \Pi {C : Set (Set E)} -> isCauchy C -> isCauchy \lam U => \Sigma (C U) (∃ U) - \func hasDensePoints_hasWeaklyDensePoints (d : HasDensePoints) : HasWeaklyDensePoints + \lemma hasDensePoints_hasWeaklyDensePoints (d : HasDensePoints) : HasWeaklyDensePoints => \lam Cc => cauchy-subset (d Cc) \case __ \with { | (byLeft e, inP (x,Ux)) => \case rewrite e in Ux \with { | inP ((),_) @@ -64,7 +64,7 @@ \lemma cauchy-inter {X : PrecoverSpace} {C D : Set (Set X)} (Cc : isCauchy C) (Dc : isCauchy D) : isCauchy (\lam U => ∃ (V W : Set X) (C V) (D W) (U = V ∧ W)) - => cauchy-trans Cc \lam _ => Dc + => cauchy-glue Cc \lam _ => Dc \lemma cauchy-array-inter {X : PrecoverSpace} (Cs : Array (Given X.isCauchy)) : isCauchy \lam V => ∃ (Us : Array (Set X) Cs.len) (\Pi (j : Fin Cs.len) -> (Cs j).1 (Us j)) (V = MeetSemilattice.Big_∧ (top :: Us)) \elim Cs | nil => top-cauchy $ inP $ later (nil, \case __ \with {}, idp) @@ -91,9 +91,9 @@ {- 3 -} Dom = {PrecoverSpace Dom} PrecoverTransfer func ) => TFAE.cycle ( \lam p f Cc => cauchy-refine (func-cover {f} $ p Cc) \lam (inP (V, inP (U',CU',p), q)) => inP (U', CU', rewrite q p), - \lam f => f PrecoverTransfer-map, + \lam f => f (PrecoverTransfer-map _), \lam f => PrecoverSpace.PrecoverSpace-ext {_} {Dom} {PrecoverTransfer func} \lam {C} => (f,PrecoverTransfer-char), - \lam p => unfolds $ rewrite p \lam (inP (D,Dc,f)) => cauchy-subset Dc f) + \lam p => unfolds $ rewrite p \lam Dc => Dc) \func IsDenseEmbedding : \Prop => \Sigma IsDense IsEmbedding @@ -111,6 +111,9 @@ | func-cover Dc => top-cauchy \case cauchy-cover Dc x \with { | inP (U,DU,Ux) => inP $ later (U, DU, ext \lam y => ext (\lam _ => Ux, \lam _ => ())) } + + \lemma id-denseEmbedding {X : PrecoverSpace} : IsDenseEmbedding {id {X}} + => (\lam {x} _ Ux => inP (x, inP (x, idp), Ux), \lam Cc => cauchy-subset Cc \lam {U} CU => inP $ later (U, CU, <=-refl)) } \type \infix 4 <=< {X : PrecoverSpace} (V U : Set X) : \Prop @@ -251,7 +254,7 @@ | cauchy-refine Ct e => \case e Ct \with { | inP (V,DV,t<=V) => rewrite (<=-antisymmetric t<=V top-univ) DV } - | cauchy-trans Ct e => inP (top, top, Ct, e Ct, <=-antisymmetric (\lam _ => ((), ())) top-univ) + | cauchy-glue Ct e => inP (top, top, Ct, e Ct, <=-antisymmetric (\lam _ => ((), ())) top-univ) | isCompletelyStronglyRegular Ct => inP (top, Ct, RatherBelow.Interpolative.<=<_top) \func DiscreteCover (X : \Set) : CompletelyRegularCoverSpace X \cowith @@ -262,7 +265,7 @@ \have | (inP (U,CU,Ux)) => c x | (inP (V,DV,U<=V)) => d CU \in inP (V, DV, U<=V Ux) - | cauchy-trans c d x => + | cauchy-glue c d x => \have | (inP (U,CU,Ux)) => c x | (inP (V,DV,Vx)) => d CU x \in inP (U ∧ V, inP (U, V, CU, DV, idp), (Ux,Vx)) @@ -271,44 +274,39 @@ } \func PrecoverTransfer {X : \Set} {Y : PrecoverSpace} (f : X -> Y) : PrecoverSpace X \cowith - | isCauchy C => ∃ (D : Set (Set Y)) (Y.isCauchy D) (\Pi {V : Set Y} -> D V -> ∃ (U : C) (f ^-1 V ⊆ U)) - | cauchy-cover (inP (D,Dc,d)) x => - \have | (inP (V,DV,Vfx)) => cauchy-cover Dc (f x) - | (inP (U,CU,p)) => d DV - \in inP (U, CU, p Vfx) - | cauchy-top => inP (single top, cauchy-top, \lam p => rewriteI p $ inP (top,idp,<=-refl)) - | cauchy-refine (inP (D,Dc,d)) e => inP (D, Dc, \lam DV => - \have | (inP (U,CU,p)) => d DV - | (inP (W,DW,q)) => e CU - \in inP (W, DW, p <=∘ q)) - | cauchy-trans {C} (inP (C',C'c,C'e)) {D} d => - \have t => cauchy-trans C'c {\lam c' V => ∃ (c : Set X) (C c) (f ^-1 c' <= c) (D' : Set (Set Y)) (isCauchy D') (\Pi {W : Set Y} -> D' W -> ∃ (U' : D c) (f ^-1 W ⊆ U')) (D' V)} \lam {V} C'V => - \have | (inP (U,CU,p)) => C'e C'V - | (inP (D',D'c,D'e)) => d CU - \in cauchy-subset D'c \lam {V} D'V => later $ inP (U,CU,p,D',D'c,D'e,D'V) - \in inP (_, t, \lam (inP (U, V, C'U, inP (c,Cc,q,D',D'c,D'e,D'V), W=UV)) => \case D'e D'V \with { - | inP (d,Dd,s) => inP (c ∧ d, inP (c, d, Cc, Dd, idp), rewrite W=UV \lam e => (q e.1, s e.2)) - }) - -\lemma PrecoverTransfer-map {X : \Set} {Y : PrecoverSpace} {f : X -> Y} : PrecoverMap (PrecoverTransfer f) Y f \cowith - | func-cover {D} Dc => inP (D, Dc, \lam {V} DV => inP (f ^-1 V, inP (V, DV, idp), <=-refl)) - -\lemma PrecoverTransfer-char {X Y : PrecoverSpace} {f : PrecoverMap X Y} {C : Set (Set X)} (c : isCauchy {PrecoverTransfer f} C) : X.isCauchy C \elim c - | inP (D,Dc,De) => cauchy-refine (f.func-cover Dc) \lam {U} (inP (V,DV,p)) => \case De DV \with { - | inP (U',CU',q) => inP (U', CU', rewrite p q) + | isCauchy C => Y.isCauchy \lam V => ∃ (U : C) (f ^-1 V ⊆ U) + | cauchy-cover Ec x => \case cauchy-cover Ec (f x) \with { + | inP (U, inP (V,CV,p), Ufx) => inP (V, CV, p Ufx) + } + | cauchy-top => top-cauchy $ inP $ later (top, idp, top-univ) + | cauchy-refine Ec r => cauchy-subset Ec \lam (inP (V,CV,p)) => \case r CV \with { + | inP (W,DW,V<=W) => inP $ later (W, DW, p <=∘ V<=W) + } + | cauchy-glue {C} Ec {D} Fc => cauchy-subset (cauchy-glue Ec {\lam U V => ∃ (U' : C) (f ^-1 U ⊆ U') (V' : D U') (f ^-1 V ⊆ V')} + \lam (inP (U',CU',p)) => cauchy-subset (Fc CU') \lam {V} (inP (V',DU'V',q)) => inP $ later (U', CU', p, V', DU'V', q)) + \lam {_} (inP (U, V, _, inP (U',CU',p,V',DU'V',q), idp)) => inP $ later (_, inP (U', V', CU', DU'V', idp), MeetSemilattice.meet-monotone p q) + \where { + \lemma makeCauchy {C : Set (Set Y)} (Cc : isCauchy C) : isCauchy {PrecoverTransfer f} \lam U => ∃ (V : C) (U = f ^-1 V) + => cauchy-subset Cc \lam {V} CV => inP $ later (f ^-1 V, inP (V, CV, idp), <=-refl) } +\lemma PrecoverTransfer-map {X : \Set} {Y : PrecoverSpace} (f : X -> Y) : PrecoverMap (PrecoverTransfer f) Y f \cowith + | func-cover Dc => cauchy-subset Dc \lam DU => inP $ later (_, inP (_, DU, idp), <=-refl) + +\lemma PrecoverTransfer-char {X Y : PrecoverSpace} {f : PrecoverMap X Y} {C : Set (Set X)} (Dc : isCauchy {PrecoverTransfer f} C) : X.isCauchy C + => cauchy-refine (f.func-cover Dc) \lam {_} (inP (V,r,idp)) => r + \func ClosurePrecoverSpace {X : \Set} (A : Set (Set X) -> \Prop) (CA : \Pi {C : Set (Set X)} -> A C -> \Pi (x : X) -> ∃ (U : C) (U x)) : PrecoverSpace X \cowith | isCauchy => Closure A | cauchy-cover CC x => closure-filter (pointFilter x) (\lam AC => CA AC x) CC | cauchy-top => closure-top idp | cauchy-refine => closure-refine - | cauchy-trans => closure-trans __ __ idp + | cauchy-glue => closure-trans __ __ idp \where { \truncated \data Closure {X : \Set} (A : Set (Set X) -> \Prop) (C : Set (Set X)) : \Prop | closure (A C) | closure-top (C = single top) - | closure-refine {D : Set (Set X)} (Closure A D) (\Pi {U : Set X} -> D U -> ∃ (V : Set X) (C V) (U ⊆ V)) + | closure-refine {D : Set (Set X)} (Closure A D) (Refines D C) | closure-trans {D : Set (Set X)} (Closure A D) {E : \Pi (U : Set X) -> Set (Set X)} (\Pi {U : Set X} -> D U -> Closure A (E U)) (C = \lam U => ∃ (V W : Set X) (D V) (E V W) (U = V ∧ W)) @@ -342,7 +340,7 @@ | closure-top p => cauchy-subset cauchy-top \lam q => inP $ later (top, rewrite p idp, inv q) | closure-refine Cc g => cauchy-refine (closure-univ-cover Ap Cc) \lam (inP (V,CV,q)) => TruncP.map (g CV) \lam (V',CV',V<=V') => (f ^-1 V', inP (V', CV', idp), rewrite q \lam c => V<=V' c) | closure-trans {D} Cc {E} g p => - \have t => cauchy-trans (closure-univ-cover Ap Cc) {\lam V V' => ∃ (U : Set X) (V = f ^-1 U) (D U) (U' : Set X) (E U U') (V' = f ^-1 U')} + \have t => cauchy-glue (closure-univ-cover Ap Cc) {\lam V V' => ∃ (U : Set X) (V = f ^-1 U) (D U) (U' : Set X) (E U U') (V' = f ^-1 U')} \lam (inP (V,DV,q)) => cauchy-subset (closure-univ-cover Ap (g DV)) \lam (inP (V',EVV',r)) => inP $ later (V, q, DV, V', EVV', r) \in cauchy-subset t \lam (inP (W, W', _, inP (V2,p2,DV2,V2',EV2V2',p2'), U=WW')) => inP $ later $ rewrite p (_, inP (V2, V2', DV2, EV2V2', idp), U=WW' *> pmap2 (∧) p2 p2') @@ -387,7 +385,7 @@ | closure-top q => top-cauchy $ inP $ later (top, rewrite q idp, top-univ) | closure-refine CD g => cauchy-subset (aux CD) \lam (inP (V,DV,q)) => TruncP.map (g DV) \lam (V',CV',V<=V') => later (V', CV', q <=∘ V<=V') | closure-trans {D} CD {E} g q => - \let t => cauchy-trans (aux CD) {\lam V V' => ∃ (U U' : Set X) (D U) (f ^-1 V ⊆ U) (f ^-1 V' ⊆ U') (E U U')} \lam (inP (U,DU,r)) => cauchy-subset (aux (g DU)) \lam (inP (U',EUU',r')) => inP $ later (U, U', DU, r, r', EUU') + \let t => cauchy-glue (aux CD) {\lam V V' => ∃ (U U' : Set X) (D U) (f ^-1 V ⊆ U) (f ^-1 V' ⊆ U') (E U U')} \lam (inP (U,DU,r)) => cauchy-subset (aux (g DU)) \lam (inP (U',EUU',r')) => inP $ later (U, U', DU, r, r', EUU') \in cauchy-subset t \lam (inP (V, W, _, inP (U1,U2,DU1,r,r',EU1U2), s)) => inP $ later (U1 ∧ U2, rewrite q $ inP (U1, U2, DU1, EU1U2, idp), rewrite s $ MeetSemilattice.meet-monotone r r') } } @@ -409,10 +407,18 @@ } \func CoverTransfer {X : \Set} {Y : CoverSpace} (f : X -> Y) : CoverSpace X \cowith - | PrecoverSpace => PrecoverTransfer f - | isRegular (inP (D,Dc,De)) => inP (_, Y.isRegular Dc, \lam {V} (inP (U,DU,V<= inP (f ^-1 V, \case De DU \with { - | inP (U',CU',p) => inP (U', CU', <=<-left (later $ inP (_, V<= inP (f ^-1 W, \lam (x,s) {_} => g (f x, s), <=-refl))) p) - }, <=-refl)) + | TopSpace => TopTransfer f + | isCauchy => isCauchy {PrecoverTransfer f} + | cauchy-cover => cauchy-cover {PrecoverTransfer f} + | cauchy-top => cauchy-top {PrecoverTransfer f} + | cauchy-refine => cauchy-refine {PrecoverTransfer f} + | cauchy-glue => cauchy-glue {PrecoverTransfer f} + | isRegular Dc => cauchy-subset (isRegular Dc) \lam {V} (inP (U, inP (W,CW,p), V<= inP $ later + (_, inP (W, CW, <=<-left (cauchy-subset (unfolds in V<= inP $ later (_, \lam (x,s) {_} => g (f x, s), <=-refl)) p), <=-refl) + | cauchy-open {S} => (\lam (inP (V,Vo,p)) Sx => cauchy-subset (cauchy-open.1 Vo $ rewrite p in Sx) \lam {W} g => inP $ later (f ^-1 W, \lam Wfx {y} Wfy => rewrite p $ g Wfx Wfy, <=-refl), + \lam c => inP (Union \lam V' => \Sigma (isOpen V') (f ^-1 V' ⊆ S), open-Union __.1, <=-antisymmetric (\lam {x} Sx => \case Y.cauchy-regular-cover (c Sx) (f x) \with { + | inP (V, inP (U,g,p), fx<= inP (_, (Y.interior {V}, \lam {x'} fx'<= g (p $ <=<_<= fx<= p Vfx)) \func ClosureCoverSpace {X : \Set} (A : Set (Set X) -> \Prop) (CA : \Pi {C : Set (Set X)} -> A C -> \Pi (x : X) -> ∃ (U : C) (U x)) @@ -474,11 +480,6 @@ } } -\func UniformlyCoverSpace {X : PrecoverSpace} (AI : \Pi {C : Set (Set X)} -> X.isCauchy C -> ∃ (D : X.isCauchy) ∀ {V : D} ∃ (U : C) ∀ {V' : D} (Given (V ∧ V') -> V' ⊆ U)) : CompletelyRegularCoverSpace X \cowith - | PrecoverSpace => X - | isCompletelyRegular {C} => transport (\lam (S : PrecoverSpace X) => S.isCauchy C -> S.isCauchy \lam V => ∃ (U : C) (V RatherBelow.<= (closure-cauchy \lam c => c, closure)) $ isCompletelyRegular {ClosureRegularCoverSpace X.isCauchy X.cauchy-cover AI} - \instance CoverLattice (X : \Set) : CompleteLattice (CoverSpace X) | <= A B => \Pi {C : Set (Set X)} -> isCauchy {A} C -> isCauchy {B} C | <=-refl c => c @@ -514,5 +515,4 @@ transport (isCauchy {RegPrecoverSpace X}) (ext \lam U => ext (\lam DU => inP (U, DU, idp), \lam (inP (V,DV,U=V)) => rewrite U=V DV)) d \lemma regPrecoverSpace-extend {X : PrecoverSpace} {Y : CoverSpace} (f : PrecoverMap X Y) : PrecoverMap (RegPrecoverSpace X) Y f \cowith - | func-cover {D} Dc => CompleteLattice.SJoin-cond {CoverLattice X} {\lam A => A <= {PrecoverLattice X} X} {CoverTransfer f} PrecoverTransfer-char $ - inP (D, Dc, \lam {V} DV => inP (f ^-1 V, inP (V, DV, idp), <=-refl)) \ No newline at end of file + | func-cover {D} Dc => CompleteLattice.SJoin-cond {CoverLattice X} {\lam A => A <= {PrecoverLattice X} X} {CoverTransfer f} PrecoverTransfer-char $ func-cover {PrecoverTransfer-map f} Dc \ No newline at end of file diff --git a/src/Topology/CoverSpace/Complete.ard b/src/Topology/CoverSpace/Complete.ard index 14cb22c1..952b8f88 100644 --- a/src/Topology/CoverSpace/Complete.ard +++ b/src/Topology/CoverSpace/Complete.ard @@ -64,6 +64,9 @@ \lemma closure-univ {X : \Set} {A : Set (Set X) -> \Prop} {S : CoverSpace X} {Y : CoverSpace} (AS : \Pi {C : Set (Set X)} -> isCauchy C -> ClosurePrecoverSpace.Closure A C) (f : Y -> X) (Ap : ∀ {C : A} (isCauchy \lam U => ∃ (V : Set X) (C V) (U = f ^-1 V))) : CoverMap Y S f \cowith | func-cover Cc => ClosurePrecoverSpace.closure-univ-cover Ap (AS Cc) + + \lemma id-denseEmbedding {X : CoverSpace} : IsDenseEmbedding {id {X}} + => PrecoverMap.id-denseEmbedding } \instance CauchyFilterPoset (S : CoverSpace) : Poset (CauchyFilter S) @@ -275,7 +278,7 @@ | inP (V'',y<= inP $ later (V'', V, rewrite p in q, V''<= isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char 4 7 $ later \case CompleteCoverSpace.filter-point-sub __ \with { | inP (V',V,p,V'<= p $ <=<_<= V'<= inP (W', W'<= isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char 0 7 \lam {U} c => \case (dense-lift-neighborhood fd (Y.filter-point $ f.func-cauchy F) _).1 c \with { + | inP (U',U'<= filter-point-elem U'<= ∃ (y : Y) (pointCF y ⊆ f.func-cauchy F)) : IsCompleteCoverSpace Y => \lam F => \case p $ regCF $ dense-filter-lift f fd F \with { | inP (y,q) => inP (y, RegularCauchyFilter.Reg_CF~_<= {_} {pointCF y} $ ~-transitive {_} {pointCF y} (CF~_<= {_} {pointCF y} $ q <=∘ func-cauchy_<= (regCF $ dense-filter-lift f fd F) (dense-filter-lift f fd F) \lam u => u <=-refl) $ dense-filter-lift.map-equiv fd) } -\instance Completion (S : CoverSpace) : CompleteCoverSpace (RegularCauchyFilter S) +\instance Completion (X : CoverSpace) : CompleteCoverSpace (RegularCauchyFilter X) | CoverSpace => coverSpace - | isSeparatedCoverSpace p => RegularCauchyFilter.equality \lam Cc => \case p (mkCover Cc) \with { + | isSeparatedCoverSpace p => RegularCauchyFilter.equality \lam Cc => \case p (makeCover Cc) \with { | inP (_, inP (U,CU,idp), r) => inP (U,CU,r) } | isComplete => dense-complete completion.isDenseEmbedding \lam F => inP (F, completion.dense-aux {_} {F} __) \where { - \func mkSet (U : Set S) : Set (RegularCauchyFilter S) + \func mkSet (U : Set X) : Set (RegularCauchyFilter X) => \lam F => F U - \lemma mkSet_<= {U V : Set S} (p : U ⊆ V) : mkSet U ⊆ mkSet V + \lemma mkSet_<= {U V : Set X} (p : U ⊆ V) : mkSet U ⊆ mkSet V => \lam {F} => filter-mono p - \func isCCauchy (D : Set (Set (RegularCauchyFilter S))) - => ∃ (C : S.isCauchy) (∀ {U : C} ∃ (V : D) (mkSet U ⊆ V)) + \lemma mkSet-open {U : Set X} (Uo : isOpen U) : isOpen {Completion X} (mkSet U) + => (PrecoverSpace.open-char {Completion X}).2 $ \lam {F} FU => \case isRegularFilter FU \with { + | inP (V,V<= inP (_, V<= inP (mkSet W, \lam (_,(idp,FW)) => mkSet_<= \case isProper (filter-meet FV FW) \with { + | inP s => g s + }, <=-refl)) + } + + \lemma pointCF_^-1_<=< {F : RegularCauchyFilter X} {U : Set (RegularCauchyFilter X)} (p : single F <=< {Completion X} U) : F (pointCF ^-1 U) \elim p + | inP (C,Cc,h) => \case F.isCauchyFilter (isRegular Cc) \with { + | inP (U', inP (U,CU,U'<= \case h CU \with { + | inP (V,g,q) => filter-mono (\lam U'x => g (F, (idp, q $ filter-mono (<=<_<= U'<= F U + => (\lam p => filter-mono (<=<_<= __ idp) (pointCF_^-1_<=< p), \lam FU => \case isRegularFilter FU \with { + | inP (V,V<= inP (_, V<= inP (mkSet W, \lam (_,(idp,FW)) => mkSet_<= $ \case isProper (filter-meet FV FW) \with { + | inP s => g s + }, <=-refl)) + }) + + \func isCCauchy (D : Set (Set (RegularCauchyFilter X))) + => ∃ (C : X.isCauchy) (∀ {U : C} ∃ (V : D) (mkSet U ⊆ V)) - \lemma mkCover {C : Set (Set S)} (Cc : isCauchy C) : isCCauchy \lam V => ∃ (U : C) (V = mkSet U) + \lemma makeCover {C : Set (Set X)} (Cc : isCauchy C) : isCCauchy \lam V => ∃ (U : C) (V = mkSet U) => inP (C, Cc, \lam {U} CU => inP (mkSet U, inP (U,CU,idp), <=-refl)) - \func coverSpace : CoverSpace (RegularCauchyFilter S) \cowith + \func coverSpace : CoverSpace (RegularCauchyFilter X) \cowith | isCauchy => isCCauchy | cauchy-cover {D} (inP (C,Cc,p)) F => \have | (inP (U,CU,FU)) => isCauchyFilter Cc @@ -322,14 +354,14 @@ \have | (inP (V,CV,p)) => g EU | (inP (W,DW,q)) => f CV \in inP (W, DW, p <=∘ q)) - | cauchy-trans {C} (inP (C',C'c,f)) {D} Dc => inP (_, cauchy-trans C'c {\lam U' V' => ∃ (U : C) (V : D U) (mkSet U' ⊆ U) (mkSet V' ⊆ V)} \lam {U'} C'U' => + | cauchy-glue {C} (inP (C',C'c,f)) {D} Dc => inP (_, cauchy-glue C'c {\lam U' V' => ∃ (U : C) (V : D U) (mkSet U' ⊆ U) (mkSet V' ⊆ V)} \lam {U'} C'U' => \have | (inP (U,CU,U'<=U)) => f C'U' | (inP (D',D'c,g)) => Dc CU \in cauchy-refine D'c \lam {V'} D'V' => \case g D'V' \with { | inP (V,DV,V'<=V) => inP (V', inP (U, CU, V, DV, U'<=U, V'<=V), <=-refl) }, \lam {W'} (inP (U', V', C'U', inP (U, CU, V, DV, U'<=U, V'<=V), W'=U'V')) => inP (U ∧ V, inP (U, V, CU, DV, idp), rewrite W'=U'V' \lam {F} FU'V' => (U'<=U $ filter-mono meet-left FU'V', V'<=V $ filter-mono meet-right FU'V'))) | isRegular {D} (inP (C,Cc,f)) => - \have <=<_mkFilters {U' U : Set S} (p : U' <=< U) : mkSet U' <=< mkSet U + \have <=<_mkFilters {U' U : Set X} (p : U' <=< U) : mkSet U' <=< mkSet U => unfolds $ inP (_, p, \lam {W} g => inP (mkSet W, \lam (F,(FU',FW)) => \case isProper (filter-meet FU' FW) \with { | inP s => mkSet_<= (g s) }, <=-refl)) @@ -361,11 +393,21 @@ => dense-lift completion completion.isDenseEmbedding g \lemma completion-lift-char {X : CoverSpace} {Z : CompleteCoverSpace} {g : CoverMap X Z} (x : X) : completion-lift g (pointCF x) = g x - => dense-lift-char {_} {_} {_} {completion} {completion.isDenseEmbedding} x + => dense-lift-char completion.isDenseEmbedding x \lemma completion-lift-unique {X : CoverSpace} {Z : SeparatedCoverSpace} (g h : PrecoverMap (Completion X) Z) (p : \Pi (x : X) -> g (pointCF x) = h (pointCF x)) (y : Completion X) : g y = h y => dense-lift-unique completion completion.isDenseEmbedding.1 g h p y +\lemma completion-lift-neighborhood {X : CoverSpace} {Z : CompleteCoverSpace} (g : CoverMap X Z) (y : Completion X) (W : Set Z) + : single (completion-lift g y) <=< W <-> ∃ (W' : Set Z) (W' <=< W) (V : Set X) (y V) (V ⊆ g ^-1 W') + => <->trans (dense-lift-neighborhood completion.isDenseEmbedding y W) $ later + (\lam (inP (W',W'<= inP (W', W'<= inP (W', W'<= <=<_<= x<= dense-lift-natural completion.isDenseEmbedding F + \lemma complete-char {X : CoverSpace} : TFAE ( {- 0 -} CompleteCoverSpace { | CoverSpace => X }, {- 1 -} ∃ (g : PrecoverMap (Completion X) X) (\Pi (x : X) -> g (pointCF x) = x), @@ -393,4 +435,11 @@ | isSeparatedCoverSpace c => fi $ isSeparatedCoverSpace \lam Cc => \case c (func-cover Cc) \with { | inP (U, inP (V,CV,p), (Ux,Uy)) => inP (V, CV, (rewrite p in Ux, rewrite p in Uy)) } - }) \ No newline at end of file + }) + +\func regPrecoverCauchyFilter {X : PrecoverSpace} (F : ProperFilter X) (Fc : ∀ {C : isCauchy} ∃ (U : C) (F U)) : CauchyFilter (RegPrecoverSpace X) \cowith + | ProperFilter => F + | isCauchyFilter Cc => ClosurePrecoverSpace.closure-filter F (\lam (inP ((A,A<=X),CAc)) => Fc $ A<=X CAc) Cc + +\lemma regPrecoverSpace-extend-coverMap {X : PrecoverSpace} {Y : CoverSpace} (f : PrecoverMap X Y) : CoverMap (RegPrecoverSpace X) Y f \cowith + | PrecoverMap => regPrecoverSpace-extend f \ No newline at end of file diff --git a/src/Topology/CoverSpace/Convergence.ard b/src/Topology/CoverSpace/Convergence.ard deleted file mode 100644 index c6afdbdd..00000000 --- a/src/Topology/CoverSpace/Convergence.ard +++ /dev/null @@ -1,133 +0,0 @@ -\import Algebra.Meta -\import Arith.Nat -\import Data.Or -\import Function.Meta -\import Logic -\import Logic.Meta -\import Meta -\import Operations -\import Order.Lattice -\import Order.LinearOrder -\import Order.PartialOrder -\import Order.StrictOrder -\import Paths -\import Paths.Meta -\import Set.Subset -\import Topology.CoverSpace -\import Topology.CoverSpace.Complete -\import Topology.CoverSpace.Product -\open Bounded(top) -\open Set - -\instance NatCoverSpace : CompletelyRegularCoverSpace Nat - => UniformlyCoverSpace { - \new PrecoverSpace Nat { - | isCauchy => Cover - | cauchy-cover (inP (U,CU,N,f,g)) n => \case LinearOrder.dec<_<= n N \with { - | inl n g n inP (U, CU, f N<=n) - } - | cauchy-top => inP (top, idp, 0, \lam _ => (), \case __) - | cauchy-refine (inP (U,CU,N,f,g)) e => \case e CU \with { - | inP (V,DV,U<=V) => inP (V, DV, N, \lam N<=n => U<=V $ f N<=n, \lam n \case g n \case e CU' \with { - | inP (V',DV',U'<=V') => inP (V', DV', U'<=V' U'n) - } - }) - } - | cauchy-trans {C} (inP (U,CU,N,f,g)) e => \case e CU \with { - | inP (V,DUV,N',f',g') => inP (U ∧ V, inP (U, V, CU, DUV, idp), N ∨ N', \lam p => (f $ join-left <=∘ p, f' $ join-right <=∘ p), \lam {n} _ => - \have (inP (U',CU',U'n)) : ∃ (U' : C) (U' n) => \case LinearOrder.dec<_<= n N \with { - | inl p => g p - | inr p => inP (U, CU, f p) - } - \in \case e CU' \with { - | inP (V',DU'V',N',f',g') => \case LinearOrder.dec<_<= n N' \with { - | inl p => TruncP.map (g' p) \lam (V'',DU'V'',V''n) => (U' ∧ V'', inP (U', V'', CU', DU'V'', idp), (U'n, V''n)) - | inr p => inP (U' ∧ V', inP (U', V', CU', DU'V', idp), (U'n, f' p)) - } - }) - } - } - } \lam (inP (U,CU,N,f,g)) => inP (_, makeCover N, \lam {V} => \case __ \with { - | byLeft p => inP (U, CU, \case __ \with { - | byLeft q => \lam _ => rewrite q \lam N<=x => f N<=x - | byRight (n,n rewrite (p,q) \lam (x,(p',q')) => absurd linarith - }) - | byRight (n,n \case g n inP (U', CU', \case __ \with { - | byLeft q => rewrite (p,q) \lam (x,(p',q')) => absurd linarith - | byRight (n',n' rewrite (p,q) \lam (x,(p',q')) => rewrite (q', inv p') (single_<= U'n) - }) - } - }) -\where { - \func Cover (C : Set (Set Nat)) : \Prop - => ∃ (U : C) (N : Nat) (\Pi {n : Nat} -> N <= n -> U n) (\Pi {n : Nat} -> n < N -> ∃ (V : C) (V n)) - - \lemma makeCover (N : Nat) : Cover \lam U => (U = (N <=)) || (\Sigma (n : Nat) (n < N) (U = single n)) - => inP (N <=, byLeft idp, N, \lam p => p, \lam {n} p => inP (single n, byRight (n, p, idp), idp)) - - \func atTop : CauchyFilter NatCoverSpace \cowith - | F U => ∃ (N : Nat) ∀ {n} (N <= n -> U n) - | filter-mono p (inP (N,f)) => inP (N, \lam q => p $ f q) - | filter-top => inP (0, \lam _ => ()) - | filter-meet (inP (N,f)) (inP (M,g)) => inP (N ∨ M, \lam p => (f $ join-left <=∘ p, g $ join-right <=∘ p)) - | isProper (inP (N,f)) => inP (N, f <=-refl) - | isCauchyFilter (inP (U,CU,N,f,g)) => inP (U, CU, inP (N, f)) -} - -\func IsConvergent {X : PrecoverSpace} (f : Nat -> X) : \Prop - => PrecoverMap NatCoverSpace X f - -\lemma convergent-char {X : PrecoverSpace} {f : Nat -> X} (p : ∀ {C : X.isCauchy} ∃ (U : C) (N : Nat) ∀ {n} (N <= n -> U (f n))) : IsConvergent f \cowith - | func-cover Dc => \case p Dc \with { - | inP (U,DU,N,g) => inP (_, inP (U, DU, idp), N, g, \lam {n} _ => \case cauchy-cover Dc (f n) \with { - | inP (V,DV,Vfn) => inP (_, inP (V, DV, idp), Vfn) - }) - } - \where - \protected \lemma conv {X : PrecoverSpace} {f : Nat -> X} (fc : IsConvergent f) : ∀ {C : X.isCauchy} ∃ (U : C) (N : Nat) ∀ {n} (N <= n -> U (f n)) - => \case fc.func-cover __ \with { - | inP (U, inP (V,CV,p), N, f, g) => inP (V, CV, N, \lam q => rewrite p in f q) - } - -\func seqLimit {X : CompleteCoverSpace} (f : CoverMap NatCoverSpace X) : X - => X.filter-point $ f.func-cauchy NatCoverSpace.atTop - -\func IsUniFuncConvergent {X : \Set} {Y : PrecoverSpace} (f : Nat -> X -> Y) : \Prop - => ∀ {D : Y.isCauchy} ∃ (V : D) (N : Nat) ∀ {n} {x} (N <= n -> V (f n x)) - -\func IsFuncConvergent {X Y : CoverSpace} (f : Nat -> X -> Y) : \Prop - => CoverMap (NatCoverSpace ⨯ X) Y \lam s => f s.1 s.2 - -\lemma funcCovergent-cover {X Y : CoverSpace} (f : Nat -> PrecoverMap X Y) - (fc : ∀ {D : Y.isCauchy} (X.isCauchy \lam U => ∃ (N : Nat) (V : D) ∀ {n} {x} (N <= n -> U x -> V (f n x)))) - : IsFuncConvergent (\lam n => f n) - => generalized (f __) \lam Dc => cauchy-subset (fc Dc) \lam (inP (N,V,DV,h)) => inP $ later (N, V, DV, h, \lam {n} _ => func-cover {f n} Dc) - \where - -- | A slightly more general version of the lemma - \lemma generalized {X Y : CoverSpace} (f : Nat -> X -> Y) (fc : ∀ {D : Y.isCauchy} (X.isCauchy \lam U => ∃ (N : Nat) (V : D) (\Pi {n : Nat} {x : X} -> N <= n -> U x -> V (f n x)) (\Pi {n : Nat} -> n < N -> X.isCauchy \lam U => ∃ (V : D) (U = f n ^-1 V)))) : IsFuncConvergent f \cowith - | func-cover {D} Dc => - \have t => cauchy-trans {ProductCoverSpace NatCoverSpace X} (ProductCoverSpace.prodCover cauchy-top (fc Dc)) - {\lam U V => ∃ (U' : Set X) (N : Nat) (W : D) (\Pi {n : Nat} {x : X} -> N <= n -> U' x -> W (f n x)) (\Pi {n : Nat} -> n < N -> X.isCauchy \lam U => ∃ (V : D) (U = f n ^-1 V)) (U = (\lam s => s.2) ^-1 U') ((V = (\lam s => s.1) ^-1 (N <=)) || Given (n : Nat) (n < N) (V' : D) ∀ {s : V} (V' (f s.1 s.2)))} - \lam {W} => \case __ \with { - | inP (_, idp, V, inP (N,V',DV',g,h), p) => cauchy-refine {ProductCoverSpace NatCoverSpace X} (ProductCoverSpace.prodCover (later $ NatCoverSpace.makeCover N) $ cauchy-array-inter \new Array _ N \lam j => later (_, h $ fin_< j)) \lam {W'} => later \case __ \with { - | inP (U1, byLeft q, V1, inP (Us,Ush,Usp), q1) => inP (_, inP (V, N, V', DV', g, h, p *> ext \lam s => ext (__.2, \lam c => ((),c)), byLeft idp), rewrite (q1,q) __.1) - | inP (U1, byRight (n,n \case Ush (toFin n n inP (W', inP (V, N, V', DV', g, h, p *> ext \lam s => ext (__.2, \lam c => ((),c)), byRight (n, n rewriteI c $ rewrite (p'',toFin=id) in MeetSemilattice.Big_meet-cond {_} {_} {top :: Us} {suc (toFin n n hiding t \case __ \with { - | inP (U, V, _, inP (U', N, V', DV', g, h, q1, byLeft q2), p) => inP (_, inP (V',DV',idp), rewrite (p,q1,q2) \lam (c,d) => g d c) - | inP (U, V, _, inP (U', N, _, _, g, h, q1, byRight (n,n inP (_, inP (V', DV', idp), rewrite (p,q1) \lam s => q2 s.2) - } - -\lemma funcCovergent-uni {X Y : CoverSpace} (f : Nat -> PrecoverMap X Y) (fc : IsUniFuncConvergent \lam n => f n) : IsFuncConvergent \lam n => f n - => funcCovergent-cover f \lam Dc => \case fc Dc \with { - | inP (V,DV,N,h) => top-cauchy $ inP $ later (N, V, DV, \lam p _ => h p) - } - -\func seqFuncLimit {X : CoverSpace} {Y : CompleteCoverSpace} (f : Nat -> X -> Y) (fc : IsFuncConvergent f) (x : X) : Y - => Y.filter-point $ fc.func-cauchy $ prodCF NatCoverSpace.atTop (pointCF x) \ No newline at end of file diff --git a/src/Topology/CoverSpace/Directed.ard b/src/Topology/CoverSpace/Directed.ard new file mode 100644 index 00000000..a94980e0 --- /dev/null +++ b/src/Topology/CoverSpace/Directed.ard @@ -0,0 +1,115 @@ +\import Data.Bool +\import Function.Meta +\import Logic +\import Logic.Meta +\import Meta +\import Operations +\import Order.Directed +\import Order.Lattice +\import Order.PartialOrder +\import Paths.Meta +\import Set.Filter +\import Set.Subset +\import Topology.CoverSpace +\import Topology.CoverSpace.Complete +\import Topology.CoverSpace.Product +\open Bounded(top,top-univ) + +\func DirectedCoverSpace (I : DirectedSet) : CoverSpace I + => RegPrecoverSpace precover + \where { + \func precover : PrecoverSpace I \cowith + | isCauchy C => \Sigma (∃ (U : C) (N : I) (\Pi {n : I} -> N <= n -> U n)) (\Pi (n : I) -> ∃ (V : C) (V n)) + | cauchy-cover => __.2 + | cauchy-top => \case I.isInhabitted \with { + | inP n => (inP (top, idp, n, \lam _ => ()), \lam n => inP (top, idp, ())) + } + | cauchy-refine Cc C \case Cc.1 \with { + | inP (U,CU,N,g) => (\case C inP (V, DV, N, \lam p => U<=V (g p)) + }, \lam n => \case Cc.2 n \with { + | inP (V,CV,Vn) => \case C inP (W, DW, V<=W Vn) + } + }) + } + | cauchy-glue Cc Dc => (\case Cc.1 \with { + | inP (U,CU,N,g) => \case (Dc CU).1 \with { + | inP (V,DUV,M,h) => \case isDirected N M \with { + | inP (L,N<=L,M<=L) => inP (U ∧ V, inP (U, V, CU, DUV, idp), L, \lam L<=n => (g $ N<=L <=∘ L<=n, h $ M<=L <=∘ L<=n)) + } + } + }, \lam n => \case Cc.2 n \with { + | inP (U,CU,Un) => \case (Dc CU).2 n \with { + | inP (V,DUV,Vn) => inP (U ∧ V, inP (U, V, CU, DUV, idp), (Un, Vn)) + } + }) + + \lemma makePrecover (N : I) : precover.isCauchy \lam V => (V = \lam n => N <= n) || Given (n : I) (V = single n) + => (inP (_, byLeft idp, N, \lam p => p), \lam n => inP (single n, byRight (n, idp), idp)) + } + +\func EventualityFilter {I : DirectedSet} : CauchyFilter (DirectedCoverSpace I) + => regPrecoverCauchyFilter (\new ProperFilter { + | F U => ∃ (N : I) ∀ {n} (N <= n -> U n) + | filter-mono p (inP (N,f)) => inP (N, \lam q => p $ f q) + | filter-top => \case I.isInhabitted \with { + | inP x => inP (x, \lam _ => ()) + } + | filter-meet (inP (N,f)) (inP (M,g)) => \case isDirected N M \with { + | inP (L,N<=L,M<=L) => inP (L, \lam p => (f $ N<=L <=∘ p, g $ M<=L <=∘ p)) + } + | isProper (inP (N,f)) => inP (N, f <=-refl) + }) $ later \lam (inP (U,CU,N,g), _) => inP (U, CU, inP (N, g)) + +\func DirectProdCover {I : DirectedSet} {X : CoverSpace} (D : Set (Set (\Sigma I X))) : \Prop + => \Sigma (X.isCauchy \lam U => ∃ (N : I) (V : D) (\Pi {n : I} {x : X} -> N <= n -> U x -> V (n,x))) (\Pi (n : I) -> X.isCauchy \lam U => ∃ (V : D) ∀ {x : U} (V (n,x))) + \where { + \protected \func Space : PrecoverSpace (\Sigma I X) \cowith + | isCauchy => DirectProdCover + | cauchy-cover Cc s => \case cauchy-cover (Cc.2 s.1) s.2 \with { + | inP (U, inP (V,CV,h), Ux) => inP (V, CV, h Ux) + } + | cauchy-top => (top-cauchy \case I.isInhabitted \with { + | inP N => inP $ later (N, top, idp, \lam _ _ => ()) + }, \lam n => top-cauchy $ inP $ later (top, idp, \lam _ => ())) + | cauchy-refine Cc C (cauchy-subset Cc.1 \lam (inP (N,V,CV,p)) => \case C inP $ later (N, V', DV', \lam N<=n Ux => V<=V' $ p N<=n Ux) + }, \lam n => cauchy-subset (Cc.2 n) \lam (inP (V,CV,h)) => \case C inP $ later (V', DV', \lam Ux => V<=V' (h Ux)) + }) + | cauchy-glue {C} Cc {D} Dc => + (cauchy-subset (cauchy-glue Cc.1 {\lam U V => ∃ (U' : C) (N : I) (Set.Prod (N <=) U ⊆ U') (V' : D U') (Set.Prod (N <=) V ⊆ V')} + \lam (inP (N,U',CU',Uh)) => cauchy-subset (Dc CU').1 \lam {V} (inP (M,V',DU'V',Vh)) => \case isDirected N M \with { + | inP (L,L<=N,L<=M) => inP $ later (U', CU', L, \lam (p1,p2) => Uh (L<=N <=∘ p1) p2, V', DU'V', \lam (p1,p2) => Vh (L<=M <=∘ p1) p2) + }) + \lam {_} (inP (U, V, _, inP (U',CU',N,Uh,V',DU'V',Vh), idp)) => inP $ later (N, U' ∧ V', inP (U', V', CU', DU'V', idp), \lam p1 p2 => (Uh (p1,p2.1), Vh (p1,p2.2))), + \lam n => cauchy-subset (cauchy-glue (Cc.2 n) {\lam U V => ∃ (U' : C) (V' : D U') (∀ {x : U} (U' (n,x))) (∀ {x : V} (V' (n,x)))} + \lam (inP (U',CU',Uh)) => cauchy-subset ((Dc CU').2 n) \lam {V} (inP (V',DU'V',Vh)) => inP $ later (U', CU', V', DU'V', Uh, Vh)) + (\lam {_} (inP (U, V, _, inP (U',CU',V',DU'V',Uh,Vh), idp)) => inP $ later (U' ∧ V', inP (U', V', CU', DU'V', idp), \lam (p1,p2) => (Uh p1, Vh p2)))) + } + +\lemma directedProdCover-char {I : DirectedSet} {X : CoverSpace} {D : Set (Set (\Sigma I X))} : isCauchy {DirectedCoverSpace.precover ⨯ X} D <-> DirectProdCover D + => (ClosurePrecoverSpace.closure-cauchy {_} {DirectProdCover.Space} $ later \case \elim __ \with { + | inP (true, (inP (U, inP (V,CV,p), N, g), h)) => (top-cauchy $ inP $ later (N, V, CV, \lam s _ => p $ g s), \lam n => \case h n \with { + | inP (W, inP (W',CW',WW'), Wn) => top-cauchy $ inP $ later (W', CW', \lam _ => WW' Wn) + }) + | inP (false, Cc) => (cauchy-subset Cc \lam (inP (V,CV,p)) => \case I.isInhabitted \with { + | inP N => inP $ later (N, V, CV, \lam _ s => p s) + }, \lam n => cauchy-subset Cc \lam (inP (V,CV,p)) => inP $ later (V, CV, p __)) + }, \lam Dc => cauchy-refine {DirectedCoverSpace.precover ⨯ X} (cauchy-glue {DirectedCoverSpace.precover {I} ⨯ X} (ProductPrecoverSpace.proj2.func-cover Dc.1) + {\lam U V => ∃ (U' : Set X) (N : I) (V' : D) (Set.Prod (N <=) U' ⊆ V') (U = (\lam s => s.2) ^-1 U') (V ⊆ (\lam s => s.1) ^-1 (N <=) || Given (V' : D) (V ⊆ V'))} + \lam {_} (inP (U', inP (N,U,DU,U'U), idp)) => cauchy-subset {DirectedCoverSpace.precover ⨯ X} (cauchy-glue {DirectedCoverSpace.precover {I} ⨯ X} (ProductPrecoverSpace.proj1.func-cover (DirectedCoverSpace.makePrecover N)) + {\lam U V => ∃ (U' : Set I) (U = (\lam s => s.1) ^-1 U') ((U' = (N <=)) || Given (n : I) (U' = single n) (Un : Set X) (Vn : D) (Set.Prod (single n) Un ⊆ Vn) (V = (\lam s => s.2) ^-1 Un))} \lam {V} => \case \elim __ \with { + | inP (V', byLeft p, VV') => top-cauchy {DirectedCoverSpace.precover ⨯ X} $ inP $ later (V', VV', byLeft p) + | inP (V', byRight (n,p), VV') => cauchy-subset {DirectedCoverSpace.precover {I} ⨯ X} (ProductPrecoverSpace.proj2.func-cover (Dc.2 n)) + \lam {W} (inP (W', inP (Vn,DVn,h), WW')) => inP $ later (V', VV', byRight (n, p, W', Vn, DVn, \lam (p1,p2) => rewrite p1 in h p2, WW')) + }) + \lam {_} (inP (U1, V, _, inP (U1',U1U1',e), idp)) => \case \elim e \with { + | byLeft p => inP $ later (U', N, U, DU, \lam (p1,p2) => U'U p1 p2, idp, byLeft $ rewrite (U1U1',p) meet-left) + | byRight (n,p,Un,Vn,DVn,q,r) => inP $ later (U', N, U, DU, \lam (p1,p2) => U'U p1 p2, idp, byRight (Vn, DVn, rewrite (U1U1',r,p) q)) + }) + \lam {_} (inP (U, V, _, inP (U',N,V',DV',U'V',p,e), idp)) => \case \elim e \with { + | byLeft q => inP (V', DV', rewrite p \lam (p1,p2) => U'V' (q p2, p1)) + | byRight (V',DV',V<=V') => inP (V', DV', meet-right <=∘ V<=V') + }) \ No newline at end of file diff --git a/src/Topology/CoverSpace/Locale.ard b/src/Topology/CoverSpace/Locale.ard index 920c790c..d5520d69 100644 --- a/src/Topology/CoverSpace/Locale.ard +++ b/src/Topology/CoverSpace/Locale.ard @@ -19,7 +19,6 @@ \import Topology.RatherBelow \open Bounded(top,top-univ,bottom,bottom-univ) \open LocalePrecoverSpace -\open Set \open RatherBelow \func CoverSpaceLocale (X : PrecoverSpace) : Locale @@ -69,7 +68,7 @@ | byRight q => byRight $ later (j, p *> inv q) } | cover-trans {I} {f} c d => - \have t => cauchy-trans (isStronglyRegular $ cover-char c U'<= cauchy-glue (isStronglyRegular $ cover-char c U'<= U1 s<=< Compl U' || (\Sigma (i : I) (U1 s<=< f i) ((V1 = Compl U1) || (\Sigma (j : J) (g j = V1))))} \case __ \with { | inP (W, byLeft e, W'<= top-cauchy $ byLeft $ rewrite e in W'<= cauchy-subset (cover-char (d i) (rewrite (inv fi=W) in W'<= byRight $ later (i, rewrite fi=W W'<= cover-trans cover-reg \lam (V,V<= cover-trans (cover-inh Xd) \lam (x,Vx) => Cover.cover-inj_<= (x, <=<-right (single_<= Vx) $ s<=<_<=< V<= hasStronglyDensePoints-fromPres \lam Q {U} q => cover-trans (cover-reg-inh Xd) \lam (x,x<= cover-inj (q {CoverSpaceLocale-unit (X.hasDensePoints_hasWeaklyDensePoints Xd) x} $ inP (U, cover-inj () idp, x<= hasStronglyDensePoints-fromPres \lam a => cover-trans (cover-reg-inh Xd) \lam (x,x<= cover-inj (inP (CoverSpaceLocale-unit (X.hasDensePoints_hasWeaklyDensePoints Xd) x, inP (a, cover-inj () idp, x<= p <=∘ Join-univ \lam (U,CU) => \case e CU \with { | inP (V,DV,U<=V) => points_*-mono U<=V <=∘ Join-cond (later (V,DV)) } - | cauchy-trans p e => p <=∘ Join-univ \lam (U,CU) => meet-univ <=-refl top-univ <=∘ MeetSemilattice.meet-monotone <=-refl (e CU) <=∘ + | cauchy-glue p e => p <=∘ Join-univ \lam (U,CU) => meet-univ <=-refl top-univ <=∘ MeetSemilattice.meet-monotone <=-refl (e CU) <=∘ Join-ldistr>= <=∘ Join-univ \lam (V,DUV) => transport (`<= _) points_*_meet $ Join-cond $ later (U ∧ V, inP (U, V, CU, DUV, idp)) \where { \lemma points_<=< {a b : L} (p : a L.<=< b) : points^* a s<=< {LocalePrecoverSpace L} points^* b @@ -162,8 +161,9 @@ } \lemma hasDensePoints (Ld : HasStronglyDensePoints L) : PrecoverSpace.HasDensePoints {LocalePrecoverSpace L} - => __ <=∘ Join-univ \lam (U,CU) => meet-univ <=-refl (points_*-mono \lam {x} Ux => inP $ later (x,Ux)) <=∘ - L.meet-monotone <=-refl (Ld $ ∃ U) <=∘ Join-ldistr>= <=∘ Join-univ \lam s => meet-left <=∘ Join-cond (later (U,(CU,s))) + => __ <=∘ Join-univ \lam (U,CU) => densePoints_cover Ld _ <=∘ Join-univ \lam (inP (x,c)) => Join-cond $ later (U, (CU, inP (x, \case filter-Join c \with { + | inP ((b,p),xb) => p xb + }))) } \func LocaleCoverSpace {L : Locale} (Lr : L.isRegular) : StronglyRegularCoverSpace \cowith diff --git a/src/Topology/CoverSpace/Product.ard b/src/Topology/CoverSpace/Product.ard index a9454b4a..6c5d508d 100644 --- a/src/Topology/CoverSpace/Product.ard +++ b/src/Topology/CoverSpace/Product.ard @@ -29,7 +29,7 @@ | cauchy-cover => cauchy-cover {Prod X Y} | cauchy-top => cauchy-top {Prod X Y} | cauchy-refine => cauchy-refine {Prod X Y} - | cauchy-trans => cauchy-trans {Prod X Y} + | cauchy-glue => cauchy-glue {Prod X Y} | isRegular Cc => closure-subset (isRegular {Prod X Y} Cc) \lam {V} (inP (U,CU,V<= inP (U, CU, unfolds V<= (\lam f {s} Ss => \case f Ss \with { | inP (U,Uo,Ux,V,Vo,Vy,h) => closure-subset (prodCover' (cauchy-open.1 Uo Ux) (cauchy-open.1 Vo Vy)) \lam {W} (inP (U',cU',V',cV',p)) => rewrite p \lam (U's,V's) {(x,y)} (U'x,V'y) => h (cU' U's U'x) (cV' V's V'y) @@ -37,15 +37,15 @@ | inP (U,V,x<= inP (_, X.interior {U}, x<= h (<=<_<= c idp) (<=<_<= d idp)) }) \where { - \private \meta Prod X Y => CoverTransfer {_} {X} __.1 ∨ CoverTransfer {_} {Y} __.2 + \private \meta Prod X Y => CoverTransfer {\Sigma X Y} {X} __.1 ∨ CoverTransfer {\Sigma X Y} {Y} __.2 \private \func proj1' {X Y : CoverSpace} : CoverMap (Prod X Y) X \cowith | func s => s.1 - | func-cover Dc => join-left {CoverLattice (\Sigma X Y)} $ PrecoverTransfer-map.func-cover Dc + | func-cover Dc => join-left {CoverLattice (\Sigma X Y)} $ func-cover {PrecoverTransfer-map {\Sigma X Y} __.1} Dc \private \func proj2' {X Y : CoverSpace} : CoverMap (Prod X Y) Y \cowith | func s => s.2 - | func-cover Dc => join-right {CoverLattice (\Sigma X Y)} $ PrecoverTransfer-map.func-cover Dc + | func-cover Dc => join-right {CoverLattice (\Sigma X Y)} $ func-cover {PrecoverTransfer-map {\Sigma X Y} __.2} Dc \private \lemma prodCover' {X Y : CoverSpace} {C : Set (Set X)} (Cc : X.isCauchy C) {D : Set (Set Y)} (Dc : Y.isCauchy D) : isCauchy {Prod X Y} \lam W => ∃ (U : C) (V : D) (W = \lam s => \Sigma (U s.1) (V s.2)) @@ -59,15 +59,11 @@ | filter-top => inP (top, top, <=<_top, <=<_top, \lam _ _ => ()) | filter-meet (inP (U,V,x<= inP (U ∧ U', V ∧ V', RatherBelow.<=<_meet-same x<= (q Ux Vy, q' U'x V'y)) }) (\case __ \with { - | inP (true, inP (D,Dc,h)) => \case CoverSpace.cauchy-regular-cover Dc x \with { - | inP (U,DU,x<= \case h DU \with { - | inP (W,CW,p) => inP (W, CW, inP (U, top, x<= p Ux)) - } + | inP (true, Dc) => \case CoverSpace.cauchy-regular-cover Dc x \with { + | inP (U, inP (W,CW,p), x<= inP (W, CW, inP (U, top, x<= p Ux)) } - | inP (false, inP (D,Dc,h)) => \case CoverSpace.cauchy-regular-cover Dc y \with { - | inP (V,DV,y<= \case h DV \with { - | inP (W,CW,p) => inP (W, CW, inP (top, V, <=<_top, y<= p Vy)) - } + | inP (false, Dc) => \case CoverSpace.cauchy-regular-cover Dc y \with { + | inP (V, inP (W,CW,p), y<= inP (W, CW, inP (top, V, <=<_top, y<= p Vy)) } }) xy<= inP (U, V, x<= h ((x,y), (idp, q (<=<_<= x<= (f z, g z) - | func-cover => closure-univ-cover $ later \case __ \with { - | inP (true, inP (D,Dc,h)) => cauchy-refine (f.func-cover Dc) \lam (inP (V,DV,p)) => \case h DV \with { - | inP (U',CU',q) => inP (_, inP (U',CU',idp), \lam Ux => q $ rewrite p in Ux) - } - | inP (false, inP (D,Dc,h)) => cauchy-refine (g.func-cover Dc) \lam (inP (V,DV,p)) => \case h DV \with { - | inP (U',CU',q) => inP (_, inP (U',CU',idp), \lam Ux => q $ rewrite p in Ux) - } + | func-cover => func-cover {precover f g} + \where { + \func precover {Z : PrecoverSpace} {X Y : CoverSpace} (f : PrecoverMap Z X) (g : PrecoverMap Z Y) : PrecoverMap Z (X ⨯ Y) \cowith + | func z => (f z, g z) + | func-cover => closure-univ-cover $ later \case __ \with { + | inP (true, Dc) => cauchy-refine (f.func-cover Dc) \lam (inP (V, inP (U',CU',q), p)) => inP (_, inP (U',CU',idp), \lam Ux => q $ rewrite p in Ux) + | inP (false, Dc) => cauchy-refine (g.func-cover Dc) \lam (inP (V, inP (U',CU',q), p)) => inP (_, inP (U',CU',idp), \lam Ux => q $ rewrite p in Ux) + } } \func prod {X Y X' Y' : CoverSpace} (f : CoverMap X Y) (g : CoverMap X' Y') : CoverMap (X ⨯ X') (Y ⨯ Y') => tuple (f ∘ proj1) (g ∘ proj2) \where { - \lemma isDense {X X' Y Y' : CoverSpace} {f : CoverMap X Y} {g : CoverMap X' Y'} (fd : f.IsDense) (gd : g.IsDense) : ContMap.IsDense {prod f g} - => (dense-char {_} {Y ⨯ Y'}).2 $ later \lam {(y,y')} yy'<= - \have | (inP (V,yy'<= <=<-inter yy'<= dense-char.1 fd {y} $ transport (`<=< _) (ext \lam z => ext (pmap __.1, \lam p => ext (p, idp))) $ <=<_^-1 {Y} {Y ⨯ Y'} {tuple id (const y')} yy'<= dense-char.1 gd {y'} $ transport (`<=< _) (ext \lam z => ext (pmap __.2, \lam p => ext (idp, p))) $ <=<_^-1 {Y'} {Y ⨯ Y'} {tuple (const (f x)) id} $ <=<-right (single_<= Vfxy') V<= closure-embedding (\lam c => c) (prod f g) \case __ \with { - | inP (true, inP (D,Dc,f)) => closure $ inP (Bool.true, inP (_, fe Dc, \lam (inP (U,DU,p)) => TruncP.map (f DU) \lam (W,CW,q) => (_, inP (W, CW, (\lam c => p c) <=∘ q), <=-refl))) - | inP (false, inP (D,Dc,f)) => closure $ inP (false, inP (_, ge Dc, \lam (inP (U,DU,p)) => TruncP.map (f DU) \lam (W,CW,q) => (_, inP (W, CW, (\lam c => p c) <=∘ q), <=-refl))) + | inP (true, Dc) => closure $ inP (true, cauchy-subset (fe Dc) \lam (inP (V, inP (W,CW,q), p)) => inP $ later (_, inP (W, CW, (\lam c => p c) <=∘ q), <=-refl)) + | inP (false, Dc) => closure $ inP (false, cauchy-subset (ge Dc) \lam (inP (V, inP (W,CW,q), p)) => inP $ later (_, inP (W, CW, (\lam c => p c) <=∘ q), <=-refl)) } \lemma isDenseEmbedding {X X' Y Y' : CoverSpace} {f : CoverMap X Y} {g : CoverMap X' Y'} (fde : f.IsDenseEmbedding) (gde : g.IsDenseEmbedding) : CoverMap.IsDenseEmbedding {prod f g} - => (isDense fde.1 gde.1, isEmbedding fde.2 gde.2) + => (ProductTopSpace.prod.isDense fde.1 gde.1, isEmbedding fde.2 gde.2) } - \lemma prod-neighborhood {X Y : CoverSpace} {x : X} {y : Y} {W : Set (\Sigma X Y)} (xy<= prod-neighborhood' $ unfolds xy<= ∃ (U : Set X) (V : Set Y) (single x <=< U) (single y <=< V) ∀ {x : U} {y : V} (W (x,y)) + => (\lam xy<= prod-neighborhood' $ unfolds xy<= cauchy-subset {X ⨯ Y} (prodCover (unfolds in x<= + later \lam s {z} t => h (Ug (s.1.1, (pmap __.1 s.2.1, s.2.2.1)) t.1) (Vg (s.1.2, (pmap __.2 s.2.1, s.2.2.2)) t.2) + }) \lemma prodCover {X Y : CoverSpace} {C : Set (Set X)} (Cc : X.isCauchy C) {D : Set (Set Y)} (Dc : Y.isCauchy D) : isCauchy {X ⨯ Y} \lam W => ∃ (U : C) (V : D) (W = \lam s => \Sigma (U s.1) (V s.2)) @@ -140,14 +133,46 @@ | inP (x,Ux), inP (y,Vy) => inP ((x,y), f Ux Vy) } | isCauchyFilter => ClosurePrecoverSpace.closure-filter \this $ later \case __ \with { - | inP (true, inP (D,Dc,f)) => \case F.isCauchyFilter Dc \with { - | inP (V,DV,FV) => \case f DV \with { - | inP (U,CU,q) => inP (U, CU, inP (V, FV, top, filter-top, \lam Vx _ => q Vx)) - } + | inP (true, Dc) => \case F.isCauchyFilter Dc \with { + | inP (V, inP (U,CU,q), FV) => inP (U, CU, inP (V, FV, top, filter-top, \lam Vx _ => q Vx)) } - | inP (false, inP (D,Dc,f)) => \case G.isCauchyFilter Dc \with { - | inP (V,DV,GV) => \case f DV \with { - | inP (U,CU,q) => inP (U, CU, inP (top, filter-top, V, GV, \lam _ Vy => q Vy)) - } + | inP (false, Dc) => \case G.isCauchyFilter Dc \with { + | inP (V, inP (U,CU,q), GV) => inP (U, CU, inP (top, filter-top, V, GV, \lam _ Vy => q Vy)) } } + +\instance PrecoverSpaceHasProduct : HasProduct PrecoverSpace + | Product => ProductPrecoverSpace + +\instance ProductPrecoverSpace (X Y : PrecoverSpace) : PrecoverSpace (\Sigma X Y) + | isCauchy => isCauchy {Prod X Y} + | cauchy-cover => cauchy-cover {Prod X Y} + | cauchy-top => cauchy-top {Prod X Y} + | cauchy-refine => cauchy-refine {Prod X Y} + | cauchy-glue => cauchy-glue {Prod X Y} + \where { + \private \meta Prod X Y => PrecoverTransfer {\Sigma X Y} {X} __.1 ∨ PrecoverTransfer {\Sigma X Y} {Y} __.2 + + \func proj1 {X Y : PrecoverSpace} : PrecoverMap (Prod X Y) X \cowith + | func s => s.1 + | func-cover Dc => join-left {PrecoverLattice (\Sigma X Y)} $ func-cover {PrecoverTransfer-map {\Sigma X Y} __.1} Dc + + \func proj2 {X Y : PrecoverSpace} : PrecoverMap (Prod X Y) Y \cowith + | func s => s.2 + | func-cover Dc => join-right {PrecoverLattice (\Sigma X Y)} $ func-cover {PrecoverTransfer-map {\Sigma X Y} __.2} Dc + + \lemma prodCover {X Y : PrecoverSpace} {C : Set (Set X)} (Cc : X.isCauchy C) {D : Set (Set Y)} (Dc : Y.isCauchy D) + : isCauchy {X ⨯ Y} \lam W => ∃ (U : C) (V : D) (W = \lam s => \Sigma (U s.1) (V s.2)) + => cauchy-subset {Prod X Y} (cauchy-inter {Prod X Y} (proj1.func-cover Cc) (proj2.func-cover Dc)) + \lam (inP (U, V, inP (U',CU',p1), inP (V',DV',p2), q)) => inP $ later (U', CU', V', DV', q *> pmap2 (∧) p1 p2) + } + +\lemma completion-lift-neighborhood2 {X Y : CoverSpace} {Z : CompleteCoverSpace} (g : CoverMap (X ⨯ Y) Z) (F : Completion X) (G : Completion Y) (W : Set Z) + : single (dense-lift (prod completion completion) (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) g (F,G)) <=< W <-> + ∃ (W' : Set Z) (W' <=< W) (V1 : Set X) (F V1) (V2 : Set Y) (G V2) (∀ {x : V1} {y : V2} (W' (g (x,y)))) + => <->trans (dense-lift-neighborhood (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) (F,G) W) $ later + (\lam (inP (W',W'<= \case prod-neighborhood.1 FG<= inP (W', W'<= p $ g V1x V2y) + }, \lam (inP (W',W'<= inP (W', W'<= h (<=<_<= s.1 idp) (<=<_<= s.2 idp), prod-neighborhood.2 $ + inP (mkSet V1, mkSet V2, mkSet_<=<-point.2 FV1, mkSet_<=<-point.2 GV2, \lam p q => (p,q)))) + \where \open Completion \ No newline at end of file diff --git a/src/Topology/CoverSpace/Subspace.ard b/src/Topology/CoverSpace/Subspace.ard index d531c9c5..282e01c4 100644 --- a/src/Topology/CoverSpace/Subspace.ard +++ b/src/Topology/CoverSpace/Subspace.ard @@ -2,6 +2,8 @@ \import Logic \import Logic.Meta \import Meta +\import Order.Lattice +\import Order.PartialOrder \import Paths \import Paths.Meta \import Set.Filter @@ -10,6 +12,7 @@ \import Topology.CoverSpace.Complete \import Topology.RatherBelow \open Set +\open Bounded(top,top-univ) \func OpenCoverSpace (X : CoverSpace) {S : Set X} (So : X.isOpen S) : CoverSpace (Total S) => ClosureCoverSpace isBasicCover (\lam e s => \case \elim e \with { @@ -91,4 +94,52 @@ | x => X.filter-point F' | (inP (U', inP (U, inP (_, idp, U<= isCauchyFilter {F} $ makeBasicCover $ byRight $ regular-closure-extends (regular-closure idp) idp \in inP ((x, <=<_<= (X.filter-point-elem {F'} U<= filter-mono (later \lam s => transport V' (ext idp) s.2) $ X.filter-point-sub (<=<-conv X So x<= CoverTransfer __.1 + | isSeparatedCoverSpace f => ext $ isSeparatedCoverSpace \lam Cc => \case f (PrecoverTransfer.makeCauchy Cc) \with { + | inP (_, inP (U,CU,idp), s) => inP (U, CU, s) + } + | isComplete F => \let G => \new CauchyFilter X { + | F U => F (Set.restrict U) + | filter-mono p Fa => filter-mono (p __) Fa + | filter-top => filter-top + | filter-meet => filter-meet + | isProper FU => \case isProper FU \with { + | inP (x,Ux) => inP (x.1, Ux) + } + | isCauchyFilter Cc => \case isCauchyFilter {F} (PrecoverTransfer.makeCauchy Cc) \with { + | inP (_, inP (U, CU, idp), FU) => inP (U,CU,FU) + } + } + | x => X.filter-point G + \in inP ((x, Sc \lam {V} Vo VG => \case (X.filter-point-char {G} {V}).1 $ X.open-char.1 Vo VG \with { + | inP (W,W<= \case isProper GW \with { + | inP ((x,Sx),Wx) => inP (x, (Sx, <=<_<= W<= \case X.cauchy-regular-cover c x \with { + | inP (U, inP (W,h,p), x<= filter-mono (p <=∘ h (_, (idp, p $ <=<_<= x<= \lam {x} h => \case IsCompleteCoverSpace.cauchyFilterToPoint Sc (later \new CauchyFilter { + | F V => ∃ (U : Set X) (single x <=< U) (restrict U ⊆ V) + | filter-mono p (inP (U,x<= inP (U, x<= inP (top, <=<_top, top-univ) + | filter-meet (inP (U,x<= inP (U ∧ V, <=<-right (meet-univ <=-refl <=-refl) $ <=<_meet x<= \case h X.interior x<= inP ((y,Sy), p $ <=<_<= y<= \case X.cauchy-regular-cover Cc x \with { + | inP (V, inP (U,CU,p), x<= inP (U, CU, inP (V, x<= transport S (isSeparatedCoverSpace $ SeparatedCoverSpace.separated-char 5 7 \lam s<= later + \case p $ <=<-right (\lam q => pmap __.1 q) $ unfolds in <=<_^-1 {_} {_} {PrecoverTransfer-map {Total S} __.1} s<= \case h X.interior $ <=<-right (meet-univ <=-refl <=-refl) $ <=<_meet x<= inP (y, (q {y,Sy} (<=<_<= y<= inP (W, DW, V, Vo, Vx, \lam c => U<=W $ V<=U c) } } - | cauchy-trans f e x => \case f x \with { + | cauchy-glue f e x => \case f x \with { | inP (U,CU,V,Vo,Vx,V<=U) => \case e CU x \with { | inP (U',DUU',V',V'o,V'x,V'<=U') => inP (U ∧ U', inP (U, U', CU, DUU', idp), V ∧ V', open-inter Vo V'o, (Vx, V'x), MeetSemilattice.meet-monotone V<=U V'<=U') } diff --git a/src/Topology/Lipschitz.ard b/src/Topology/Lipschitz.ard new file mode 100644 index 00000000..1ae768ae --- /dev/null +++ b/src/Topology/Lipschitz.ard @@ -0,0 +1,20 @@ +\import Algebra.Monoid +\import Algebra.Ordered +\import Arith.Real +\import Arith.Real.Field +\import Logic +\import Meta +\import Order.LinearOrder +\import Order.PartialOrder +\import Order.StrictOrder +\import Paths +\import Topology.CoverSpace +\import Topology.MetricSpace +\open OrderedField + +\record LipschitzMap (C : Real) (C>0 : 0 < C) \extends UniformMetricMap { + | func-lipschitz {x y : Dom} : dist (func x) (func y) <= C * dist x y + | func-dist-uniform {eps} eps>0 => inP (pos-inv C>0 * eps, OrderedSemiring.<_*_positive_positive (pos-inv>0 C>0) eps>0, + \lam d => func-lipschitz <∘r transport (_ <) (inv *-assoc *> pmap (`* _) (pos-inv-right C>0) *> ide-left) (RealField.<_*_positive-right C>0 d)) + | func-cont {U} => defaultImpl PrecoverMap func-cont {_} {U} +} \ No newline at end of file diff --git a/src/Topology/Locale/Points.ard b/src/Topology/Locale/Points.ard index 0790e8ab..7419e876 100644 --- a/src/Topology/Locale/Points.ard +++ b/src/Topology/Locale/Points.ard @@ -140,7 +140,10 @@ => cover-trans __ \lam ((U,p),V,UV) => cover-trans (d $ points^*-mono (PresentedFrame.embed<= $ cover-inj (V,UV) idp) <=∘ p) \case __ \func HasStronglyDensePoints (L : Locale) : \Prop - => \Pi (P : \Prop) -> points_* (\lam _ => P) <= L.pHat P + => \Pi (a : L) -> a <= L.pHat (∃ (x : CompleteFilter L) (x a)) -\lemma hasStronglyDensePoints-fromPres {P : FramePres} (d : \Pi (Q : \Prop) {a : P} -> points^* (PresentedFrame.embed a) ⊆ (\lam _ => Q) -> Cover a {Q} \lam _ => a) : HasStronglyDensePoints (PresentedFrame P) - => \lam Q => cover-trans __ \lam ((U,q),p,Up) => cover-trans (d Q $ points^*-mono (PresentedFrame.embed<= $ cover-inj (p,Up) idp) <=∘ q) \lam q => cover-inj (q, _, ()) idp \ No newline at end of file +\lemma densePoints_cover {L : Locale} (d : HasStronglyDensePoints L) (a : L) : a <= Join \lam (_ : ∃ (x : CompleteFilter L) (x a)) => a + => meet-univ <=-refl (d a) <=∘ Join-ldistr>= <=∘ Join-univ \lam c => meet-left <=∘ Join-cond c + +\lemma hasStronglyDensePoints-fromPres {P : FramePres} (d : \Pi (a : P) -> Cover a {∃ (points^* (PresentedFrame.embed a))} \lam _ => a) : HasStronglyDensePoints (PresentedFrame P) + => \lam U {a} Ua => cover-trans (d a) \lam (inP (x,ax)) => cover-inj (inP (x, filter-mono (PresentedFrame.embed<= $ cover-inj (a,Ua) idp) ax), a, ()) idp \ No newline at end of file diff --git a/src/Topology/Locale/Real.ard b/src/Topology/Locale/Real.ard index 070a5fbb..63e15ad5 100644 --- a/src/Topology/Locale/Real.ard +++ b/src/Topology/Locale/Real.ard @@ -272,10 +272,10 @@ } \lemma hasStronglyDensePoints : HasStronglyDensePoints RealLocale - => hasStronglyDensePoints-fromPres $ later \lam Q {a} c => \case LinearOrder.dec<_<= a.1 a.2 \with { + => hasStronglyDensePoints-fromPres $ later \lam a => \case LinearOrder.dec<_<= a.1 a.2 \with { | inl r => \case isDense r \with { - | inP (x,a1 cover-inj (c {ratPoint x} (inP (a, cover-inj () idp, (a1 cover-inj (inP (ratPoint x, inP (a, cover-inj () idp, (a1 RealPres.cover-empty r } } diff --git a/src/Topology/MetricSpace.ard b/src/Topology/MetricSpace.ard index 56951176..c9f1b623 100644 --- a/src/Topology/MetricSpace.ard +++ b/src/Topology/MetricSpace.ard @@ -2,6 +2,7 @@ \import Algebra.Monoid \import Algebra.Ordered \import Algebra.Pointed +\import Arith.Rat \import Arith.Real \import Function.Meta \import Logic @@ -27,7 +28,7 @@ \open RealAbGroup \hiding (+, join, meet, negative, zro E -> Real | dist-refl {x : E} : dist x x = zro | dist-symm {x y : E} : dist x y = dist y x @@ -61,20 +62,27 @@ } }) } - | isStronglyRegular Cc => cauchy-subset (uniform-cauchy.2 $ ClosureCoverSpace.closure-regular {ClosurePrecoverSpace isUniform uniform-cover} StronglyRatherBelow (\case dist-uniform.1 __ \with { - | inP (eps,eps>0,h) => ClosurePrecoverSpace.closure $ dist-uniform.2 $ inP $ later (half (half eps), half>0 (half>0 eps>0), \lam x => \case h x \with { - | inP (U,CU,f) => inP (\lam y => dist x y < half (half eps), inP (U, CU, ClosurePrecoverSpace.closure $ uniform-refine {_} {\lam U => ∃ (x : E) (U = \lam y => dist x y < half (half eps))} (dist-uniform.2 $ inP (half (half eps), half>0 (half>0 eps>0), \lam x => inP $ later (_, inP (x, idp), \lam r => r))) \lam {W} => \case __ \with { - | inP (y,p) => rewrite p \case real-located {dist x y} {half eps} {half eps + half (half eps)} (transport (`< _) zro-right $ <_+-right _ $ half>0 $ half>0 eps>0) \with { - | byLeft xy>1/2 => inP (_, byLeft idp, \lam {z} yz<1/4 => \lam xz<1/4 => <-irreflexive $ xy>1/2 <∘ (rewrite (half+half {half eps}) in dist-triang <∘r OrderedAddMonoid.<_+ xz<1/4 (rewrite dist-symm in yz<1/4))) - | byRight xy<3/4 => inP (_, byRight idp, \lam {z} yz<1/4 => f $ dist-triang <∘r OrderedAddMonoid.<_+ xy<3/4 yz<1/4 <∘l Preorder.=_<= (+-assoc *> pmap (_ +) (half+half {half eps}) *> half+half)) - } - }), \lam r => r) + | isStronglyRegularUniform Cu => \case dist-uniform.1 Cu \with { + | inP (eps,eps>0,h) => dist-uniform.2 $ inP $ later (half (half eps), half>0 (half>0 eps>0), \lam x => \case h x \with { + | inP (U,CU,f) => inP (\lam y => dist x y < half (half eps), inP (U, CU, uniform-refine {_} {\lam U => ∃ (x : E) (U = \lam y => dist x y < half (half eps))} (dist-uniform.2 $ inP (half (half eps), half>0 (half>0 eps>0), \lam x => inP $ later (_, inP (x, idp), \lam r => r))) \lam {W} => \case __ \with { + | inP (y,p) => rewrite p \case real-located {dist x y} {half eps} {half eps + half (half eps)} (transport (`< _) zro-right $ <_+-right _ $ half>0 $ half>0 eps>0) \with { + | byLeft xy>1/2 => inP (_, byLeft idp, \lam {z} yz<1/4 => \lam xz<1/4 => <-irreflexive $ xy>1/2 <∘ (rewrite (half+half {half eps}) in dist-triang <∘r OrderedAddMonoid.<_+ xz<1/4 (rewrite dist-symm in yz<1/4))) + | byRight xy<3/4 => inP (_, byRight idp, \lam {z} yz<1/4 => f $ dist-triang <∘r OrderedAddMonoid.<_+ xy<3/4 yz<1/4 <∘l Preorder.=_<= (+-assoc *> pmap (_ +) (half+half {half eps}) *> half+half)) + } + }), \lam r => r) }) - }) (uniform-cauchy.1 Cc)) \lam {V} (inP (U,CU,V<= inP $ later (U, CU, uniform-cauchy.2 V<= ∃ (eps : Real) (0 < eps) ∀ x ∃ (U : C) ∀ {y} (dist x y < eps -> U y) \default dist-uniform \as dist-uniform-impl {C} : isUniform C <-> _ => <->refl + \lemma properUniform : IsProperUniform + => \lam Cu => \case dist-uniform.1 Cu \with { + | inP (eps,eps>0,h) => dist-uniform.2 $ inP (eps, eps>0, \lam x => \case h x \with { + | inP (U,CU,g) => inP (U, later (CU, inP (x, g $ rewrite dist-refl eps>0)), g) + }) + } + \lemma halving {z x y : E} {eps : Real} (d1 : dist z x < half eps) (d2 : dist z y < half eps) : dist x y < eps => dist-triang <∘r OrderedAddMonoid.<_+ (rewrite dist-symm in d1) d2 <∘l Preorder.=_<= half+half @@ -86,6 +94,15 @@ | filter-mono p (inP (eps,eps>0,q)) => inP (eps, eps>0, q <=∘ p) | filter-top => inP (1, RealAbGroup.zro ()) | filter-meet (inP (eps,eps>0,p)) (inP (eps',eps'>0,p')) => inP (eps ∧ eps', LinearOrder.<_meet-univ eps>0 eps'>0, \lam d => (p $ d <∘l meet-left, p' $ d <∘l meet-right)) + + \lemma dist-uniform-rat {C : Set (Set E)} : UniformSpace.isUniform C <-> ∃ (eps : Rat) (0 < eps) ∀ x ∃ (U : C) ∀ {y} (dist x y < eps -> U y) + => (\lam Cu => \case dist-uniform.1 Cu \with { + | inP (eps,eps>0,h) => \case real_<-rat-char.1 eps>0 \with { + | inP (eps',eps'>0,eps' inP (eps', eps'>0, \lam x => \case h x \with { + | inP (U,CU,g) => inP (U, CU, \lam d => g $ d <∘ real_<_L.2 eps'0,h)) => dist-uniform.2 $ inP (eps, real_<_L.2 eps>0, h)) } \lemma dist>=0 {X : PseudoMetricSpace} {x y : X} : 0 <= dist x y @@ -99,7 +116,10 @@ transportInv (`< _) dist-refl eps>0 \lemma OBall-open {X : PseudoMetricSpace} {eps : Real} {x : X} : isOpen (OBall eps x) - => cauchy-open.2 \lam {y} xy uniform-cauchy.2 $ ClosurePrecoverSpace.closure $ uniform-refine (X.makeUniform $ half>0 {eps - dist x y} $ transport (`< _) negative-right $ <_+-left (negative (dist x y)) xy inP (_, later \lam d {w} e => dist-triang <∘r <_+-right (dist x y) (X.halving d e) <∘l Preorder.=_<= (+-comm *> +-assoc *> pmap (eps +) negative-left *> zro-right), <=-refl) + => cauchy-open.2 \lam {y} xy X.makeCauchy $ uniform-refine (X.makeUniform $ half>0 {eps - dist x y} $ transport (`< _) negative-right $ <_+-left (negative (dist x y)) xy inP (_, later \lam d {w} e => dist-triang <∘r <_+-right (dist x y) (X.halving d e) <∘l Preorder.=_<= (+-comm *> +-assoc *> pmap (eps +) negative-left *> zro-right), <=-refl) + +\lemma OBall-center_<=< {X : PseudoMetricSpace} {eps : Real} (eps>0 : 0 < eps) {x : X} : single x <=< OBall eps x + => X.open-char.1 OBall-open (OBall-center eps>0) \lemma dist_open {X : PseudoMetricSpace} {U : Set X} : isOpen U <-> ∀ {x : U} ∃ (eps : Real) (0 < eps) (OBall eps x ⊆ U) => (\lam Uo {x} Ux => \case cauchy-ball (cauchy-open.1 Uo Ux) x \with { @@ -126,9 +146,12 @@ => inP (_, makeUniform $ half>0 $ transport (`< _) negative-right $ <_+-left (negative delta) delta transport (_ <) (+-comm *> +-assoc *> pmap (eps +) negative-left *> zro-right) $ dist-triang <∘r OrderedAddMonoid.<_+ xw ∃ (B : Real) (0 < B) ∀ {x y : S} (dist x y < B) + \class MetricSpace \extends PseudoMetricSpace, SeparatedCoverSpace | dist-ext {x y : E} : dist x y = zro -> x = y - | isSeparatedCoverSpace {x} {y} f => dist-ext $ <=-antisymmetric (\lam d>0 => \case f (uniform-cauchy.2 $ ClosurePrecoverSpace.closure $ makeUniform (half>0 d>0)) \with { + | isSeparatedCoverSpace {x} {y} f => dist-ext $ <=-antisymmetric (\lam d>0 => \case f (makeCauchy $ makeUniform (half>0 d>0)) \with { | inP (U, inP (z,p), (Ux,Uy)) => \have | U'x => rewrite p Ux | U'y => rewrite p Uy diff --git a/src/Topology/MetricSpace/Complete.ard b/src/Topology/MetricSpace/Complete.ard new file mode 100644 index 00000000..53b2266e --- /dev/null +++ b/src/Topology/MetricSpace/Complete.ard @@ -0,0 +1,98 @@ +\import Algebra.Meta +\import Algebra.Monoid +\import Arith.Rat +\import Arith.Real +\import Arith.Real.Field +\import Function() +\import Function.Meta +\import Logic +\import Logic.Meta +\import Meta +\import Operations +\import Order.Lattice +\import Order.LinearOrder +\import Order.PartialOrder +\import Order.StrictOrder +\import Paths +\import Paths.Meta +\import Set.Filter +\import Set.Subset +\import Topology.CoverSpace +\import Topology.CoverSpace.Complete +\import Topology.CoverSpace.Product +\import Topology.MetricSpace +\import Topology.NormedAbGroup.Real +\import Topology.NormedAbGroup.Real.Functions +\import Topology.TopAbGroup.Product +\import Topology.TopSpace +\import Topology.TopSpace.Product +\import Topology.UniformSpace +\import Topology.UniformSpace.Complete + +\func dense-metric-lift {X Y : MetricSpace} {Z : CompleteMetricSpace} (f : IsometricMap X Y) (fd : f.IsDense) (g : MetricMap X Z) : MetricMap Y Z \cowith + | UniformMap => dense-uniform-lift f (f.dense->uniformEmbedding fd) g + | func-dist {y} {y'} => + \have | g~ : UniformMap Y Z => dense-uniform-lift f (f.dense->uniformEmbedding fd) g + | g-char {x} : g~ (f x) = g x => dense-lift-char (fd, f.embedding->coverEmbedding (f.dense->uniformEmbedding fd).2) x + \in Function.id {dist (g~ y) (g~ y') <= dist y y'} $ RealAbGroup.meet_<=' $ dense-lift-unique (prod f f) (prod.isDense fd fd) (real-meet-uniform ∘ tuple (dist-uniform-map ∘ prod g~ g~) dist-uniform-map) (dist-uniform-map ∘ prod g~ g~) + (\lam (x,x') => Function.id {dist (g~ (f x)) (g~ (f x')) ∧ dist (f x) (f x') = dist (g~ (f x)) (g~ (f x'))} $ rewrite (g-char,g-char) $ RealAbGroup.meet_<= $ later $ rewrite f.func-isometry g.func-dist) (y,y') + \where { + \open ProductTopSpace + \open ContMap + } + +\instance MetricCompletion (X : PseudoMetricSpace) : CompleteMetricSpace + | CompleteUniformSpace => UniformCompletion X + | dist x y => dist-cover (x,y) + | dist-refl => dist-refl-lem + | dist-symm {y} {y'} => dense-lift-unique (prod completion completion) (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding).1 dist-cover (dist-cover ∘ tuple proj2 proj1) (\lam x => dist-char *> dist-symm *> inv dist-char) (y,y') + | dist-triang => filter-dist-triang _ _ _ + | dist-uniform => dist-uniform-lem + | dist-ext {F} {G} FG=0 => isSeparatedCoverSpace $ UniformSpace.uniform-separated.2 $ later \case dist-uniform-lem.1 __ \with { + | inP (eps,eps>0,h) => later \case h F \with { + | inP (U,CU,g) => inP (U, CU, (g $ rewrite dist-refl-lem eps>0, g $ rewrite FG=0 eps>0)) + } + } + \where { + \open ProductCoverSpace + \open CoverMap + + \sfunc dist-cover : CoverMap (Completion X ⨯ Completion X) RealNormed + => dense-lift (prod completion completion) (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) dist-uniform-map + + \lemma dist-char {x y : X} : dist-cover (pointCF x, pointCF y) = dist x y + => rewrite (\peval dist-cover) $ dense-lift-char (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) (x,y) + + \private \lemma dist-refl-lem {F : RegularCauchyFilter X} : dist-cover (F, F) = (0 : Real) + => dense-lift-unique completion completion.isDenseEmbedding.1 (dist-cover ∘ tuple id id) (const 0) (\lam x => dist-char *> dist-refl) F + + \private \lemma dist-uniform-lem {C : Set (Set (Completion X))} : isUniform C <-> ∃ (eps : Real) (0 < eps) ∀ x ∃ (U : C) ∀ {y} (dist-cover (x,y) < eps -> U y) + => (later \lam (inP (D,Du,g)) => \case dist-uniform.1 Du \with { + | inP (eps,eps>0,h) => inP (halfs 2 eps, halfs>0 2 eps>0, \lam F => \case isCauchyFilter (X.makeCauchy $ X.makeUniform (halfs>0 4 eps>0)) \with { + | inP (_, inP (x,idp), Fx) => \case h x \with { + | inP (V,DV,Vd) => \case g DV \with { + | inP (U,CU,VU) => inP (U, CU, \lam {G} d => \case isCauchyFilter (X.makeCauchy $ X.makeUniform (halfs>0 4 eps>0)) \with { + | inP (_, inP (y,idp), Gy) => VU $ filter-mono (later \lam {z} d' => Vd + \have | t => dist-neighborhood (pointCF x) F (halfs>0 2 eps>0) (OBall-center_<=< $ halfs>0 4 eps>0) Fx + | s => dist-neighborhood G (pointCF y) (halfs>0 2 eps>0) Gy (OBall-center_<=< $ halfs>0 4 eps>0) + \in rewriteI dist-char $ rewriteI dist-char at d' $ linarith (filter-dist-triang (pointCF x) F (pointCF z), filter-dist-triang F G (pointCF z), filter-dist-triang G (pointCF y) (pointCF z))) Gy + }) + } + } + }) + }, \lam (inP (eps,eps>0,h)) => inP (_, X.makeUniform {half (half eps)} $ half>0 $ half>0 eps>0, \lam {_} (inP (x,idp)) => \case h (pointCF x) \with { + | inP (U,CU,g) => inP (U, CU, \lam {F} Fx => g $ dist-neighborhood _ _ eps>0 {x} (OBall-center_<=< $ half>0 $ half>0 eps>0) Fx) + })) + + \lemma filter-dist-triang (x y z : RegularCauchyFilter X) : dist-cover (x,z) <= dist-cover (x,y) + dist-cover (y,z) + => RealAbGroup.meet_<=' $ dense-lift-unique (prod (prod completion completion) completion) (prod.isDenseEmbedding (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) completion.isDenseEmbedding).1 + (real-meet-uniform ∘ tuple (dist-cover ∘ prod proj1 id) (+-uniform ∘ tuple (dist-cover ∘ proj1) (dist-cover ∘ prod proj2 id))) + (dist-cover ∘ prod proj1 id) + (\lam ((x,y),z) => Function.id {dist-cover (pointCF x, pointCF z) ∧ (dist-cover (pointCF x, pointCF y) + dist-cover (pointCF y, pointCF z)) = dist-cover (pointCF x, pointCF z)} $ + rewrite (dist-char,dist-char,dist-char) $ RealAbGroup.meet_<= dist-triang) + ((x,y),z) + + \lemma dist-neighborhood (F G : RegularCauchyFilter X) {eps : Real} (eps>0 : 0 < eps) {x : X} (Fx : F (OBall (half (half eps)) x)) (Gx : G (OBall (half (half eps)) x)) : dist-cover (F,G) < eps + => rewrite (\peval dist-cover) $ simplify in RealAbGroup.abs>=_- <∘r <=<_<= ((completion-lift-neighborhood2 (dist-uniform-map {X}) F G (OBall eps 0)).2 $ inP + (OBall (half eps) 0, <=*_<=< $ OBall_<=* (half0), _, Fx, _, Gx, \lam {z1} d1 {z2} d2 => RealAbGroup.abs_-_< (linarith (dist>=0 {X} {z1}, half>0 eps>0)) $ simplify $ halving d1 d2)) idp + } \ No newline at end of file diff --git a/src/Topology/MetricSpace/Nat.ard b/src/Topology/MetricSpace/Nat.ard new file mode 100644 index 00000000..aa1e9bfc --- /dev/null +++ b/src/Topology/MetricSpace/Nat.ard @@ -0,0 +1,109 @@ +\import Algebra.Group +\import Algebra.Meta +\import Algebra.Monoid +\import Algebra.Ordered +\import Arith.Int +\import Arith.Nat +\import Arith.Rat +\import Arith.Real +\import Data.Or +\import Function.Meta +\import Logic +\import Logic.Meta +\import Meta +\import Order.Lattice +\import Order.LinearOrder +\import Order.PartialOrder +\import Order.StrictOrder +\import Paths +\import Paths.Meta +\import Set.Fin +\import Set.Subset +\import Topology.Compact +\import Topology.CoverSpace +\import Topology.CoverSpace.Complete +\import Topology.MetricSpace +\import Topology.NormedAbGroup.Real +\import Topology.UniformSpace +\import Topology.UniformSpace.Complete +\open LinearlyOrderedAbGroup +\open RatField (finv) + +\instance NatMetricSpace : MetricSpace Nat + | dist n m => abs (finv (suc n) - finv (suc m)) + | dist-refl => RatNormed.dist-refl + | dist-symm => RatNormed.dist-symm + | dist-triang => RatNormed.dist-triang {_} {_} {finv (suc _)} + | dist-ext p => pmap pred $ pmap ratDenom $ RatNormed.dist-ext {_} {finv (suc _)} p + \where { + \func Cover (C : Set (Set Nat)) : \Prop + => ∃ (U : C) (N : Nat) (\Pi {n : Nat} -> N <= n -> U n) (\Pi (j : Fin N) -> Given (V : C) (V j)) + + \lemma uniform-char {C : Set (Set Nat)} : NatMetricSpace.isUniform C <-> Cover C + => (\lam Cu => \case NatMetricSpace.dist-uniform-rat.1 Cu \with { + | inP (eps,eps>0,h) => \case Real.natBounded {finv (eps * ratio 1 2) : Real} \with { + | inP (N,eps \case h N, FinSet.finiteAC {N} (\lam j => NatMetricSpace.uniform-cover Cu j) \with { + | inP (U,CU,g), inP c => inP (U, CU, N, \lam {n} N<=n => g $ real_<_L.2 $ abs_+ <∘r + (\have lem {m : Nat} (p : finv (eps * ratio 1 2) < m) : finv (suc m) < eps * ratio 1 2 + => transport (_ <) RatField.finv_finv $ RatField.finv_< (RatField.finv>0 linarith) $ p <∘ fromInt_< (pos + \have | N1N2>0 {m : Nat} (m>0 : 0 < m) : 0 RatField.< m * suc m => fromInt_< $ pos0 NatSemiring.zero finv (suc m) < finv (suc n) + => (\lam p => RatField.finv_< {suc n} {suc m} idp $ fromInt_< $ pos NatSemiring.unsuc< $ pos cmp.2 $ linarith (transportInv (_ <) (RatField.finv>0-diff {suc N} idp) $ RatField.abs_-left {finv (suc n)} {finv (suc m)} <∘r real_<_U.1 d, cmp.1 n real_<_U.2 $ transport (_ <) (simplify : finv (suc n) - finv m + (finv m - finv (suc m)) = _) ( + transportInv (_ <) (zro-left *> RatField.finv>0-diff (fromInt_< $ pos0 $ zero<=_ <∘r n0 $ N1N2>0 NatSemiring.zero \case LinearOrder.dec<_<= n N \with { + | inl n \have s => c (toFin n n \case LinearOrder.trichotomy n m \with { + | less n absurd $ <-irreflexive $ lem2 n transport s.1 (toFin=id *> n=m) s.3 + | greater m absurd $ <-irreflexive $ lem2 m inP (U, CU, \lam {m} d => g \case LinearOrder.dec<_<= m N, LinearOrder.dec<_<= m n \with { + | inr N<=m, _ => N<=m + | _, inr n<=m => N<=n <=∘ n<=m + | inl m \have d' => transport (`< _) NatMetricSpace.dist-symm d + \in absurd $ <-irreflexive $ lem2 m totallyBounded-uniform-char NatMetricSpace.properUniform 1 0 \lam Cu => \case uniform-char.1 Cu \with { + | inP (U,CU,N,g,h) => inP (U :: \lam j => (h j).1, uniform-char.2 $ inP $ later (U, inP (0,idp), N, g, \lam j => ((h j).1, inP (suc j, idp), (h j).3)), \case \elim __ \with { + | 0 => CU + | suc j => (h j).2 + }) + } + + \lemma cauchy-char {C : Set (Set Nat)} : NatMetricSpace.isCauchy C <-> Cover C + => (\lam Cc => uniform-char.1 $ totallyBounded-cauchy-uniform NatMetricSpace.properUniform totallyBounded Cc, + \lam Cc => uniform-cauchy.1 $ ClosurePrecoverSpace.closure $ uniform-char.2 Cc) + + \lemma makeUniform (N : Nat) : NatMetricSpace.isUniform \lam U => (U = (N <=)) || (\Sigma (n : Nat) (n < N) (U = single n)) + => uniform-char.2 $ inP $ later (N <=, byLeft idp, N, \lam p => p, \lam n => (_, byRight (n, fin_< n, idp), idp)) + + \lemma makeCover (N : Nat) : NatMetricSpace.isCauchy \lam U => (U = (N <=)) || (\Sigma (n : Nat) (n < N) (U = single n)) + => NatMetricSpace.makeCauchy (makeUniform N) + } + +\func atTop : CauchyFilter NatMetricSpace \cowith + | F U => ∃ (N : Nat) ∀ {n} (N <= n -> U n) + | filter-mono p (inP (N,f)) => inP (N, \lam q => p $ f q) + | filter-top => inP (0, \lam _ => ()) + | filter-meet (inP (N,f)) (inP (M,g)) => inP (N ∨ M, \lam p => (f $ join-left <=∘ p, g $ join-right <=∘ p)) + | isProper (inP (N,f)) => inP (N, f <=-refl) + | isCauchyFilter => (cauchyFilter-uniform-char {_} {\this}).2 \lam Cu => \case NatMetricSpace.uniform-char.1 Cu \with { + | inP (U,CU,N,g,_) => inP (U, CU, inP (N,g)) + } \ No newline at end of file diff --git a/src/Topology/NormedAbGroup.ard b/src/Topology/NormedAbGroup.ard index f823a3cc..8cfa5ffd 100644 --- a/src/Topology/NormedAbGroup.ard +++ b/src/Topology/NormedAbGroup.ard @@ -1,5 +1,6 @@ \import Algebra.Group \import Algebra.Group.Category +\import Algebra.Monoid \import Algebra.Ordered \import Arith.Real \import Function.Meta @@ -15,6 +16,7 @@ \import Topology.CoverSpace \import Topology.MetricSpace \import Topology.TopAbGroup +\import Topology.TopAbGroup.Complete \import Topology.UniformSpace \import Topology.UniformSpace.Product @@ -59,6 +61,13 @@ \default dist x y : Real => norm (x - y) \default norm-dist \as norm-dist-impl {x} {y} : dist x y = norm (x - y) => idp + + \func IsUnbounded : \Prop + => \Pi (B : Nat) -> ∃ (x : E) (B RealAbGroup.< norm x) + + \lemma norm_BigSum {l : Array E} : norm (BigSum l) <= RealAbGroup.BigSum \lam j => norm (l j) \elim l + | nil => transportInv (`<= _) norm_zro <=-refl + | x :: l => norm_+ <=∘ LinearlyOrderedAbMonoid.<=_+ <=-refl norm_BigSum } \class NormedAbGroup \extends PseudoNormedAbGroup, MetricSpace @@ -68,6 +77,18 @@ \lemma norm_dist {X : PseudoNormedAbGroup} {x : X} : norm x = dist 0 x => inv norm_negative *> simplify *> inv norm-dist +\lemma norm>=0 {X : PseudoNormedAbGroup} {x : X} : 0 <= norm x + => rewrite norm_dist dist>=0 + +\lemma norm_- {X : PseudoNormedAbGroup} {x y : X} : norm (x - y) = norm (y - x) + => pmap norm (inv X.negative-isInv) *> norm_negative *> simplify + +\lemma norm_-left {X : PseudoNormedAbGroup} {x y : X} : norm x - norm y <= norm (x - y) + => transport (_ <=) (+-assoc *> pmap (_ +) negative-right *> zro-right) $ LinearlyOrderedAbMonoid.<=_+ (transport (norm __ <= _) (+-assoc *> pmap (x +) negative-left *> zro-right) norm_+) <=-refl + +\lemma norm_-right {X : PseudoNormedAbGroup} {x y : X} : norm y - norm x <= norm (x - y) + => transport (_ <=) norm_- norm_-left + \record UniformNormedAbGroupMap \extends UniformMetricMap, TopAbGroupMap { \override Dom : PseudoNormedAbGroup \override Cod : PseudoNormedAbGroup @@ -100,4 +121,4 @@ | func-isometry => norm-dist *> pmap norm (inv func-minus) *> func-norm-isometry *> inv norm-dist } -\class CompleteNormedAbGroup \extends NormedAbGroup, CompleteMetricSpace +\class CompleteNormedAbGroup \extends NormedAbGroup, CompleteMetricSpace, CompleteTopAbGroup diff --git a/src/Topology/NormedAbGroup/Real.ard b/src/Topology/NormedAbGroup/Real.ard index 05026511..a5ca33e4 100644 --- a/src/Topology/NormedAbGroup/Real.ard +++ b/src/Topology/NormedAbGroup/Real.ard @@ -43,8 +43,8 @@ \lam F => inP (fromCF F, \lam {U} => \case <=<-ball __ \with { | inP (eps,eps>0,p) => \let | x => fromCF F - | (inP (a, x-eps0,Fy1,a (real_<-char {x - eps} {x}).1 $ transport (_ <) zro-right $ <_+-right x $ RealAbGroup.positive_negative eps>0 - | (inP (b, inP (y2,eps2,eps2>0,Fy2,y2+eps2 (real_<-char {x} {x + eps}).1 $ transport {Real} (`< _) zro-right $ <_+-right x eps>0 + | (inP (a, x-eps0,Fy1,a (real_<-rat-char {x - eps} {x}).1 $ transport (_ <) zro-right $ <_+-right x $ RealAbGroup.positive_negative eps>0 + | (inP (b, inP (y2,eps2,eps2>0,Fy2,y2+eps2 (real_<-rat-char {x} {x + eps}).1 $ transport {Real} (`< _) zro-right $ <_+-right x eps>0 \in filter-mono ((later \lam {z} (|y1-z| abs_-_< (RealAbGroup.<-diff-left $ real_<_U.2 x-eps=id <∘r real_<_L.1 (transport (`< _) norm-dist |y1-z|=neg {y2 - z} <∘r real_<_L.1 (transport (`< _) norm-dist |y2-z| \lam {y} {U} Uo Uy => \case (dist_open {RealNormedAbGroup} {U}).1 Uo Uy \with { - | inP (eps,eps>0,p) => \case real_<-char.1 $ transport (`< _) zro-right $ <_+-right y eps>0 \with { + | inP (eps,eps>0,p) => \case real_<-rat-char.1 $ transport (`< _) zro-right $ <_+-right y eps>0 \with { | inP (x,y inP (x, inP (x, idp), p $ unfold OBall $ rewrite norm-dist $ abs_-_< (transport (_ <) negative-right (RealAbGroup.<_+-left _ $ real_<_U.2 y0) $ transport2 (<) +-comm (inv +-assoc *> pmap (`+ _) negative-left *> zro-left) $ <_+-right (negative y) $ real_<_L.2 x0 : 0 < eps) : RealNormed.isCauchy \lam U => ∃ (a : Rat) (U = open-rat-int a (a + eps)) - => uniform-cauchy.2 $ closure $ dist-uniform.2 $ inP (eps * ratio 1 4, real_<_L.2 linarith, \lam x => later \case (real_<-char {x - eps * ratio 1 2} {x - eps * ratio 1 4}).1 $ <_+-right x $ RealAbGroup.negative_< $ real_<_L.2 linarith \with { + => RealNormed.makeCauchy $ inP (eps * ratio 1 4, real_<_L.2 linarith, \lam x => later \case (real_<-rat-char {x - eps * ratio 1 2} {x - eps * ratio 1 4}).1 $ <_+-right x $ RealAbGroup.negative_< $ real_<_L.2 linarith \with { | inP (a,x-eps/2 inP (_, inP (a, idp), \lam d => ( real_<_L.1 $ real_<_L.2 a=id <∘r (rewrite norm-dist in d)), real_<_U.1 $ RealAbGroup.<-diff-mid (simplify in abs>=neg <∘r (rewrite norm-dist in d)) <∘ @@ -129,7 +129,7 @@ \lemma <=<-open-int {x : Real} {U : Set Real} (p : single x <=< U) : ∃ (a b : Rat) (x.L a) (x.U b) ∀ (y : Real) (y.L a -> y.U b -> U y) => \case <=<-ball p \with { - | inP (eps,eps>0,q) => \case (real_<-char {x - eps} {x}).1 $ transport (_ <) zro-right $ <_+-right x $ RealAbGroup.positive_negative eps>0, (real_<-char {x} {x + eps}).1 $ transport (`< _) zro-right $ <_+-right x eps>0 \with { + | inP (eps,eps>0,q) => \case (real_<-rat-char {x - eps} {x}).1 $ transport (_ <) zro-right $ <_+-right x $ RealAbGroup.positive_negative eps>0, (real_<-rat-char {x} {x + eps}).1 $ transport (`< _) zro-right $ <_+-right x eps>0 \with { | inP (a,x-eps inP (a, b, a q $ transportInv (`< _) norm-dist $ abs_-_< (RealAbGroup.<-diff-left $ real_<_U.2 x-eps ∃ (a' b' c1 d1 c2 d2 : Rat) (a < a') (b' < b) (x.L c1) (x.U d1) (y.L c2) (y.U d2) (\Pi {x y : Rat} -> \Sigma (c1 < x) (x < d1) -> \Sigma (c2 < y) (y < d2) -> open-rat-int a' b' (f (x,y))) => <->trans (dense-lift-real-char {RatNormed ⨯ RatNormed} {_} {prod rat_real rat_real} (prod.isDenseEmbedding rat_real.dense-coverEmbedding rat_real.dense-coverEmbedding) (x,y) a b) $ later - (\lam (inP (a',b',a \case prod-neighborhood xy<= \case prod-neighborhood.1 xy<= \case <=<-open-int x<= inP (a', b', c1, d1, c2, d2, a q $ h (p1 x' c1 rewrite (norm-dist,norm-dist) $ join-univ norm_-left $ simplify norm_-right + +\lemma dist-uniform-map {X : PseudoMetricSpace} : UniformMap (X ⨯ X) RealNormed (\lam s => dist s.1 s.2) \cowith + | func-uniform Eu => \case dist-uniform.2 Eu \with { + | inP (eps,eps>0,h) => inP (_, X.makeUniform (RealAbGroup.half>0 eps>0), _, X.makeUniform (RealAbGroup.half>0 eps>0), \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (dist x x') \with { + | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy g $ LinearOrder.<_join-univ + (linarith (RealAbGroup.half+half, X.dist-triang {x} {y} {x'}, X.dist-triang {y} {y'} {x'}, X.dist-symm {x'} {y'})) + (linarith (RealAbGroup.half+half, X.dist-triang {y} {x} {y'}, X.dist-triang {x} {x'} {y'}, X.dist-symm {x} {y}))) + }) + } + +\lemma real-meet-uniform : UniformMap (RealNormed ⨯ RealNormed) RealNormed \lam s => s.1 ∧ s.2 \cowith + | func-uniform Eu => \case dist-uniform.2 Eu \with { + | inP (eps,eps>0,h) => inP (_, RealNormed.makeUniform eps>0, _, RealNormed.makeUniform eps>0, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (x ∧ x') \with { + | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy g $ RealAbGroup.abs_-_< + (unfold (-) $ rewrite (RealAbGroup.meet_negative, RealAbGroup.join_+-left) $ LinearOrder.<_join-univ + (RealAbGroup.<=_+ meet-left <=-refl <∘r RealAbGroup.abs>=id <∘r xy=id <∘r x'y'=_- <∘r xy=_- <∘r x'y' s.1 ∨ s.2 \cowith + | func-uniform Eu => \case dist-uniform.2 Eu \with { + | inP (eps,eps>0,h) => inP (_, RealNormed.makeUniform eps>0, _, RealNormed.makeUniform eps>0, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (x ∨ x') \with { + | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy g $ RealAbGroup.abs_-_< + (unfold (-) $ rewrite (RealAbGroup.join_negative, RealAbGroup.join_+-right) $ LinearOrder.<_join-univ + (RealAbGroup.<=_+ <=-refl meet-left <∘r RealAbGroup.abs>=id <∘r xy=id <∘r x'y'=_- <∘r xy=_- <∘r x'y' s.1 * s.2) + => LocallyUniformMetricMap.makeLocallyUniformMap2 (*) \lam {eps} eps>0 => inP (1, RealAbGroup.zro + \let | lem : 0 < norm x0 + norm y0 + 3 => linarith (norm>=0 {_} {x0}, norm>=0 {_} {y0}) + | gamma => (RealField.pos-inv lem * eps) ∧ 1 + | gamma>0 : 0 < gamma => LinearOrder.<_meet-univ (RealField.<_*_positive_positive (RealField.pos-inv>0 lem) eps>0) zro0, \lam {x} {x'} {y} {y'} x0x<1 y0y<1 xx' + rewrite norm-dist at xx'=0 $ LinearOrder.<_<= yy'=0) <∘r + rewrite {2} *-comm (transport (`< _) rdistr $ <_*_positive-left (linarith (norm_-right {_} {x0} {x}, norm_-right {_} {y0} {y}, norm_-right {_} {y} {y'}, meet-right : gamma <= 1) : norm x + norm y' < norm x0 + norm y0 + 3) gamma>0 <∘l + <=_*_positive-right (LinearOrder.<_<= lem) meet-left <=∘ Preorder.=_<= (inv *-assoc *> pmap (`* _) (OrderedField.pos-inv-right lem) *> ide-left))))) + +\lemma pow-cover {X : PseudoNormedRing} (n : Nat) : CoverMap X X (pow __ n) \elim n + | 0 => CoverMap.const 1 + | suc n => *-locally-uniform CoverMap.∘ ProductCoverSpace.tuple (pow-cover n) CoverMap.id + +\class NormedRing \extends PseudoNormedRing, NormedAbGroup + +\class CompleteNormedRing \extends NormedRing, CompleteNormedAbGroup + +\lemma norm_zro_ide {X : PseudoNormedRing} : (X.norm 1 = (0 : Real)) || (X.norm 1 = (1 : Real)) + => \have t => rewrite ide-left in X.norm_*_<= {1} {1} + \in \case RealField.locality_- (X.norm 1) \with { + | byLeft q => byRight $ <=-antisymmetric norm_ide_<= $ RealField.<=_Inv-cancel-left q norm>=0 $ transportInv (`<= _) ide-right t + | byRight q => byLeft $ <=-antisymmetric (RealField.<=_Inv-cancel-left q (linarith norm_ide_<=) $ transport2 (<=) (inv rdistr) (inv zro_*-right) $ later $ rewrite (ide-left,Ring.negative_*-left) linarith) norm>=0 + } + +\lemma norm_ide=0 {X : PseudoNormedRing} (p : X.norm 1 = (0 : Real)) {x : X} : norm x = (0 : Real) + => pmap norm (inv ide-right) *> <=-antisymmetric (norm_*_<= <=∘ rewrite (p,RealField.zro_*-right) <=-refl) norm>=0 + +\lemma norm_<=_pow {X : PseudoNormedRing} {x : X} {n : Nat} : norm (pow x n) <= pow (norm x) n \elim n + | 0 => norm_ide_<= + | suc n => norm_*_<= <=∘ RealField.<=_*_positive-left norm_<=_pow norm>=0 + +\class PseudoValuedRing \extends PseudoNormedRing + | norm_* {x y : E} : norm (x * y) = norm x RealField.* norm y + | norm_ide : norm 1 = (1 : Real) + | norm_*_<= => Preorder.=_<= norm_* + | norm_ide_<= => Preorder.=_<= norm_ide + +\class ValuedRing \extends PseudoValuedRing, NormedRing + +\class CompleteValuedRing \extends ValuedRing, CompleteNormedRing + +\lemma norm_pow {X : PseudoValuedRing} {x : X} {n : Nat} : norm (pow x n) = pow (norm x) n \elim n + | 0 => norm_ide + | suc n => norm_* *> pmap (`* _) norm_pow + +\instance RealValuedRing : CompleteValuedRing Real + | CompleteNormedAbGroup => RealNormed + | Ring => RealField + | norm_* => RealField.abs_* + | norm_ide => RealField.abs-ofPos $ LinearOrder.<_<= zro ∃ (U : isOpen) (U 0) ∀ x ∃ (V : C) ∀ {y} (U (x - y) -> V y) \default neighborhood-uniform \as neighborhood-uniform-impl {C} : _ <-> _ => <->refl {isUniform C} + \lemma properUniform : IsProperUniform + => \lam Cu => \case neighborhood-uniform.1 Cu \with { + | inP (U,Uo,U0,h) => neighborhood-uniform.2 $ inP (U, Uo, U0, \lam x => \case h x \with { + | inP (V,CV,g) => inP (V, later (CV, inP (x, g $ transportInv U negative-right U0)), g) + }) + } + \func makeUniform {U : Set E} (Uo : isOpen U) (U0 : U 0) : UniformSpace.isUniform \lam V => ∃ (x : E) (V = \lam y => U (x - y)) => neighborhood-uniform.2 $ inP (U, Uo, U0, \lam x => inP (_, inP $ later (x, idp), \lam u => u)) - \lemma shrink {U : Set E} (Uo : isOpen U) (U0 : U 0) : ∃ (V : isOpen) (V 0) ∀ {x y : V} (U (x - y)) + \lemma shrink {U : Set E} (Uo : isOpen U) (U0 : U 0) : ∃ (V : isOpen) (V 0) (V <= shrink' +-cont negative-cont Uo U0 \func UBall (U : Set E) (x : E) : Set E => \lam x' => U (x - x') @@ -88,6 +95,22 @@ } } +\func \infix 4 <= ∀ {x y : V} (U (x - y)) + +\lemma <= \lam Vx => transport U simplify (p Vx V0) + +\lemma <= \lam W-x W-y => simplify $ transport U +-comm $ simplify in p W-x W-y + +\lemma <= inP (_, X.makeUniform Wo W0, \lam {y} (inP (_, (inP (z,idp), (w,(Wxw,Wzw))), Wzy)) => simplify in q (p Wxw Wzw) (p W0 Wzy)) + +\lemma <= transport2 (<=*) (ext \lam x => simplify) (ext \lam x => simplify) $ <= dense-uniform-lift f (f.embedding->uniformEmbedding fd) g + | func-+ {y} {y'} => + \have | g~ => dense-uniform-lift f (f.embedding->uniformEmbedding fd) g + | g-char {x} : g~ (f x) = g x => dense-lift-char (fd.1, f.embedding->coverEmbedding (f.embedding->uniformEmbedding fd).2) x + \in dense-lift-unique (prod f f) (prod.isDense fd.1 fd.1) (g~ ∘ Y.+-cont) (+-cont ∘ prod g~ g~) (\lam (x,x') => pmap g~ (inv f.func-+) *> g-char *> g.func-+ *> inv (pmap2 (+) g-char g-char)) (y,y') + \where { + \open ProductTopSpace + \open ContMap + } + +\instance TopAbGroupCompletion (X : TopAbGroup) : CompleteTopAbGroup + | CompleteUniformSpace => UniformCompletion X + | AbGroup => abGroup + | +-cont => +-cover + | negative-cont => negative-cover + | neighborhood-uniform => (\lam (inP (D,Du,g)) => \case neighborhood-uniform.1 Du \with { + | inP (U1,U1o,U1_0,h) => + \have | (inP (U2,U2o,U2_0,h2)) => X.shrink U1o U1_0 + | (inP (U3,U3o,U3_0,h3)) => X.shrink U2o U2_0 + \in inP (mkSet U3, mkSet-open U3o, PrecoverSpace.open-char.1 U3o U3_0, \lam F => \case isCauchyFilter {F} (X.makeCauchy $ X.makeUniform U3o U3_0) \with { + | inP (_, inP (x,idp), Fx) => \case h x \with { + | inP (V,DV,d) => \case g DV \with { + | inP (U',CU',p) => inP (U', CU', \lam {G} q => p \case topAb-neighborhood.1 $ mkSet_<=<-point.2 q \with { + | inP (U'',U''<= filter-mono (later \lam {z} V2z => \case isProper (filter-meet Fx FV1) \with { + | inP (y,(U3xy,V1y)) => d $ simplify in h2 (h3 U3xy U3_0) (h3 U3_0 $ <=<_<= (<=<_<= U''<= \case <=<-inter $ (PrecoverSpace.open-char {Completion X}).1 (PrecoverSpace.cauchy-open.2 U1o) U1_0 \with { + | inP (U2,U2_0,U2<= \case X.shrink (completion.func-cont $ CoverSpace.interior {Completion X}) U2_0 \with { + | (inP (U3,U3o,U3_0,h3)) => inP (_, X.makeUniform U3o U3_0, \lam {_} (inP (x,idp)) => \case h1 (pointCF x) \with { + | inP (V,CV,g) => inP (V, CV, \lam {F} FU3x => g $ <=<_<= (topAb-neighborhood.2 $ + inP (U2, U2<= transport (\lam w => U2 (pointCF w)) X.diff-cancel-left $ <=<_<= (h3 q p) idp)) idp) + }) + } + }) + \where { + \open ProductCoverSpace + \open CoverMap + + \private \func abGroup : AbGroup (RegularCauchyFilter X) \cowith + | zro => pointCF 0 + | + => +-func + | zro-left => unique1 (+-cover ∘ tuple (const _) id) id \lam x => +-char *> pmap pointCF zro-left + | +-assoc => unique3 (+-cover ∘ prod +-cover id) (+-cover ∘ tuple (proj1 ∘ proj1) (+-cover ∘ prod proj2 id)) + \lam x y z => pmap (+-func __ _) +-char *> +-char *> pmap pointCF +-assoc *> inv (pmap (+-func _) +-char *> +-char) + | negative => negative-cover + | negative-left => unique1 (+-cover ∘ tuple negative-cover id) (const _) \lam x => pmap (+-func __ _) negative-char *> +-char *> pmap pointCF negative-left + | +-comm => unique2 +-cover (+-cover ∘ tuple proj2 proj1) \lam x y => +-char *> pmap pointCF +-comm *> inv +-char + + \sfunc subtract-cover : CoverMap (Completion X ⨯ Completion X) (Completion X) + => dense-lift (prod completion completion) (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) (completion CoverMap.∘ +-uniform ∘ prod id negative-uniform) + + \lemma subtract-char {x y : X} : subtract-cover (pointCF x, pointCF y) = pointCF (x - y) + => rewrite (\peval subtract-cover) $ dense-lift-char (prod.isDenseEmbedding completion.isDenseEmbedding completion.isDenseEmbedding) (x,y) + + \lemma subtract_- {F G : RegularCauchyFilter X} : subtract-cover (F,G) = F - {abGroup} G + => unique2 subtract-cover (+-cover ∘ prod id negative-cover) \lam x y => subtract-char *> inv +-char *> pmap (+-func _) (inv negative-char) + + \sfunc +-cover : CoverMap (Completion X ⨯ Completion X) (Completion X) + => subtract-cover ∘ prod id negative-cover + + \func +-func (x y : RegularCauchyFilter X) => +-cover (x,y) + + \lemma +-char {x y : X} : +-cover (pointCF x, pointCF y) = pointCF (x + y) + => rewrite (\peval +-cover) $ pmap (\lam z => subtract-cover (pointCF x, z)) negative-char *> subtract-char *> simplify + + \sfunc negative-cover : CoverMap (Completion X) (Completion X) + => subtract-cover ∘ tuple (const $ pointCF 0) id + + \lemma negative-char {x : X} : negative-cover (pointCF x) = pointCF (negative x) + => rewrite (\peval negative-cover) $ subtract-char *> simplify + + \lemma unique1 (f g : CoverMap (Completion X) (Completion X)) (p : \Pi (x : X) -> f (pointCF x) = g (pointCF x)) {x : RegularCauchyFilter X} : f x = g x + => dense-lift-unique completion completion.isDenseEmbedding.1 f g p x + + \lemma unique2 (f g : CoverMap (Completion X ⨯ Completion X) (Completion X)) (p : \Pi (x y : X) -> f (pointCF x, pointCF y) = g (pointCF x, pointCF y)) {x y : RegularCauchyFilter X} : f (x,y) = g (x,y) + => dense-lift-unique (prod completion completion) (ProductTopSpace.prod.isDense completion.isDenseEmbedding.1 completion.isDenseEmbedding.1) f g (\lam s => p s.1 s.2) (x,y) + + \lemma unique3 (f g : CoverMap (Completion X ⨯ Completion X ⨯ Completion X) (Completion X)) (p : \Pi (x y z : X) -> f ((pointCF x, pointCF y), pointCF z) = g ((pointCF x, pointCF y), pointCF z)) {x y z : RegularCauchyFilter X} : f ((x,y),z) = g ((x,y),z) + => dense-lift-unique (prod (prod completion completion) completion) (ProductTopSpace.prod.isDense (ProductTopSpace.prod.isDense completion.isDenseEmbedding.1 completion.isDenseEmbedding.1) completion.isDenseEmbedding.1) f g (\lam s => p s.1.1 s.1.2 s.2) ((x,y),z) + + \lemma topAb-neighborhood {F G : RegularCauchyFilter X} {U : Set (Completion X)} : single (F - {abGroup} G) <=< U <-> + ∃ (U' : Set (Completion X)) (U' <=< U) (V1 : Set X) (F V1) (V2 : Set X) (G V2) ∀ {x : V1} {y : V2} (U' (pointCF (x - y))) + => rewrite (inv subtract_-, \peval subtract-cover) $ completion-lift-neighborhood2 (completion ∘ +-uniform ∘ prod id negative-uniform) F G U + } diff --git a/src/Topology/TopAbGroup/Product.ard b/src/Topology/TopAbGroup/Product.ard index d80a5611..94fecde2 100644 --- a/src/Topology/TopAbGroup/Product.ard +++ b/src/Topology/TopAbGroup/Product.ard @@ -8,6 +8,9 @@ \import Paths \import Paths.Meta \import Set.Subset +\import Topology.CoverSpace +\import Topology.CoverSpace.Complete +\import Topology.CoverSpace.Product \import Topology.TopAbGroup \import Topology.TopSpace \import Topology.TopSpace.Product @@ -54,10 +57,15 @@ \instance TopAbGroupHasProduct : HasProduct TopAbGroup | Product => ProductTopAbGroup -\lemma negative-map {X : TopAbGroup} : TopAbGroupMap X X negative \cowith +\lemma negative-uniform {X : TopAbGroup} : TopAbGroupMap X X negative \cowith | func-+ => X.negative_+ *> +-comm | func-cont => negative-cont.func-cont \lemma +-uniform {X : TopAbGroup} : TopAbGroupMap (X ⨯ X) X \lam s => s.1 + s.2 \cowith | func-+ => equation - | func-cont => +-cont.func-cont \ No newline at end of file + | func-cont => +-cont.func-cont + +\lemma BigSum-cover {X : CoverSpace} {Y : TopAbGroup} (fs : Array (CoverMap X Y)) + : CoverMap X Y \lam x => Y.BigSum \lam j => fs j x \elim fs + | nil => CoverMap.const 0 + | f :: fs => +-uniform CoverMap.∘ ProductCoverSpace.tuple f (BigSum-cover fs) \ No newline at end of file diff --git a/src/Topology/TopSpace.ard b/src/Topology/TopSpace.ard index a356427e..a7c7eb5b 100644 --- a/src/Topology/TopSpace.ard +++ b/src/Topology/TopSpace.ard @@ -1,6 +1,8 @@ +\import Function.Meta ($) \import Logic \import Logic.Meta \import Meta +\import Order.Directed \import Order.Lattice \import Order.PartialOrder \import Paths @@ -29,6 +31,12 @@ => \Pi (y : E) -> ∃ (W : isOpen) (W y) (Given (V ∧ W) -> W ⊆ U) \func IsRegular => ∀ {U : isOpen} {x : U} ∃ (V : isOpen) (V x) (V <= E) (l : E) : \Prop + => ∀ {U : isOpen} (U l) ∃ (N : I) ∀ {n} (N <= n -> U (f n)) + + \func IsClosed (U : Set E) : \Prop + => \Pi {x : E} -> (\Pi {V : Set E} -> isOpen V -> V x -> ∃ (U ∧ V)) -> U x } \func NFilter {X : TopSpace} (x : X) : ProperFilter X \cowith @@ -41,7 +49,7 @@ \func IsDenseSet {X : TopSpace} (S : Set X) : \Prop => \Pi {x : X} {U : Set X} -> isOpen U -> U x -> ∃ (y : S) (U y) -\class ContMap \extends SetHom { +\record ContMap \extends SetHom { \override Dom : TopSpace \override Cod : TopSpace @@ -76,6 +84,14 @@ | func-cont _ => Y.cover-open \lam Ux => inP (top, open-top, (), \lam _ => Ux) } +\lemma const-limit {I : DirectedSet} {X : TopSpace} {x : X} : X.IsLimit (\lam (_ : I) => x) x + => \lam _ Ux => \case I.isInhabitted \with { + | inP N => inP (N, \lam _ => Ux) + } + +\lemma cont-limit {I : DirectedSet} {X Y : TopSpace} {f : I -> X} {l : X} (p : X.IsLimit f l) (g : ContMap X Y) : Y.IsLimit (\lam n => g (f n)) (g l) + => \lam Uo Ugl => p (g.func-cont Uo) Ugl + \class HausdorffTopSpace \extends TopSpace | isHausdorff {x y : E} : ∀ {U V : isOpen} (U x) (V y) ∃ (U ∧ V) -> x = y @@ -85,4 +101,12 @@ } \lemma dense-lift-unique {X Y : TopSpace} {Z : HausdorffTopSpace} (f : ContMap X Y) (fd : f.IsDense) (g h : ContMap Y Z) (p : \Pi (x : X) -> g (f x) = h (f x)) (y : Y) : g y = h y - => denseSet-lift-unique fd g h (\lam (inP (x,q)) => rewriteI q (p x)) y \ No newline at end of file + => denseSet-lift-unique fd g h (\lam (inP (x,q)) => rewriteI q (p x)) y + +\func TopTransfer {X : \Set} {Y : TopSpace} (f : X -> Y) : TopSpace X \cowith + | isOpen U => ∃ (V : isOpen) (U = f ^-1 V) + | open-top => inP (top, open-top, idp) + | open-inter (inP (V,Vo,p)) (inP (V',V'o,p')) => inP (V ∧ V', open-inter Vo V'o, pmap2 (∧) p p') + | open-Union {S} h => inP (Set.Union \lam V => \Sigma (isOpen V) (f ^-1 V ⊆ Set.Union S), open-Union __.1, <=-antisymmetric (\lam (inP (U,SU,Ux)) => \case h SU \with { + | inP (V,Vo,p) => inP (V, (Vo, rewriteI p $ Set.Union-cond SU), rewrite p in Ux) + }) (\lam (inP (V,(Vo,p),Vfx)) => p Vfx)) \ No newline at end of file diff --git a/src/Topology/TopSpace/Product.ard b/src/Topology/TopSpace/Product.ard index 1cf93446..4a7b6926 100644 --- a/src/Topology/TopSpace/Product.ard +++ b/src/Topology/TopSpace/Product.ard @@ -37,6 +37,24 @@ \func prod {X X' Y Y' : TopSpace} (f : ContMap X Y) (f' : ContMap X' Y') : ContMap (X ⨯ X') (Y ⨯ Y') => tuple (f ∘ proj1) (f' ∘ proj2) + \where { + \lemma isDense {X X' Y Y' : TopSpace} {f : ContMap X Y} {g : ContMap X' Y'} (fd : f.IsDense) (gd : g.IsDense) : ContMap.IsDense {prod f g} + => \lam Uo Ux => \case Uo Ux \with { + | inP (U1,U1o,U1x,U2,U2o,U2y,h) => \case fd U1o U1x, gd U2o U2y \with { + | inP (_, inP (x',idp), U1fx'), inP (_, inP (y',idp), U2gy') => inP (_, inP ((x',y'), idp), h U1fx' U2gy') + } + } + + \lemma isEmbedding {X X' Y Y' : TopSpace} {f : ContMap X Y} {g : ContMap X' Y'} (fd : f.IsEmbedding) (gd : g.IsEmbedding) : ContMap.IsEmbedding {prod f g} + => (embedding-char {prod f g}).2 \lam Uo Uxy => \case Uo Uxy \with { + | inP (U1,U1o,U1x,U2,U2o,U2y,h) => \case f.embedding-char.1 fd U1o U1x, g.embedding-char.1 gd U2o U2y \with { + | inP (V1,V1o,V1fx,p1), inP (V2,V2o,V2gy,p2) => inP (Set.Prod V1 V2, Prod-open V1o V2o, (V1fx,V2gy), \lam (q1,q2) => h (p1 q1) (p2 q2)) + } + } + + \lemma isDenseEmbedding {X X' Y Y' : TopSpace} {f : ContMap X Y} {g : ContMap X' Y'} (fd : f.IsDenseEmbedding) (gd : g.IsDenseEmbedding) : ContMap.IsDenseEmbedding {prod f g} + => (isDense fd.1 gd.1, isEmbedding fd.2 gd.2) + } } \lemma Prod-open {X Y : TopSpace} {U : Set X} (Uo : isOpen U) {V : Set Y} (Vo : isOpen V) : isOpen (Set.Prod U V) diff --git a/src/Topology/UniformSpace.ard b/src/Topology/UniformSpace.ard index 4d802a04..b6a3bd20 100644 --- a/src/Topology/UniformSpace.ard +++ b/src/Topology/UniformSpace.ard @@ -4,6 +4,7 @@ \import Meta \import Order.Lattice \import Order.PartialOrder +\import Paths \import Paths.Meta \import Set.Filter \import Set.Subset @@ -11,7 +12,7 @@ \import Topology.CoverSpace.Complete \import Topology.RatherBelow \open Set -\open Bounded(top,top-univ) +\open Bounded(top,top-univ,bottom,bottom-univ) \open ClosurePrecoverSpace \class UniformSpace \extends CompletelyRegularCoverSpace { @@ -26,13 +27,43 @@ | cauchy-cover Cc x => closure-filter (pointFilter x) (\lam Cu => uniform-cover Cu x) $ uniform-cauchy.1 Cc | cauchy-top => uniform-cauchy.2 $ closure-top idp | cauchy-refine Cc e => uniform-cauchy.2 $ closure-refine (uniform-cauchy.1 Cc) e - | cauchy-trans Cc e => uniform-cauchy.2 $ closure-trans (uniform-cauchy.1 Cc) (\lam CU => uniform-cauchy.1 $ e CU) idp + | cauchy-glue Cc e => uniform-cauchy.2 $ closure-trans (uniform-cauchy.1 Cc) (\lam CU => uniform-cauchy.1 $ e CU) idp | isCompletelyRegular Cc => cauchy-subset (uniform-cauchy.2 $ isCompletelyRegular {ClosureRegularCoverSpace isUniform uniform-cover uniform-star} (uniform-cauchy.1 Cc)) \lam {V} (inP (U,CU,V<= inP $ later (U, CU, unfolds $ unfolds at V<= (R', \lam r => uniform-cauchy.2 $ c r, d, e)) \default isCauchy : Set (Set E) -> \Prop => Closure isUniform \default uniform-cauchy \as uniform-cauchy-impl {C} : isCauchy C <-> Closure isUniform C => <->refl + \lemma makeCauchy {C : Set (Set E)} (Cu : isUniform C) : CoverSpace.isCauchy C + => uniform-cauchy.2 (closure Cu) + + \func IsProperUniform : \Prop + => ∀ {C : isUniform} (isUniform \lam U => \Sigma (C U) (∃ U)) + + \func IsWeaklyProperUniform : \Prop + => \Pi {C : Set (Set E)} -> isUniform (\lam U => (U = {Set E} bottom) || C U) -> isUniform C + + \lemma proper_weaklyProper (p : IsProperUniform) : IsWeaklyProperUniform + => \lam Cu => uniform-subset (p Cu) \case __ \with { + | (byLeft e, inP (x,Ux)) => \case rewrite e in Ux \with { + | inP ((),_) + } + | (byRight CU, _) => CU + } + + \lemma inhabited_weaklyProper (p : TruncP E) : IsWeaklyProperUniform \elim p + | inP x => \lam Cu => uniform-refine Cu \case \elim __ \with { + | byLeft p => \case uniform-cover Cu x \with { + | inP (_, byLeft idp, inP ((),_)) + | inP (V, byRight CV, Vx) => inP (V, CV, rewrite p bottom-univ) + } + | byRight CU => inP (_, CU, <=-refl) + } + + \lemma uniform-inter-big (Cs : Array (Set (Set E))) (Cu : ∀ (C : Cs) (isUniform C)) : isUniform (CoverInterBig Cs) \elim Cs + | nil => uniform-top + | C :: Cs => uniform-inter (Cu 0) $ uniform-inter-big _ (\lam j => Cu (suc j)) + \lemma <=*-inter {V U : Set E} (p : V <=* U) : ∃ (V' : Set E) (V <=* V') (V' <=* U) \elim p | inP (C,Cc,p) => \case uniform-star Cc \with { | inP (D,Dc,g) => inP (star V D, inP (D, Dc, <=-refl), inP (D, Dc, (\case __ \with { @@ -54,6 +85,14 @@ \lemma <=<-regular {C : Set (Set E)} (Cu : isUniform C) : isUniform \lam V => ∃ (U : C) (V <=< U) => uniform-subset (<=*-regular Cu) \lam {V} (inP (U,CU,p)) => inP $ later (U, CU, <=*_<=< p) + + \lemma uniform-separated {x y : E} : ∀ {C : CoverSpace.isCauchy} ∃ (U : C) (\Sigma (U x) (U y)) <-> ∀ {C : isUniform} ∃ (U : C) (\Sigma (U x) (U y)) + => (\lam sf Cu => sf $ makeCauchy Cu, \lam sf Cc => closure-filter (\new SetFilter E { + | F U => \Sigma (U x) (U y) + | filter-mono p (Ux,Uy) => (p Ux, p Uy) + | filter-top => ((), ()) + | filter-meet (Ux,Uy) (Vx,Vy) => ((Ux, Vx), (Uy, Vy)) + }) sf $ uniform-cauchy.1 Cc) } \where { \func star {X : \Set} (V : Set X) (C : Set (Set X)) : Set X => Union \lam W => \Sigma (C W) (Given (V ∧ W)) @@ -67,8 +106,12 @@ \func \infix 4 <=* {X : UniformSpace} (V U : Set X) : \Prop => ∃ (C : isUniform) (UniformSpace.star V C ⊆ U) -\lemma <=*_<=< {X : UniformSpace} {V U : Set X} (p : V <=* U) : V <=< U \elim p - | inP (C,Cc,p) => uniform-cauchy.2 $ closure $ uniform-refine Cc \lam {W} CW => inP (W, \lam s => Union-cond (CW,s) <=∘ p, <=-refl) +\lemma <=*-char {X : UniformSpace} {V U : Set X} : V <=* U <-> isUniform \lam W => Given (V ∧ W) -> W ⊆ U + => (\lam (inP (C,Cu,p)) => uniform-subset Cu $ later \lam {W} CW s Wx => p $ inP (W,(CW,s),Wx), + \lam Cu => inP (_, Cu, \lam (inP (W,(g,s),Wx)) => g s Wx)) + +\lemma <=*_<=< {X : UniformSpace} {V U : Set X} (p : V <=* U) : V <=< U + => X.makeCauchy (<=*-char.1 p) \instance StarRatherBelow {X : UniformSpace} : RatherBelow (<=* {X}) | <=<-left (inP (C,Cu,p)) q => inP (C, Cu, p <=∘ q) @@ -79,15 +122,18 @@ \lemma uniform-subset {X : UniformSpace} {C D : Set (Set X)} (Cc : isUniform C) (e : \Pi {U : Set X} -> C U -> D U) : isUniform D => uniform-refine Cc \lam {U} CU => inP (U, e CU, <=-refl) +\lemma top-uniform {X : UniformSpace} {C : Set (Set X)} (Ct : C top) : isUniform C + => uniform-subset uniform-top $ later \lam p => rewriteI p Ct + \lemma uniform-embedding-char {X : UniformSpace} {Y : PrecoverSpace} {f : PrecoverMap X Y} : f.IsEmbedding <-> ∀ {C : isUniform} (isCauchy \lam V => ∃ (U : C) (f ^-1 V ⊆ U)) - => (\lam e Cu => e $ uniform-cauchy.2 $ closure Cu, closure-embedding (uniform-cauchy.1 __) f) + => (\lam e Cu => e $ X.makeCauchy Cu, closure-embedding (uniform-cauchy.1 __) f) \record LocallyUniformMap \extends CoverMap { \override Dom : UniformSpace \override Cod : UniformSpace - | func-locally-uniform {E : Set (Set Cod)} : isUniform E -> ∃ (C : isUniform) (∀ {U : C} (isUniform \lam V => ∃ (W : E) (U ∧ V ⊆ func ^-1 W))) + | func-locally-uniform {E : Set (Set Cod)} : isUniform E -> ∃ (C : isUniform) ∀ {U : C} (isUniform \lam V => ∃ (W : E) (U ∧ V ⊆ func ^-1 W)) | func-cover {E'} E'c => closure-univ-cover (\lam {E} Eu => uniform-cauchy.2 \case func-locally-uniform Eu \with { | inP (C,Cu,e) => closure-refine (closure-trans (closure Cu) (\lam CU => closure (e CU)) idp) \lam {Z} (inP (U, V, CU, inP (W, EW, q), p)) => inP $ later (_, inP (W, EW, idp), rewrite p q) }) (uniform-cauchy.1 E'c) @@ -105,4 +151,61 @@ \func IsDenseEmbedding : \Prop => \Sigma IsDense IsEmbedding -} \ No newline at end of file +} \where { + \func compose \alias \infixl 8 ∘ {X Y Z : UniformSpace} (g : UniformMap Y Z) (f : UniformMap X Y) : UniformMap X Z \cowith + | func x => g (f x) + | func-uniform Du => uniform-subset (f.func-uniform $ g.func-uniform Du) \lam (inP (V, inP (W,DW,q), p)) => inP $ later (W, DW, p *> rewrite q idp) +} + +\func UniformTransfer {X : \Set} {Y : UniformSpace} (f : X -> Y) : UniformSpace X \cowith + | CoverSpace => CoverTransfer f + | isUniform C => isUniform \lam V => ∃ (U : C) (f ^-1 V ⊆ U) + | uniform-cover Ec x => \case uniform-cover Ec (f x) \with { + | inP (U, inP (V,CV,p), Ufx) => inP (V, CV, p Ufx) + } + | uniform-top => top-uniform $ inP $ later (top, idp, top-univ) + | uniform-refine Ec r => uniform-subset Ec \lam (inP (V,CV,p)) => \case r CV \with { + | inP (W,DW,V<=W) => inP $ later (W, DW, p <=∘ V<=W) + } + | uniform-inter Cu Du => uniform-subset (uniform-inter Cu Du) \lam {_} (inP (U', inP (U,CU,Up), V', inP (V,DV,Vp), idp)) => inP $ later (U ∧ V, inP (U, CU, V, DV, idp), MeetSemilattice.meet-monotone Up Vp) + | uniform-star Cu => \case uniform-star Cu \with { + | inP (D',D'u,h) => inP (\lam V => ∃ (V' : D') (V = f ^-1 V'), uniform-subset D'u \lam {V'} D'V' => \case h D'V' \with { + | inP (V, inP (U,CU,p), g) => inP $ later (_, inP (V', D'V', idp), <=-refl) + }, \lam {_} (inP (V',D'V',idp)) => \case h D'V' \with { + | inP (V, inP (U,CU,p), g) => inP (U, CU, \lam {_} (inP (W',D'W',idp)) (x,s) {y} W'fy => p $ g D'W' (f x, s) W'fy) + }) + } + | uniform-cauchy => (\lam Cc => closure-refine (closure-univ-closure f (\lam Cu => closure $ uniform-subset Cu \lam {U} CU => inP $ later (_, inP (U, CU, idp), <=-refl)) (uniform-cauchy.1 Cc)) \lam {_} (inP (V, inP (U,CU,p), idp)) => inP (U, CU, p), + closure-cauchy {X} {CoverTransfer f} \lam Cu => Y.makeCauchy Cu) + +\type \infix 4 s<=* {X : UniformSpace} (V U : Set X) : \Prop + => isUniform \lam W => (W = Compl V) || (W = U) + +\instance StronglyStarRatherBelow {X : UniformSpace} : RatherBelow (s<=* {X}) + | <=<_top => unfolds $ top-uniform $ byRight idp + | <=<-left p q => uniform-refine (unfolds in p) \lam {U'} => later \case __ \with { + | byLeft r => rewrite r $ inP (_, byLeft idp, <=-refl) + | byRight r => rewrite r $ inP (_, byRight idp, q) + } + | <=<-right p q => uniform-refine (unfolds in q) \lam {U'} => later \case __ \with { + | byLeft r => inP (_, byLeft idp, rewrite r \lam nVx Wx => nVx (p Wx)) + | byRight r => inP (U', byRight r, <=-refl) + } + | <=<_meet U<= uniform-refine (uniform-inter (unfolds in U<= rewrite p \case \elim t1, \elim t2 \with { + | byLeft r, _ => inP (_, byLeft idp, rewrite r \lam (nUx,_) (Ux,_) => nUx Ux) + | _, byLeft r => inP (_, byLeft idp, rewrite r \lam (_,nVx) (_,Vx) => nVx Vx) + | byRight q, byRight r => inP (_, byRight $ pmap2 (∧) q r, <=-refl) + } + +\class StronglyRegularUniformSpace \extends UniformSpace, StronglyRegularCoverSpace { + | isStronglyRegularUniform {C : Set (Set E)} : isUniform C -> isUniform \lam V => ∃ (U : C) (V s<=* U) + | isStronglyRegular Cc => uniform-cauchy.2 $ ClosureCoverSpace.closure-regular StronglyRatherBelow (\lam Cu => closure $ uniform-subset (isStronglyRegularUniform Cu) \lam {V} (inP (U,CU,p)) => inP $ later (U, CU, uniform-cauchy.2 $ closure p)) (uniform-cauchy.1 Cc) + + \lemma s<=*-cauchy-regular {C : Set (Set E)} (Cc : CoverSpace.isCauchy C) : CoverSpace.isCauchy \lam V => ∃ (U : C) (V s<=* U) + => uniform-cauchy.2 $ ClosureCoverSpace.closure-regular StronglyStarRatherBelow (\lam Cu => closure $ isStronglyRegularUniform Cu) (uniform-cauchy.1 Cc) +} + +\func StronglyRegularUniformTransfer {X : \Set} {Y : StronglyRegularUniformSpace} (f : X -> Y) : StronglyRegularUniformSpace X \cowith + | UniformSpace => UniformTransfer f + | isStronglyRegularUniform Cu => uniform-subset (isStronglyRegularUniform Cu) \lam {V} (inP (U, inP (W,CW,p), V<= inP $ later + (_, inP (W, CW, <=<-left (uniform-subset (unfolds in V<= inP $ later (_, ||.map (pmap (f ^-1)) (pmap (f ^-1)) e, <=-refl)) p), <=-refl) \ No newline at end of file diff --git a/src/Topology/UniformSpace/Complete.ard b/src/Topology/UniformSpace/Complete.ard index 344e99bf..57d3cf7f 100644 --- a/src/Topology/UniformSpace/Complete.ard +++ b/src/Topology/UniformSpace/Complete.ard @@ -28,7 +28,7 @@ | CompleteCoverSpace => Completion X | isUniform D => ∃ (C : isUniform) (∀ {U : C} ∃ (V : D) (mkSet U ⊆ V)) | uniform-cover (inP (C,Cu,p)) F => - \have | (inP (U,CU,FU)) => isCauchyFilter (uniform-cauchy.2 $ closure Cu) + \have | (inP (U,CU,FU)) => isCauchyFilter (X.makeCauchy Cu) | (inP (V,DV,q)) => p CU \in inP (V, DV, q FU) | uniform-top => inP (single top, uniform-top, \lam _ => inP (top, idp, \lam _ => ())) @@ -48,7 +48,22 @@ } }) } - | uniform-cauchy => (\lam (inP (C',C'c,f)) => closure-map mkSet (\lam {F} => filter-top) mkSet_<= (\lam s => filter-meet s.1 s.2) f $ uniform-cauchy.1 C'c, closure-cauchy $ later \lam (inP (C',C'u,f)) => inP (C', uniform-cauchy.2 $ closure C'u, f)) + | uniform-cauchy => (\lam (inP (C',C'c,f)) => closure-map mkSet (\lam {F} => filter-top) mkSet_<= (\lam s => filter-meet s.1 s.2) f $ uniform-cauchy.1 C'c, + closure-cauchy $ later \lam (inP (C',C'u,f)) => inP (C', X.makeCauchy C'u, f)) + \where { + \lemma properUniform (Xp : X.IsProperUniform) : UniformSpace.IsProperUniform {UniformCompletion X} + => \lam (inP (D,Du,h)) => inP (_, Xp $ X.<=<-regular Du, \lam {U'} (inP (U, DU, U'<= \case h DU \with { + | inP (V,CV,p) => inP (V, (CV, inP (pointCF x, p $ <=<-right (single_<= U'x) U'<= ∃ (U : C) (V = mkSet U) + => inP (C, Cu, \lam CU => inP (_, inP (_, CU, idp), <=-refl)) + } + +\lemma mkSet_<=* {X : UniformSpace} {V U : Set X} (p : V <=* U) : mkSet V <=* mkSet U \elim p + | inP (C,Cu,p) => inP (_, UniformCompletion.makeUniform Cu, \lam {F} (inP (_, (inP (W,CW,idp), (G,(GV,GW))), FW)) => filter-mono ((\lam Wx => \case isProper (filter-meet GV GW) \with { + | inP s => inP $ later (W, (CW, s), Wx) + }) <=∘ p) FW) \func uniform-completion {X : UniformSpace} : UniformMap X (UniformCompletion X) \cowith | CoverMap => completion @@ -58,9 +73,13 @@ | inP (V,DV,p) => inP (pointCF ^-1 V, inP (V, DV, idp), \lam Ux => p $ <=<-right (single_<= Ux) U<= (completion.isDenseEmbedding.1, \lam {C} Cu => inP (C, Cu, \lam {U} CU => inP (Completion.mkSet U, inP (U, CU, <=<_<= __ idp), <=-refl))) + } \lemma cauchyFilter-uniform-char {X : UniformSpace} {F : SetFilter X} : ∀ {C : isCauchy} ∃ (U : C) (F U) <-> ∀ {C : isUniform} ∃ (U : C) (F U) - => (\lam Fc Cu => Fc $ uniform-cauchy.2 $ closure Cu, \lam f Cc => closure-filter F f (uniform-cauchy.1 Cc)) + => (\lam Fc Cu => Fc $ X.makeCauchy Cu, \lam f Cc => closure-filter F f (uniform-cauchy.1 Cc)) \lemma regularFilter-uniform-char {X : UniformSpace} {F : CauchyFilter X} : ∀ {U : F.F} ∃ (V : Set X) (V <=< U) (F V) <-> ∀ {U : F.F} ∃ (V : Set X) (V <=* U) (F V) => (\lam Fr => RegularCauchyFilter.ratherBelow StarRatherBelow StarRatherBelow.<=<-left (\lam p => <=<_<= (<=*_<=< p)) X.<=*-cauchy-regular (\new RegularCauchyFilter { | CauchyFilter => F | isRegularFilter => Fr }), \lam f FU => TruncP.map (f FU) \lam (V,p,FV) => (V, <=*_<=< p, FV)) diff --git a/src/Topology/UniformSpace/Product.ard b/src/Topology/UniformSpace/Product.ard index beba8ba7..34c7389f 100644 --- a/src/Topology/UniformSpace/Product.ard +++ b/src/Topology/UniformSpace/Product.ard @@ -11,10 +11,12 @@ \import Set.Subset \import Topology.CoverSpace \import Topology.CoverSpace.Product +\import Topology.TopSpace.Product \import Topology.UniformSpace \open ClosurePrecoverSpace \open Set \open Bounded(top) +\open UniformMap \instance UniformSpaceHasProduct : HasProduct UniformSpace | Operations.HasProduct.Product => ProductUniformSpace @@ -36,14 +38,15 @@ }) } | uniform-cauchy => (closure-univ-closure-id $ later \case \elim __ \with { - | inP (true, inP (D,Dc,h)) => closure-refine (closure-univ-closure __.1 (\lam {C} Cu => closure $ inP (C, Cu, single top, uniform-top, \lam {_} (inP (U,CU,_,idp,idp)) => inP (_, inP (U, CU, idp), __.1))) $ uniform-cauchy.1 Dc) \lam (inP (V,DV,p)) => \case h DV \with { - | inP (W,CW,q) => inP (W, CW, rewrite p q) - } - | inP (false, inP (D,Dc,h)) => closure-refine (closure-univ-closure __.2 (\lam {C} Cu => closure $ inP (single top, uniform-top, C, Cu, \lam {_} (inP (_,idp,U,CU,idp)) => inP (_, inP (U, CU, idp), __.2))) $ uniform-cauchy.1 Dc) \lam (inP (V,DV,p)) => \case h DV \with { - | inP (W,CW,q) => inP (W, CW, rewrite p q) - } - }, closure-univ-closure-id $ later \lam {E} (inP (C,Cu,D,Du,r)) => closure-refine (ProductCoverSpace.prodCover (uniform-cauchy.2 $ closure Cu) (uniform-cauchy.2 $ closure Du)) r) + | inP (true, Dc) => closure-refine (closure-univ-closure __.1 (\lam {C} Cu => closure $ inP (C, Cu, single top, uniform-top, \lam {_} (inP (U,CU,_,idp,idp)) => inP (_, inP (U, CU, idp), __.1))) $ uniform-cauchy.1 Dc) \lam (inP (V, inP (W,CW,q), p)) => inP (W, CW, rewrite p q) + | inP (false, Dc) => closure-refine (closure-univ-closure __.2 (\lam {C} Cu => closure $ inP (single top, uniform-top, C, Cu, \lam {_} (inP (_,idp,U,CU,idp)) => inP (_, inP (U, CU, idp), __.2))) $ uniform-cauchy.1 Dc) \lam (inP (V, inP (W,CW,q), p)) => inP (W, CW, rewrite p q) + }, closure-univ-closure-id $ later \lam {E} (inP (C,Cu,D,Du,r)) => closure-refine (ProductCoverSpace.prodCover (X.makeCauchy Cu) (Y.makeCauchy Du)) r) \where { + \lemma properUniform (Xp : X.IsProperUniform) (Yp : Y.IsProperUniform) : UniformSpace.IsProperUniform {X ⨯ Y} + => \lam {E} (inP (C,Cu,D,Du,r)) => inP (_, Xp Cu, _, Yp Du, \lam {W'} (inP (U, (CU, inP (x,Ux)), V, (DV, inP (y,Vy)), p)) => \case r {W'} $ inP (U, CU, V, DV, p) \with { + | inP (W,EW,W'<=W) => inP (W, (EW, inP ((x,y), W'<=W $ rewrite p (Ux,Vy))), W'<=W) + }) + \func proj1 {X Y : UniformSpace} : UniformMap (X ⨯ Y) X \cowith | func s => s.1 | func-uniform {D} Du => inP (D, Du, single top, uniform-top, \lam {_} (inP (U,DU,V,_,idp)) => inP (_, inP (U, DU, idp), __.1)) @@ -52,6 +55,17 @@ | func s => s.2 | func-uniform {D} Du => inP (single top, uniform-top, D, Du, \lam {_} (inP (U,_,V,DV,idp)) => inP (_, inP (V, DV, idp), __.2)) + \func tuple {X Y Z : UniformSpace} (f : UniformMap Z X) (g : UniformMap Z Y) : UniformMap Z (X ⨯ Y) \cowith + | func z => (f z, g z) + | func-uniform => \case \elim __ \with { + | inP (C,Cu,D,Du,r) => uniform-refine (uniform-inter (f.func-uniform Cu) (g.func-uniform Du)) \lam {_} (inP (_, inP (U,CU,idp), _, inP (V,DV,idp), idp)) => \case r $ inP (U,CU,V,DV,idp) \with { + | inP (W,EW,p) => inP (_, inP (W, EW, idp), p __) + } + } + + \func prod {X X' Y Y' : UniformSpace} (f : UniformMap X Y) (f' : UniformMap X' Y') : UniformMap (X ⨯ X') (Y ⨯ Y') + => tuple (f ∘ proj1) (f' ∘ proj2) + \lemma prodCover {X Y : UniformSpace} {C : Set (Set X)} (Cu : X.isUniform C) {D : Set (Set Y)} (Du : Y.isUniform D) : isUniform {X ⨯ Y} \lam W => ∃ (U : C) (V : D) (W = \lam s => \Sigma (U s.1) (V s.2)) => uniform-subset {X ⨯ Y} (uniform-inter {X ⨯ Y} (proj1.func-uniform Cu) (proj2.func-uniform Du)) diff --git a/test/Algebra/LinearSolverTest.ard b/test/Algebra/LinearSolverTest.ard index 6c3430c1..bc37c000 100644 --- a/test/Algebra/LinearSolverTest.ard +++ b/test/Algebra/LinearSolverTest.ard @@ -186,6 +186,9 @@ \lemma realTest2 {x : Real} : x = x * ratio 1 2 + x * ratio 1 2 => linarith +\lemma realTest3 {x : Real} (p : 0 < x) : 0 RealAbGroup.< x * ratio 1 2 + => linarith + \lemma ratAlgebraTest {A : OrderedAAlgebra RatField} {x : A} (p : 0 < x) : 0 < x * coefMap (ratio 1 3) => linarith