Grace/Cumulus/FixedPoint/CubeMask.g17

Open in Workbench Download source

Imports

CubeFunctions · Real.Natural · Set.Indicator

Declarations

Source

1-- Points of the cube padded to real sequences and masked by a set of2-- coordinates, the terms of the block sums used to retract onto simplices3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.FixedPoint.CubeMask9import CubeFunctions10import Real.Natural11import Set.Indicator1213-- Two cube functions that agree on the cube share continuity.14theorem CubeFunctionContinuous.congr (g h n : Set)15  requires gFunction : CubeFunction(g, n)16  requires hContinuous : CubeFunctionContinuous(h, n)17  requires agree : ∀ x ∈ unitCube(n), g(x) = h(x)18  shows CubeFunctionContinuous(g, n)19proof20  constructor21  . exact gFunction22  . intros x hx E EReal Epos23    have hAt := CubeFunctionContinuous.at with hContinuous, hx24    obtain ⟨D, DReal, DPos, close⟩ := hAt with EReal, Epos25    witness D26    constructor27    . exact DReal28    . constructor29      . exact DPos30      . intros y hy near31        have gy := agree with hy32        have gx := agree with hx33        rw [gy, gx]34        exact close with hy, near3536-- A point of the cube padded by zero to a real sequence.37def paddedPoint (n x : Set) : Set := x ∪ constantFunction(ℕ ∖ n, ℝ, (0:R))3839theorem naturals.split (n : Nat)40  shows n ∪ (ℕ ∖ n) = ℕ41proof42  ext z43  constructor44  . intro hz45    have split := union2.membership.forward with hz46    cases split with inN | inRest47    . have zNat := natural.member at n with inN48      exact nat.omega.forward with zNat49    . have parts := difference.membership.forward with inRest50      exact parts.left51  . intro hz52    apply union2.membership.backward53    have alternatives : z ∈ n ∨ ¬z ∈ n by tauto54    cases alternatives with inN | notN55    . left56      exact inN57    . right58      exact difference.membership.backward with ⟨hz, notN⟩5960theorem paddedPoint.sequence (n : Nat) (x : Set)61  requires xFunction : x : n → ℝ62  shows RealSequence(paddedPoint(n, x))63proof64  have zeroIn : (0:R) ∈ ℝ by typecheck65  have constant := constantFunction.function at ℕ ∖ n, ℝ, (0:R) with zeroIn66  have disjoint := Disjoint.symmetric with (difference.disjoint at ℕ, n)67  have union := FunctionBetween.union_disjoint with xFunction, constant, disjoint68  have domain := naturals.split at n69  have codomain := union2.idempotent at ℝ70  rw [domain, codomain] at union71  have same : paddedPoint(n, x) = x ∪ constantFunction(ℕ ∖ n, ℝ, (0:R))72    unfold paddedPoint73    rfl74  unfold RealSequence75  rwa same7677theorem paddedPoint.value (n : Nat) (x i : Set)78  requires xFunction : x : n → ℝ79  requires hi : i ∈ n80  shows paddedPoint(n, x)(i) = x(i)81proof82  have zeroIn : (0:R) ∈ ℝ by typecheck83  have constant := constantFunction.function at ℕ ∖ n, ℝ, (0:R) with zeroIn84  have disjoint := Disjoint.symmetric with (difference.disjoint at ℕ, n)85  have same : paddedPoint(n, x) = x ∪ constantFunction(ℕ ∖ n, ℝ, (0:R))86    unfold paddedPoint87    rfl88  rw same89  exact FunctionBetween.union_apply_left with xFunction, constant, disjoint, hi9091-- The i-th term of the sum over S: the coordinate when i ∈ S, else zero.92defgraph maskedPoint (n S x : Set) (i ∈ ℕ) : ℝ := (realNat(indicator(S, i)):R) * (paddedPoint(n, x)(i):R)93requires nNat : Nat(n)94requires xFunction : x : n → ℝ95proof96  have sequence := paddedPoint.sequence with xFunction97  have iNat : Nat(i) by typecheck98  have padded := RealSequence.value at paddedPoint(n, x), i with sequence99  have weightNat := indicator.natural at S, i100  have weight := realNat.real at indicator(S, i)101  exact realMulValue.real at realNat(indicator(S, i)), paddedPoint(n, x)(i)102103theorem maskedPoint.sequence (n : Nat) (S x : Set)104  requires xFunction : x : n → ℝ105  shows RealSequence(maskedPoint(n, S, x))106proof107  exact maskedPoint.function at n, S, x with *108109theorem maskedPoint.coordinate (n : Nat) (S x i : Set)110  requires xFunction : x : n → ℝ111  requires hi : i ∈ n112  shows maskedPoint(n, S, x)(i) = (realNat(indicator(S, i)):R) * (x(i):R)113proof114  have iNat := natural.member at n with hi115  have iIn := nat.omega.forward with iNat116  have value := maskedPoint.value at n, S, x, i with *117  have padded := paddedPoint.value with xFunction, hi118  rw [value, padded]119  rfl120