Grace/Cumulus/Metric/Product.g17

Open in Workbench Download source

Imports

Subspace

Declarations

Source

1-- The product of two metric spaces with the sum metric: its distance2-- function, the metric laws, the projections as Lipschitz maps, balls3-- against products of balls, and bounded products4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Metric.Product10import Subspace1112def productDistance (X d Y e : Set) : Set :=13  { q ∈ ((X × Y) × (X × Y)) × ℝ | ∃ x ∈ X, ∃ y ∈ Y, ∃ a ∈ X, ∃ b ∈ Y,14    q = (((x, y), (a, b)) ↦ realAdd(d(x, a), e(y, b))) }1516theorem productDistance.sum_real (X d Y e x y a b : Set)17  requires metricD : IsMetric(X, d)18  requires metricE : IsMetric(Y, e)19  requires hx : x ∈ X20  requires hy : y ∈ Y21  requires ha : a ∈ X22  requires hb : b ∈ Y23  shows realAdd(d(x, a), e(y, b)) ∈ ℝ24proof25  have dxa := IsMetric.real with metricD, hx, ha26  have eyb := IsMetric.real with metricE, hy, hb27  have sum : d(x, a) + e(y, b) ∈ ℝ by typecheck28  exact sum2930theorem productDistance.relates (X d Y e x y a b : Set)31  requires metricD : IsMetric(X, d)32  requires metricE : IsMetric(Y, e)33  requires hx : x ∈ X34  requires hy : y ∈ Y35  requires ha : a ∈ X36  requires hb : b ∈ Y37  shows relates(productDistance(X, d, Y, e), ((x, y), (a, b)),38    realAdd(d(x, a), e(y, b)))39proof40  have sum := productDistance.sum_real with metricD, metricE, hx, hy, ha, hb41  have first := product.pair at x, y, X, Y with hx, hy42  have second := product.pair at a, b, X, Y with ha, hb43  have pair := product.pair at (x, y), (a, b), X × Y, X × Y with first, second44  have entry := product.pair at ((x, y), (a, b)), realAdd(d(x, a), e(y, b)),45    (X × Y) × (X × Y), ℝ with pair, sum46  unfold relates47  apply productDistance.membership.backward48  refine ⟨entry, x, hx, y, hy, a, ha, b, hb, ?_⟩49  rfl5051theorem productDistance.value_shape (X d Y e q v : Set)52  requires edge : relates(productDistance(X, d, Y, e), q, v)53  shows ∃ x ∈ X, ∃ y ∈ Y, ∃ a ∈ X, ∃ b ∈ Y,54    q = ((x, y), (a, b)) ∧ v = realAdd(d(x, a), e(y, b))55proof56  unfold relates at edge57  obtain ⟨bound, x, hx, y, hy, a, ha, b, hb, shape⟩ :=58    productDistance.membership.forward with edge59  obtain ⟨first, second⟩ := orderedPair.injective with shape60  exact ⟨x, hx, y, hy, a, ha, b, hb, first, second⟩6162theorem productDistance.relation (X d Y e : Set)63  shows RelationBetween(productDistance(X, d, Y, e), (X × Y) × (X × Y), ℝ)64proof65  intros q hq66  have parts := productDistance.membership.forward with hq67  exact parts.left6869theorem productDistance.functional (X d Y e : Set)70  shows Functional(productDistance(X, d, Y, e))71proof72  intros q v first w second73  obtain ⟨x, hx, y, hy, a, ha, b, hb, shapeV, valueV⟩ :=74    productDistance.value_shape with first75  obtain ⟨x2, hx2, y2, hy2, a2, ha2, b2, hb2, shapeW, valueW⟩ :=76    productDistance.value_shape with second77  rw shapeV at shapeW78  obtain ⟨firstPair, secondPair⟩ := orderedPair.injective with shapeW79  obtain ⟨xx, yy⟩ := orderedPair.injective with firstPair80  obtain ⟨aa, bb⟩ := orderedPair.injective with secondPair81  rw [valueV, valueW, xx, yy, aa, bb]82  rfl8384theorem productDistance.total (X d Y e : Set)85  requires metricD : IsMetric(X, d)86  requires metricE : IsMetric(Y, e)87  shows88    ∀ q ∈ (X × Y) × (X × Y), ∃ v ∈ ℝ, relates(productDistance(X, d, Y, e), q, v)89proof90  intros q hq91  obtain ⟨bound, p, hp, p2, hp2, rfl⟩ := product.membership.forward with hq92  obtain ⟨boundP, x, hx, y, hy, rfl⟩ := product.membership.forward with hp93  obtain ⟨boundP2, a, ha, b, hb, rfl⟩ := product.membership.forward with hp294  have sum := productDistance.sum_real with metricD, metricE, hx, hy, ha, hb95  refine ⟨realAdd(d(x, a), e(y, b)), sum, ?_⟩96  exact productDistance.relates with metricD, metricE, hx, hy, ha, hb9798theorem productDistance.function (X d Y e : Set)99  requires metricD : IsMetric(X, d)100  requires metricE : IsMetric(Y, e)101  shows productDistance(X, d, Y, e) : (X × Y) × (X × Y) → ℝ102proof103  constructor104  . exact productDistance.relation at X, d, Y, e105  . constructor106    . exact productDistance.functional at X, d, Y, e107    . exact productDistance.total with metricD, metricE108109theorem productDistance.apply (X d Y e x y a b : Set)110  requires metricD : IsMetric(X, d)111  requires metricE : IsMetric(Y, e)112  requires hx : x ∈ X113  requires hy : y ∈ Y114  requires ha : a ∈ X115  requires hb : b ∈ Y116  shows productDistance(X, d, Y, e)((x, y), (a, b)) = realAdd(d(x, a), e(y, b))117proof118  have function := productDistance.function with metricD, metricE119  have first := product.pair at x, y, X, Y with hx, hy120  have second := product.pair at a, b, X, Y with ha, hb121  have pair := product.pair at (x, y), (a, b), X × Y, X × Y with first, second122  have edge := productDistance.relates with metricD, metricE, hx, hy, ha, hb123  have left := Metric.apply_pair at productDistance(X, d, Y, e), (x, y), (a, b)124  rw ← left125  exact FunctionBetween.apply_value with function, pair, edge126127theorem productDistance.metric (X d Y e : Set)128  requires metricD : IsMetric(X, d)129  requires metricE : IsMetric(Y, e)130  shows IsMetric(X × Y, productDistance(X, d, Y, e))131proof132  constructor133  . exact productDistance.function with metricD, metricE134  . constructor135    . intros p hp q hq136      obtain ⟨boundP, x, hx, y, hy, rfl⟩ := product.membership.forward with hp137      obtain ⟨boundQ, a, ha, b, hb, rfl⟩ := product.membership.forward with hq138      have value := productDistance.apply with metricD, metricE, hx, hy, ha, hb139      rw value140      have dxa := IsMetric.real with metricD, hx, ha141      have eyb := IsMetric.real with metricE, hy, hb142      have nonnegativeD := IsMetric.nonnegative with metricD, hx, ha143      have nonnegativeE := IsMetric.nonnegative with metricE, hy, hb144      linarith145    . constructor146      . intros p hp q hq147        obtain ⟨boundP, x, hx, y, hy, rfl⟩ := product.membership.forward with hp148        obtain ⟨boundQ, a, ha, b, hb, rfl⟩ := product.membership.forward with hq149        have value := productDistance.apply with150          metricD, metricE, hx, hy, ha, hb151        rw value152        have dxa := IsMetric.real with metricD, hx, ha153        have eyb := IsMetric.real with metricE, hy, hb154        have nonnegativeD := IsMetric.nonnegative with metricD, hx, ha155        have nonnegativeE := IsMetric.nonnegative with metricE, hy, hb156        constructor157        . intro zero158          have zeroD : d(x, a) = (0:R) by linarith159          have zeroE : e(y, b) = (0:R) by linarith160          have xa := IsMetric.eq_of_zero with metricD, hx, ha, zeroD161          have yb := IsMetric.eq_of_zero with metricE, hy, hb, zeroE162          rw [xa, yb]163          rfl164        . intro same165          obtain ⟨xa, yb⟩ := orderedPair.injective with same166          rw [xa, yb]167          have selfA := IsMetric.self with metricD, ha168          have selfB := IsMetric.self with metricE, hb169          rw [selfA, selfB]170          linarith171      . constructor172        . intros p hp q hq173          obtain ⟨boundP, x, hx, y, hy, rfl⟩ :=174            product.membership.forward with hp175          obtain ⟨boundQ, a, ha, b, hb, rfl⟩ :=176            product.membership.forward with hq177          have value := productDistance.apply with178            metricD, metricE, hx, hy, ha, hb179          have valueBack := productDistance.apply with180            metricD, metricE, ha, hb, hx, hy181          rw [value, valueBack]182          have symmetricD := IsMetric.symmetric with metricD, hx, ha183          have symmetricE := IsMetric.symmetric with metricE, hy, hb184          rw [symmetricD, symmetricE]185          rfl186        . intros p hp q hq s hs187          obtain ⟨boundP, x, hx, y, hy, rfl⟩ :=188            product.membership.forward with hp189          obtain ⟨boundQ, a, ha, b, hb, rfl⟩ :=190            product.membership.forward with hq191          obtain ⟨boundS, c, hc, g, hg, rfl⟩ :=192            product.membership.forward with hs193          have valuePS := productDistance.apply with194            metricD, metricE, hx, hy, hc, hg195          have valuePQ := productDistance.apply with196            metricD, metricE, hx, hy, ha, hb197          have valueQS := productDistance.apply with198            metricD, metricE, ha, hb, hc, hg199          rw [valuePS, valuePQ, valueQS]200          have triangleD := IsMetric.triangle with metricD, hx, ha, hc201          have triangleE := IsMetric.triangle with metricE, hy, hb, hg202          have dxc := IsMetric.real with metricD, hx, hc203          have dxa := IsMetric.real with metricD, hx, ha204          have dac := IsMetric.real with metricD, ha, hc205          have eyg := IsMetric.real with metricE, hy, hg206          have eyb := IsMetric.real with metricE, hy, hb207          have ebg := IsMetric.real with metricE, hb, hg208          linarith209210-- The projections are 1-Lipschitz, hence continuous.211theorem firstProjection.lipschitz (X d Y e : Set)212  requires metricD : IsMetric(X, d)213  requires metricE : IsMetric(Y, e)214  shows IsLipschitz(firstProjection(X, Y), X × Y, productDistance(X, d, Y, e),215    X, d, (1:R))216proof217  have one : (0:R) ≤ 1 by linarith218  unfold IsLipschitz219  constructor220  . exact firstProjection.function at X, Y221  . constructor222    . exact one223    . intros p hp q hq224      obtain ⟨boundP, x, hx, y, hy, rfl⟩ := product.membership.forward with hp225      obtain ⟨boundQ, a, ha, b, hb, rfl⟩ := product.membership.forward with hq226      have valueP := firstProjection.pair at X, Y, x, y with hx, hy227      have valueQ := firstProjection.pair at X, Y, a, b with ha, hb228      have value := productDistance.apply with metricD, metricE, hx, hy, ha, hb229      rw [valueP, valueQ, value]230      have dxa := IsMetric.real with metricD, hx, ha231      have eyb := IsMetric.real with metricE, hy, hb232      have nonnegativeE := IsMetric.nonnegative with metricE, hy, hb233      have unit := realMulValue.one_left at d(x, a) + e(y, b)234      rw unit235      linarith236237theorem secondProjection.lipschitz (X d Y e : Set)238  requires metricD : IsMetric(X, d)239  requires metricE : IsMetric(Y, e)240  shows IsLipschitz(secondProjection(X, Y), X × Y, productDistance(X, d, Y, e),241    Y, e, (1:R))242proof243  have one : (0:R) ≤ 1 by linarith244  unfold IsLipschitz245  constructor246  . exact secondProjection.function at X, Y247  . constructor248    . exact one249    . intros p hp q hq250      obtain ⟨boundP, x, hx, y, hy, rfl⟩ := product.membership.forward with hp251      obtain ⟨boundQ, a, ha, b, hb, rfl⟩ := product.membership.forward with hq252      have valueP := secondProjection.pair at X, Y, x, y with hx, hy253      have valueQ := secondProjection.pair at X, Y, a, b with ha, hb254      have value := productDistance.apply with metricD, metricE, hx, hy, ha, hb255      rw [valueP, valueQ, value]256      have dxa := IsMetric.real with metricD, hx, ha257      have eyb := IsMetric.real with metricE, hy, hb258      have nonnegativeD := IsMetric.nonnegative with metricD, hx, ha259      have unit := realMulValue.one_left at d(x, a) + e(y, b)260      rw unit261      linarith262263theorem firstProjection.metric_continuous (X d Y e : Set)264  requires metricD : IsMetric(X, d)265  requires metricE : IsMetric(Y, e)266  shows IsMetricContinuous(firstProjection(X, Y), X × Y,267    productDistance(X, d, Y, e), X, d)268proof269  have product := productDistance.metric with metricD, metricE270  have lipschitz := firstProjection.lipschitz with metricD, metricE271  exact IsLipschitz.continuous with product, metricD, lipschitz272273theorem secondProjection.metric_continuous (X d Y e : Set)274  requires metricD : IsMetric(X, d)275  requires metricE : IsMetric(Y, e)276  shows IsMetricContinuous(secondProjection(X, Y), X × Y,277    productDistance(X, d, Y, e), Y, e)278proof279  have product := productDistance.metric with metricD, metricE280  have lipschitz := secondProjection.lipschitz with metricD, metricE281  exact IsLipschitz.continuous with product, metricE, lipschitz282283-- Balls in the product against products of balls.284theorem productDistance.ball_subset_product (X d Y e x y : Set, r : Real)285  requires metricD : IsMetric(X, d)286  requires metricE : IsMetric(Y, e)287  requires hx : x ∈ X288  requires hy : y ∈ Y289  shows ball(X × Y, productDistance(X, d, Y, e), (x, y), r) ⊆290    ball(X, d, x, r) × ball(Y, e, y, r)291proof292  intros q hq293  have hqP := ball.point with hq294  have near := ball.distance with hq295  obtain ⟨boundQ, a, ha, b, hb, rfl⟩ := product.membership.forward with hqP296  have value := productDistance.apply with metricD, metricE, hx, hy, ha, hb297  rw value at near298  have dxa := IsMetric.real with metricD, hx, ha299  have eyb := IsMetric.real with metricE, hy, hb300  have nonnegativeD := IsMetric.nonnegative with metricD, hx, ha301  have nonnegativeE := IsMetric.nonnegative with metricE, hy, hb302  have nearA : d(x, a) < r by linarith303  have nearB : e(y, b) < r by linarith304  apply product.pair305  . exact ball.of_distance with ha, nearA306  . exact ball.of_distance with hb, nearB307308theorem productDistance.product_subset_ball (X d Y e x y : Set, r s : Real)309  requires metricD : IsMetric(X, d)310  requires metricE : IsMetric(Y, e)311  requires hx : x ∈ X312  requires hy : y ∈ Y313  shows ball(X, d, x, r) × ball(Y, e, y, s) ⊆314    ball(X × Y, productDistance(X, d, Y, e), (x, y), r + s)315proof316  intros q hq317  obtain ⟨boundQ, a, ha, b, hb, rfl⟩ := product.membership.forward with hq318  have haX := ball.point with ha319  have hbY := ball.point with hb320  have nearA := ball.distance with ha321  have nearB := ball.distance with hb322  have value := productDistance.apply with metricD, metricE, hx, hy, haX, hbY323  have member := product.pair at a, b, X, Y with haX, hbY324  apply ball.of_distance with member325  rw value326  have dxa := IsMetric.real with metricD, hx, haX327  have eyb := IsMetric.real with metricE, hy, hbY328  linarith329330theorem IsBounded.product (X d Y e S T : Set)331  requires metricD : IsMetric(X, d)332  requires metricE : IsMetric(Y, e)333  requires boundedS : IsBounded(X, d, S)334  requires boundedT : IsBounded(Y, e, T)335  shows IsBounded(X × Y, productDistance(X, d, Y, e), S × T)336proof337  obtain ⟨insideS, r, hr, boundS⟩ := boundedS338  obtain ⟨insideT, s, hs, boundT⟩ := boundedT339  have typedR : Real(r) by exact hr340  have typedS : Real(s) by exact hs341  apply IsBounded.of_bound at342    X × Y, productDistance(X, d, Y, e), S × T, r + s with343    (product.monotone with insideS, insideT)344  intros p hp q hq345  obtain ⟨boundP, x, hx, y, hy, rfl⟩ := product.membership.forward with hp346  obtain ⟨boundQ, a, ha, b, hb, rfl⟩ := product.membership.forward with hq347  have hxX := insideS with x, hx348  have haX := insideS with a, ha349  have hyY := insideT with y, hy350  have hbY := insideT with b, hb351  have value := productDistance.apply with metricD, metricE, hxX, hyY, haX, hbY352  rw value353  have dxa := IsMetric.real with metricD, hxX, haX354  have eyb := IsMetric.real with metricE, hyY, hbY355  have estimateD := boundS with x, hx, a, ha356  have estimateE := boundT with y, hy, b, hb357  linarith358