Carleson/TileStructure.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

94 declarations, 0 contain sorry, 0 declared as axioms

Stack sizes
Imports (1)
Imported by 7 files
  1. class PreTileStructure The data in a tile structure, and some basic properties line 19 source

    Source comment

    The data in a tile structure, and some basic properties. This is mostly separated out so that we can nicely define the notation `d_𝔭`. Note: compose `π“˜` with `Grid` to get the `π“˜` of the paper.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: RCLike, outParam, NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, FunctionDistances, MeasureTheory.SimpleFunc, FunctionDistances.Θ, Nat, Real

    6 instances, coercions and auxiliary constants left out.

    class PreTileStructure {A : outParam ℝβ‰₯0} [PseudoMetricSpace X] [DoublingMeasure X A]
  [FunctionDistances π•œ X] (Q : outParam (SimpleFunc X (Θ X)))
  (D : outParam β„•) (ΞΊ : outParam ℝ) (S : outParam β„•) (o : outParam X)
  extends GridStructure X D ΞΊ S o where
…

    Mentions: A, FunctionDistances, GridStructure

  2. def 𝔓 line 36 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: RCLike, NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, FunctionDistances, MeasureTheory.SimpleFunc, FunctionDistances.Θ, PreTileStructure

    Proof uses: PreTileStructure.𝔓

    12 instances, coercions and auxiliary constants left out.

  3. instance (instance at line 38) line 38 source
  4. def π“˜ line 40 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: RCLike, NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, FunctionDistances, MeasureTheory.SimpleFunc, FunctionDistances.Θ, PreTileStructure, 𝔓, Grid

    Proof uses: PreTileStructure.π“˜

    13 instances, coercions and auxiliary constants left out.

  5. lemma surjective_π“˜ line 42 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: RCLike, NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, FunctionDistances, MeasureTheory.SimpleFunc, FunctionDistances.Θ, PreTileStructure, Function.Surjective, 𝔓, Grid, π“˜

    Proof uses: PreTileStructure.surjective_π“˜

    13 instances, coercions and auxiliary constants left out.

  6. instance (instance at line 44) line 44 source
  7. def 𝔠 line 46 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: RCLike, NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, FunctionDistances, MeasureTheory.SimpleFunc, FunctionDistances.Θ, PreTileStructure, 𝔓

    Proof uses: c, π“˜

    13 instances, coercions and auxiliary constants left out.

  8. def 𝔰 line 47 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: RCLike, NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, FunctionDistances, MeasureTheory.SimpleFunc, FunctionDistances.Θ, PreTileStructure, 𝔓, Int

    Proof uses: s, π“˜

    13 instances, coercions and auxiliary constants left out.

  9. class TileStructure A tile structure line 54 source

    Source documentation

    A tile structure.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: outParam, NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, FunctionDistances, Real, MeasureTheory.SimpleFunc, FunctionDistances.Θ, Nat

    5 instances, coercions and auxiliary constants left out.

    class TileStructure {A : outParam ℝβ‰₯0} [PseudoMetricSpace X] [DoublingMeasure X A]
    [FunctionDistances ℝ X] (Q : outParam (SimpleFunc X (Θ X)))
    (D : outParam β„•) (ΞΊ : outParam ℝ) (S : outParam β„•) (o : outParam X)
    extends PreTileStructure Q D ΞΊ S o where
…

    Mentions: A, FunctionDistances, PreTileStructure

  10. lemma dist_π“˜ line 85 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, FunctionDistances.Θ, 𝔓, Eq, Dist.dist, WithFunctionDistance and 8 more

    Proof uses: rfl

    60 instances, coercions and auxiliary constants left out.

  11. lemma nndist_π“˜ line 86 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, FunctionDistances.Θ, 𝔓, Eq, NNDist.nndist, WithFunctionDistance and 8 more

    Proof uses: rfl

    60 instances, coercions and auxiliary constants left out.

  12. lemma ball_π“˜ line 87 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, FunctionDistances.Θ, 𝔓, Eq, WithFunctionDistance, c and 8 more

    Proof uses: rfl

    58 instances, coercions and auxiliary constants left out.

  13. lemma cball_subset line 89 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, WithFunctionDistance, 𝔠, HDiv.hDiv and 7 more

    Proof uses: TileStructure.cball_subset

    38 instances, coercions and auxiliary constants left out.

  14. lemma subset_cball line 90 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, FunctionDistances.Θ, TileStructure.Ξ©, Metric.ball and 7 more

    Proof uses: TileStructure.subset_cball

    42 instances, coercions and auxiliary constants left out.

  15. lemma ball_eq_of_grid_eq line 93 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Eq, Grid, π“˜ and 7 more

    Proof uses: Eq.mpr, c, s, id, congrArg, Eq.symm, ball_π“˜, Eq.refl

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  16. lemma cball_disjoint line 96 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Ne, Eq, Grid, π“˜ and 10 more

    Proof uses: Set.disjoint_of_subset, TileStructure.Ξ©, cball_subset, TileStructure.disjoint_Ξ©

    61 instances, coercions and auxiliary constants left out.

  17. lemma volume_xDsp_bound A bound used in both nontrivial cases of Lemma 7.5.5 line 101 source

    Source documentation

    A bound used in both nontrivial cases of Lemma 7.5.5.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, Grid, π“˜, LE.le and 10 more

    Proof uses: ENNReal.div_le_of_le_mul', HAdd.hAdd, Dist.dist, Trans.trans, Eq, add_le_add, LT.lt.le, GridStructure.c, GridStructure.s, Iff.mp, LT.lt, Metric.mem_ball, GridStructure.Grid_subset_ball, le_refl, Eq.mpr, id, congrArg, Eq.symm, add_mul, of_eq_true and 37 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

    lemma volume_xDsp_bound {x : X} (hx : x ∈ π“˜ p) :
    volume (ball (𝔠 p) (4 * D ^ 𝔰 p)) / 2 ^ (3 * a) ≀ volume (ball x (D ^ 𝔰 p)) := by
…

    Mentions: π“˜, 𝔠, 𝔰

  18. lemma volume_xDsp_bound_4 A bound used in Lemma 7.6.2 line 114 source

    Source documentation

    A bound used in Lemma 7.6.2.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, Grid, π“˜, LE.le and 10 more

    Proof uses: ENNReal.div_le_of_le_mul', HAdd.hAdd, Dist.dist, Trans.trans, add_le_add, LT.lt.le, GridStructure.c, GridStructure.s, Iff.mp, LT.lt, Metric.mem_ball, GridStructure.Grid_subset_ball, le_refl, Eq.mpr, id, Eq, congrArg, Eq.symm, add_mul, mul_le_mul_of_nonneg_right and 35 more

    146 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

    Open to load the checked before-and-after goal states.

    lemma volume_xDsp_bound_4 {x : X} (hx : x ∈ π“˜ p) :
    volume (ball (𝔠 p) (8 * D ^ 𝔰 p)) / 2 ^ (4 * a) ≀ volume (ball x (D ^ 𝔰 p)) := by
…

    Mentions: π“˜, 𝔠, 𝔰

  19. def E The set E defined in Proposition 2.0.2 line 127 source

    Source documentation

    The set E defined in Proposition 2.0.2.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, Grid, π“˜, FunctionDistances.Θ, TileStructure.Ξ©, MeasureTheory.SimpleFunc, Set.Icc, 𝔰

    42 instances, coercions and auxiliary constants left out.

    def E (p : 𝔓 X) : Set X :=
…

    Mentions: 𝔓

  20. lemma E_subset_π“˜ line 130 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, E, π“˜

    Proof uses: Set.mem_of_mem_inter_left, And, Membership.mem, FunctionDistances.Θ, TileStructure.Ξ©, MeasureTheory.SimpleFunc, Set.Icc, 𝔰

    45 instances, coercions and auxiliary constants left out.

  21. lemma Q_mem_Ξ© line 132 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, E, FunctionDistances.Θ, TileStructure.Ξ© and 1 more

    Proof uses: And.left, Set.Icc, 𝔰, And.right, Grid, π“˜, And

    52 instances, coercions and auxiliary constants left out.

  22. lemma disjoint_E line 134 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Ne, Eq, Grid, π“˜ and 2 more

    Proof uses: FunctionDistances.Θ, TileStructure.Ξ©, TileStructure.disjoint_Ξ©, Mathlib.Tactic.Contrapose.contrapose₁, Not, Eq.mpr, Exists, And, Membership.mem, id, congrArg, propext, Set.not_disjoint_iff, Eq.mp, Exists.intro, MeasureTheory.SimpleFunc, And.intro, Q_mem_Ξ©

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  23. lemma measurableSet_E line 139 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, MeasurableSet, E

    Proof uses: Measurable.setOf, And, Membership.mem, Grid, π“˜, FunctionDistances.Θ, TileStructure.Ξ©, MeasureTheory.SimpleFunc, Set.Icc, 𝔰, Measurable.and, Eq.mpr, Measurable, Set.ofPred, id, Eq, congrArg, Eq.symm, propext, measurableSet_setOfPred and 15 more

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

  24. lemma volume_E_lt_top line 148 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LT.lt, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume and 2 more

    Proof uses: Trans.trans, LE.le, π“˜, MeasureTheory.measure_mono, E_subset_π“˜, volume_coeGrid_lt_top

    45 instances, coercions and auxiliary constants left out.

  25. def TileLike line 151 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt

    Proof uses: Prod, Grid, OrderDual, FunctionDistances.Θ

    28 instances, coercions and auxiliary constants left out.

  26. def TileLike.fst line 153 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, TileLike, Grid

    Proof uses: Prod.fst, OrderDual, FunctionDistances.Θ

    30 instances, coercions and auxiliary constants left out.

  27. def TileLike.snd line 154 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileLike, FunctionDistances.Θ

    Proof uses: Prod.snd, Grid, OrderDual

    32 instances, coercions and auxiliary constants left out.

  28. lemma TileLike.fst_mk line 156 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, FunctionDistances.Θ, Eq, TileLike.fst, Prod.mk and 1 more

    Proof uses: Eq.refl

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  29. lemma TileLike.snd_mk line 157 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, FunctionDistances.Θ, Eq, TileLike.snd, Prod.mk and 1 more

    Proof uses: Eq.refl

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  30. instance (instance at line 159) line 159 source
  31. lemma TileLike.le_def line 162 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, TileLike, Iff, LE.le, And, Grid and 3 more

    Proof uses: Iff.rfl

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  32. def toTileLike line 164 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, TileLike

    Proof uses: Prod.mk, Grid, OrderDual, FunctionDistances.Θ, π“˜, TileStructure.Ξ©

    29 instances, coercions and auxiliary constants left out.

  33. lemma toTileLike_fst line 166 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, Grid, TileLike.fst, toTileLike and 1 more

    Proof uses: Eq.refl

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  34. lemma toTileLike_snd line 167 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, FunctionDistances.Θ, TileLike.snd, toTileLike and 1 more

    Proof uses: Eq.refl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  35. def smul This is not defined as such in the blueprint, but Ξ»p ≲ Ξ»'p' can be written using smul l p ≀ smul l' p' line 172 source

    Source documentation

    This is not defined as such in the blueprint, but Ξ»p ≲ Ξ»'p' can be written using smul l p ≀ smul l' p'. Beware: smul 1 p is very different from toTileLike p.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, TileLike

    Proof uses: Prod.mk, Grid, OrderDual, FunctionDistances.Θ, π“˜, Metric.ball, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, OfNat.ofNat, PreTileStructure.𝒬

    39 instances, coercions and auxiliary constants left out.

    def smul (l : ℝ) (p : 𝔓 X) : TileLike X :=
…

    Mentions: 𝔓, TileLike

  36. lemma smul_fst line 175 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, Grid, TileLike.fst, smul and 1 more

    Proof uses: Eq.refl

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  37. lemma smul_snd line 176 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, FunctionDistances.Θ, TileLike.snd, smul and 8 more

    Proof uses: Eq.refl

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  38. lemma smul_mono_left line 179 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, TileLike, smul

    Proof uses: of_eq_true, Eq.trans, And, Grid, TileLike.fst, FunctionDistances.Θ, TileLike.snd, True, congr, congrArg, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, π“˜, smul_fst, Metric.ball, WithFunctionDistance, 𝔠, HDiv.hDiv and 4 more

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  39. lemma smul_le_toTileLike line 183 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, TileLike, smul, OfNat.ofNat and 1 more

    Proof uses: of_eq_true, Eq.trans, And, Grid, TileLike.fst, FunctionDistances.Θ, TileLike.snd, True, congr, congrArg, HPow.hPow, HMul.hMul, 𝕔, π“˜, smul_fst, toTileLike_fst, TileStructure.Ξ©, Metric.ball, WithFunctionDistance, 𝔠 and 8 more

    62 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  40. lemma toTileLike_le_smul line 187 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, TileLike, toTileLike, smul and 2 more

    Proof uses: of_eq_true, Eq.trans, And, Grid, TileLike.fst, FunctionDistances.Θ, TileLike.snd, True, congr, congrArg, HPow.hPow, HMul.hMul, 𝕔, π“˜, toTileLike_fst, smul_fst, Metric.ball, WithFunctionDistance, 𝔠, HDiv.hDiv and 8 more

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  41. lemma 𝒬_mem_Ξ© line 190 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, FunctionDistances.Θ, TileStructure.Ξ©, PreTileStructure.𝒬

    Proof uses: cball_subset, Metric.mem_ball_self, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, OfNat.ofNat, Inv.inv, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_inv_pos, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true

    59 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  42. lemma 𝒬_inj line 192 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, FunctionDistances.Θ, PreTileStructure.𝒬, Grid and 1 more

    Proof uses: Mathlib.Tactic.Contrapose.contrapose₁, id, Not, Ne, Iff.mpr, Disjoint, TileStructure.Ξ©, Exists, And, Membership.mem, Set.not_disjoint_iff, Exists.intro, And.intro, 𝒬_mem_Ξ©, Eq.rec, Eq.symm, TileStructure.disjoint_Ξ©

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  43. lemma toTileLike_injective line 197 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Function.Injective, 𝔓, TileLike, toTileLike

    Proof uses: Eq, Classical.byContradiction, Not, Disjoint, FunctionDistances.Θ, TileStructure.Ξ©, TileStructure.disjoint_Ξ©, And.left, Grid, π“˜, OrderDual, Eq.mp, Prod, Prod.mk, And, EmptyCollection.emptyCollection, id, HPow.hPow, OfNat.ofNat, HMul.hMul and 11 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  44. instance (instance at line 205) line 205 source
  45. lemma 𝔓.le_def line 207 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Iff, LE.le, TileLike, toTileLike

    Proof uses: Iff.rfl

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  46. lemma 𝔓.le_def' line 208 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Iff, LE.le, And, Grid and 3 more

    Proof uses: Iff.rfl

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  47. lemma tile_le_of_cube_le_and_not_disjoint Deduce an inclusion of tiles from an inclusion of their cubes and non-disjointness of their Ξ©s line 212 source

    Source documentation

    Deduce an inclusion of tiles from an inclusion of their cubes and non-disjointness of their Ξ©s.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, Grid, π“˜, FunctionDistances.Θ and 2 more

    Proof uses: And.intro, Prod.fst, OrderDual, toTileLike, Prod.snd, Or.resolve_left, Disjoint, TileStructure.relative_fundamental_dyadic, Iff.mpr, Not, Exists, And, Set.not_disjoint_iff, Exists.intro

    62 instances, coercions and auxiliary constants left out.

    lemma tile_le_of_cube_le_and_not_disjoint {p q : 𝔓 X} (hi : π“˜ p ≀ π“˜ q)
    {x : Θ X} (mxp : x ∈ Ξ© p) (mxq : x ∈ Ξ© q) : p ≀ q :=
…

    Mentions: 𝔓, π“˜, Ξ©

  48. lemma dist_𝒬_lt_one_of_le line 216 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, LT.lt, Dist.dist, WithFunctionDistance and 6 more

    Proof uses: LE.le.trans, Metric.ball, Inv.inv, Prod.snd, Grid, OrderDual, FunctionDistances.Θ, toTileLike, TileStructure.Ω, cball_subset, And.right, Prod.fst, subset_cball, Metric.mem_ball_self, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_inv_pos, Eq.refl and 3 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  49. lemma dist_𝒬_lt_one_of_le' line 219 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, LT.lt, Dist.dist, WithFunctionDistance and 6 more

    Proof uses: Iff.mp, Membership.mem, Metric.ball, Metric.mem_ball', dist_𝒬_lt_one_of_le

    63 instances, coercions and auxiliary constants left out.

  50. lemma π“˜_strictMono line 222 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, StrictMono, 𝔓, Grid, π“˜

    Proof uses: LT.lt, LE.le.lt_of_ne, Prod.fst, OrderDual, FunctionDistances.Θ, toTileLike, And.left, LE.le, Prod.snd, LT.lt.le, Eq, Iff.mp, Disjoint, TileStructure.Ξ©, Membership.mem, Not, Set.disjoint_left, TileStructure.disjoint_Ξ©, LT.lt.ne, PreTileStructure.𝒬 and 2 more

    52 instances, coercions and auxiliary constants left out.

  51. lemma smul_mono Lemma 5.3.1 line 226 source

    Source documentation

    Lemma 5.3.1

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, TileLike, smul

    Proof uses: LE.le.trans, smul_mono_left

    32 instances, coercions and auxiliary constants left out.

    lemma smul_mono {m m' n n' : ℝ} (hp : smul n p ≀ smul m p') (hm : m' ≀ m) (hn : n ≀ n') :
    smul n' p ≀ smul m' p' :=
…

    Mentions: smul

  52. lemma smul_C2_1_2 Lemma 5.3.2 (generalizing 1 to k > 0) line 232 source

    Source documentation

    Lemma 5.3.2 (generalizing 1 to k > 0)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LT.lt, OfNat.ofNat, Ne, Grid and 7 more

    Proof uses: LE.le.lt_of_ne, Prod.fst, OrderDual, FunctionDistances.Θ, And.left, Prod.snd, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, Metric.ball, PreTileStructure.𝒬, Membership.mem, Eq.mpr, Dist.dist, id, Eq, congrArg, propext and 33 more

    109 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

    lemma smul_C2_1_2 (m : ℝ) {n k : ℝ} (hk : 0 < k) (hp : π“˜ p β‰  π“˜ p') (hl : smul n p ≀ smul k p') :
    smul (n + C2_1_2 a * m) p ≀ smul m p' := by
…

    Mentions: k, π“˜, smul

  53. lemma dist_LTSeries line 248 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LTSeries, Membership.mem, Eq, RelSeries.length and 17 more

    Proof uses: Nat.recAux, Eq.mpr, id, congrArg, pow_zero, one_mul, Grid.dist_mono, Prod.fst, Grid, OrderDual, toTileLike, And.left, Prod.snd, LTSeries.head_le_last, HAdd.hAdd, RelSeries.eraseLast, Grid.dist_strictMono, π“˜, π“˜_strictMono, RelSeries.eraseLast_last_rel_last and 25 more

    145 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

    Open to load the checked before-and-after goal states.

  54. def C5_3_3 The constraint on Ξ» in the first part of Lemma 5.3.3 line 262 source

    Source documentation

    The constraint on Ξ» in the first part of Lemma 5.3.3.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real

    Proof uses: Inv.inv, HSub.hSub, OfNat.ofNat, C2_1_2

    5 instances, coercions and auxiliary constants left out.

    def C5_3_3 (a : β„•) : ℝ := (1 - C2_1_2 a)⁻¹
…
  55. lemma C5_3_3_le line 265 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, LE.le, C5_3_3, HDiv.hDiv, OfNat.ofNat

    Proof uses: Eq.mpr, Inv.inv, HSub.hSub, C2_1_2, id, Eq, congrArg, C5_3_3.eq_1, propext, inv_le_commβ‚€, Iff.mpr, LT.lt, sub_pos, HAdd.hAdd, C2_1_2_lt_one, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div and 17 more

    96 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  56. lemma wiggle_order_11_10 Lemma 5.3.3, Equation (5.3.3) line 272 source

    Source documentation

    Lemma 5.3.3, Equation (5.3.3)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, C5_3_3, TileLike, smul

    Proof uses: Eq, Grid, π“˜, Ne, Or, eq_or_ne, le_refl, absurd, LT.lt.ne, π“˜_strictMono, lt_of_le_of_ne, Trans.trans, HAdd.hAdd, OfNat.ofNat, HMul.hMul, C2_1_2, smul_mono_left, Eq.mpr, HSub.hSub, id and 95 more

    140 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

    Open to load the checked before-and-after goal states.

    lemma wiggle_order_11_10 {n : ℝ} (hp : p ≀ p') (hn : C5_3_3 a ≀ n) : smul n p ≀ smul n p' := by
…

    Mentions: C5_3_3, smul

  57. lemma wiggle_order_100 Lemma 5.3.3, Equation (5.3.4) line 286 source

    Source documentation

    Lemma 5.3.3, Equation (5.3.4)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, TileLike, smul, OfNat.ofNat and 3 more

    Proof uses: Trans.trans, HAdd.hAdd, HMul.hMul, C2_1_2, smul_mono_left, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Ring and 76 more

    118 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    lemma wiggle_order_100 (hp : smul 10 p ≀ smul 1 p') (hn : π“˜ p β‰  π“˜ p') :
    smul 100 p ≀ smul 100 p' :=
…

    Mentions: smul, π“˜

  58. lemma wiggle_order_500 Lemma 5.3.3, Equation (5.3.5) line 294 source

    Source documentation

    Lemma 5.3.3, Equation (5.3.5)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, TileLike, smul, OfNat.ofNat and 3 more

    Proof uses: Trans.trans, HAdd.hAdd, HMul.hMul, C2_1_2, smul_mono_left, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Ring and 76 more

    118 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    lemma wiggle_order_500 (hp : smul 2 p ≀ smul 1 p') (hn : π“˜ p β‰  π“˜ p') :
    smul 4 p ≀ smul 500 p' :=
…

    Mentions: smul, π“˜

  59. def C5_3_2 line 301 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real

    Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, Neg.neg

    10 instances, coercions and auxiliary constants left out.

  60. def TileLike.toTile line 303 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileLike, Prod, FunctionDistances.Θ

    Proof uses: SProd.sprod, TileLike.fst, TileLike.snd

    34 instances, coercions and auxiliary constants left out.

  61. def TileLike.toSet From a TileLike, we can construct a set line 307 source

    Source documentation

    From a TileLike, we can construct a set. This is used in the definitions E₁ and Eβ‚‚.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, TileLike

    Proof uses: Inter.inter, TileLike.fst, Set.preimage, FunctionDistances.Θ, MeasureTheory.SimpleFunc, TileLike.snd

    34 instances, coercions and auxiliary constants left out.

    def TileLike.toSet (t : TileLike X) : Set X :=
…

    Mentions: TileLike

  62. def E₁ line 310 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: TileLike.toSet, toTileLike

    24 instances, coercions and auxiliary constants left out.

  63. def Eβ‚‚ line 313 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: TileLike.toSet, smul

    24 instances, coercions and auxiliary constants left out.

  64. lemma E₁_subset line 316 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, E₁, π“˜

    Proof uses: id, Eq.mpr, Inter.inter, Set.preimage, FunctionDistances.Θ, MeasureTheory.SimpleFunc, TileStructure.Ω, Eq, congrArg, Set.inter_assoc, Set.inter_subset_left

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  65. lemma Eβ‚‚_subset line 321 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, Eβ‚‚, π“˜

    Proof uses: id, Eq.mpr, Inter.inter, Set.preimage, FunctionDistances.Θ, MeasureTheory.SimpleFunc, Metric.ball, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, OfNat.ofNat, PreTileStructure.𝒬, Eq, congrArg, Set.inter_assoc, Set.inter_subset_left

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  66. lemma Eβ‚‚_mono line 326 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Monotone, Eβ‚‚

    Proof uses: LE.le, id, TileLike.toSet, smul, Eq.mpr, Inter.inter, TileLike.fst, Set.preimage, FunctionDistances.Θ, MeasureTheory.SimpleFunc, TileLike.snd, Eq, congr, congrArg, Set.inter_assoc, Set.inter_subset_inter_right, Set.preimage_mono, Metric.ball, WithFunctionDistance, 𝔠 and 7 more

    63 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  67. def lowerCubes 𝔓(𝔓') in the blueprint line 333 source

    Source documentation

    𝔓(𝔓') in the blueprint. The set of all tiles whose cubes are less than the cube of some tile in the given set.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, Exists, And, Membership.mem, LE.le, Grid, π“˜

    29 instances, coercions and auxiliary constants left out.

    def lowerCubes (𝔓' : Set (𝔓 X)) : Set (𝔓 X) :=
…

    Mentions: 𝔓

  68. lemma mem_lowerCubes line 336 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Iff, Membership.mem, lowerCubes, Exists and 4 more

    Proof uses: Iff.rfl

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  69. lemma lowerCubes_mono line 338 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Monotone, 𝔓, lowerCubes

    Proof uses: LE.le, Membership.mem, Eq.mpr, Set.ofPred, Exists, And, Grid, π“˜, id, Eq, congrArg, lowerCubes.eq_1, propext, Set.mem_ofPred, Eq.mp, Exists.intro, And.intro

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  70. lemma subset_lowerCubes line 341 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, lowerCubes

    Proof uses: Membership.mem, Eq.mpr, Set.ofPred, Exists, And, Grid, π“˜, id, Eq, congrArg, lowerCubes.eq_1, propext, Set.mem_ofPred, Exists.intro, And.intro, le_refl

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  71. def dens₁ This density is defined to live in ℝβ‰₯0∞ line 345 source

    Source documentation

    This density is defined to live in ℝβ‰₯0∞. Use ENNReal.toReal to get a real number.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, ENNReal

    Proof uses: iSup, Membership.mem, GE.ge, OfNat.ofNat, HMul.hMul, HPow.hPow, Neg.neg, lowerCubes, LE.le, TileLike, smul, HDiv.hDiv, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Eβ‚‚, π“˜

    58 instances, coercions and auxiliary constants left out.

    def dens₁ (𝔓' : Set (𝔓 X)) : ℝβ‰₯0∞ :=
…

    Mentions: 𝔓

  72. lemma dens₁_mono line 350 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, ENNReal, dens₁

    Proof uses: Eq.mpr, Membership.mem, GE.ge, OfNat.ofNat, HMul.hMul, HPow.hPow, Neg.neg, iSup, lowerCubes, TileLike, smul, HDiv.hDiv, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Eβ‚‚, π“˜, id, Eq, Eq.trans, forall_congr and 37 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

    Open to load the checked before-and-after goal states.

  73. def densβ‚‚ This density is defined to live in ℝβ‰₯0∞ line 367 source

    Source documentation

    This density is defined to live in ℝβ‰₯0∞. Use ENNReal.toReal to get a real number.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, ENNReal

    Proof uses: iSup, Membership.mem, GE.ge, HMul.hMul, OfNat.ofNat, HPow.hPow, 𝔰, HDiv.hDiv, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Inter.inter, Metric.ball, 𝔠

    50 instances, coercions and auxiliary constants left out.

    def densβ‚‚ (𝔓' : Set (𝔓 X)) : ℝβ‰₯0∞ :=
…

    Mentions: 𝔓

  74. lemma le_densβ‚‚ line 371 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, GE.ge, HMul.hMul, OfNat.ofNat and 11 more

    Proof uses: le_trans, iSup, le_iSupβ‚‚

    79 instances, coercions and auxiliary constants left out.

  75. lemma densβ‚‚_eq_biSup_densβ‚‚ line 376 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, ENNReal, densβ‚‚, iSup and 2 more

    Proof uses: of_eq_true, Eq.trans, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, LE.le, 𝔰, HDiv.hDiv, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Inter.inter, Metric.ball, 𝔠, True, congr, congrArg, GE.ge, funext, iSup_congr_Prop and 6 more

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  76. lemma dens₁_le_one A rough estimate line 381 source

    Source comment

    A rough estimate. It's also less than 2 ^ (-a)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, ENNReal, dens₁, OfNat.ofNat

    Proof uses: Eq.mpr, HMul.hMul, id, Eq, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, mul_one, Membership.mem, GE.ge, HPow.hPow, Neg.neg, iSup, And, Grid, π“˜, TileLike, smul and 39 more

    120 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

    Open to load the checked before-and-after goal states.

    lemma dens₁_le_one {𝔓' : Set (𝔓 X)} : dens₁ 𝔓' ≀ 1 := by
…

    Mentions: 𝔓, dens₁

  77. lemma volume_Eβ‚‚_le_dens₁_mul_volume line 399 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, lowerCubes, LE.le, OfNat.ofNat and 10 more

    Proof uses: Ne, LT.lt.ne', volume_coeGrid_pos, defaultD_pos, Eq.mpr, HDiv.hDiv, id, Eq, congrArg, Eq.symm, propext, ENNReal.div_le_iff_le_mul, Or.inl, Top.top, LT.lt.ne, volume_coeGrid_lt_top, ENNReal.rpow_natCast, Neg.neg, neg_neg, Inv.inv and 41 more

    157 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  78. def stackSize The number of tiles p in s whose underlying cube π“˜ p contains x line 416 source

    Source documentation

    The number of tiles p in s whose underlying cube π“˜ p contains x.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator, π“˜, OfNat.ofNat

    34 instances, coercions and auxiliary constants left out.

    def stackSize (C : Set (𝔓 X)) (x : X) : β„• :=
…

    Mentions: 𝔓

  79. lemma stackSize_setOf_add_stackSize_setOf_not line 419 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, HAdd.hAdd, stackSize, Set.ofPred and 3 more

    Proof uses: id, Eq.mpr, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, Set.indicator, π“˜, OfNat.ofNat, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, Finset.sum_filter_add_sum_filter_not, congr, Finset.sum_congr, Finset.filter_filter, Finset, HAdd and 4 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  80. lemma stackSize_inter_add_stackSize_sdiff line 427 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, HAdd.hAdd, stackSize, Inter.inter and 1 more

    Proof uses: stackSize_setOf_add_stackSize_setOf_not, Membership.mem

    29 instances, coercions and auxiliary constants left out.

  81. lemma stackSize_sdiff_eq line 431 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, stackSize, SDiff.sdiff, HSub.hSub and 1 more

    Proof uses: Nat.eq_sub_of_add_eq', stackSize_inter_add_stackSize_sdiff

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  82. lemma stackSize_congr line 435 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, Iff, π“˜, Eq and 1 more

    Proof uses: Finset.sum_congr, Finset.filter, Classical.propDecidable, Finset.univ, Set.indicator, OfNat.ofNat, rfl, Finset, id, Eq.mpr, ite, Classical.decPred, congrFun', congrArg, ite_congr, propext, Eq.mp, Finset.mem_filter_univ, Eq.refl, Not and 5 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  83. lemma stackSize_mono line 443 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, stackSize

    Proof uses: Finset.sum_le_sum_of_subset, Set.indicator, π“˜, OfNat.ofNat, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, of_eq_true, HPow.hPow, HMul.hMul, 𝕔, Finset, Eq.trans, True, implies_congr, And, congrFun', congrArg, true_and and 2 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  84. lemma stackSize_real Simplify the cast of stackSize C x from β„• to ℝ line 450 source

    Source comment

    Simplify the cast of `stackSize C x` from `β„•` to `ℝ`

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, stackSize, Finset.sum, Finset.filter and 6 more

    Proof uses: Eq.mpr, id, congrArg, stackSize.eq_1, Nat.cast_sum, Finset.sum_congr, rfl, Finset, dite, of_eq_true, Eq.trans, True, congr, Set.indicator_of_mem, HPow.hPow, HMul.hMul, 𝕔, Nat.cast_one, eq_self, Not and 5 more

    75 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

    lemma stackSize_real (C : Set (𝔓 X)) (x : X) :
    (stackSize C x : ℝ) = βˆ‘ p with p ∈ C, (π“˜ p : Set X).indicator (1 : X β†’ ℝ) x := by
…

    Mentions: 𝔓, stackSize, π“˜

  85. lemma stackSize_measurable line 456 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Measurable, ENNReal, stackSize

    Proof uses: id, Eq.mpr, Finset.sum, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator, π“˜, OfNat.ofNat, Eq, congrArg, funext, Nat.cast_sum, ite, Classical.decPred, Finset.sum_congr, Eq.refl, Finset, Nat.cast_ite and 8 more

    62 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  86. lemma stackSize_le_one_of_pairwiseDisjoint line 461 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Set.PairwiseDisjoint, π“˜, LE.le, stackSize and 1 more

    Proof uses: dite, Exists, And, Membership.mem, Classical.propDecidable, Eq.mpr, Finset.sum, Finset.filter, Finset.univ, Set.indicator, id, Eq, congrArg, stackSize.eq_1, Finset.sum_eq_single_of_mem, of_eq_true, HPow.hPow, HMul.hMul, 𝕔, Finset and 80 more

    152 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

    Open to load the checked before-and-after goal states.

  87. lemma eq_empty_of_forall_stackSize_zero line 480 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, stackSize, OfNat.ofNat, EmptyCollection.emptyCollection

    Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Not, id, Eq.trans, False, congrArg, iff_false, π“˜, Set.Nonempty, Grid.nonempty, Eq.mp, Finset.sum, HPow.hPow, HMul.hMul, 𝕔, Finset.filter, Classical.propDecidable and 7 more

    61 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

  88. lemma exists_maximal_disjoint_covering_subfamily Given any family of tiles, one can extract a maximal disjoint subfamily, covering everything line 495 source

    Source documentation

    Given any family of tiles, one can extract a maximal disjoint subfamily, covering everything.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Exists, And, Set.PairwiseDisjoint, π“˜ and 2 more

    Proof uses: Set.ofPred, Or, Disjoint, MaximalFor, id, Set.Finite.exists_maximalFor, Set.toFinite, Exists.intro, EmptyCollection.emptyCollection, of_eq_true, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, Eq.trans, True, congr, congrArg, forall_congr, implies_congr and 41 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 40 steps

    Open to load the checked before-and-after goal states.

    lemma exists_maximal_disjoint_covering_subfamily (A : Set (𝔓 X)) :
    βˆƒ (B : Set (𝔓 X)), B.PairwiseDisjoint (fun p ↦ (π“˜ p : Set X)) ∧
      B βŠ† A ∧ (βˆ€ a ∈ A, βˆƒ b ∈ B, (π“˜ a : Set X) βŠ† π“˜ b) := by
…

    Mentions: A, 𝔓, π“˜

  89. def maximalSubfamily A disjoint subfamily of A covering everything line 535 source

    Source documentation

    A disjoint subfamily of A covering everything.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Exists.choose, And, Set.PairwiseDisjoint, π“˜, LE.le, Membership.mem, Exists, exists_maximal_disjoint_covering_subfamily

    37 instances, coercions and auxiliary constants left out.

    def maximalSubfamily (A : Set (𝔓 X)) : Set (𝔓 X) :=
…

    Mentions: A, 𝔓

  90. def iteratedMaximalSubfamily Iterating maximalSubfamily to obtain disjoint subfamilies of A line 539 source

    Source documentation

    Iterating maximalSubfamily to obtain disjoint subfamilies of A.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, maximalSubfamily, SDiff.sdiff, Set.iUnion, Set.ofPred, Membership.mem

    31 instances, coercions and auxiliary constants left out.

    def iteratedMaximalSubfamily (A : Set (𝔓 X)) (n : β„•) : Set (𝔓 X) :=
…

    Mentions: A, 𝔓

  91. lemma pairwiseDisjoint_iteratedMaximalSubfamily_image line 542 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Set.PairwiseDisjoint, iteratedMaximalSubfamily, π“˜

    Proof uses: Eq.mpr, maximalSubfamily, SDiff.sdiff, Set.iUnion, Set.ofPred, LT.lt, Membership.mem, id, Eq, congrArg, iteratedMaximalSubfamily.eq_1, And.left, Exists.choose, And, LE.le, Exists, exists_maximal_disjoint_covering_subfamily, Exists.choose_spec

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  92. lemma iteratedMaximalSubfamily_subset line 547 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, iteratedMaximalSubfamily

    Proof uses: Eq.mpr, maximalSubfamily, SDiff.sdiff, Set.iUnion, Set.ofPred, LT.lt, Membership.mem, id, Eq, congrArg, iteratedMaximalSubfamily.eq_1, LE.le.trans, Exists.choose, And, Set.PairwiseDisjoint, π“˜, Exists, exists_maximal_disjoint_covering_subfamily, And.left, And.right and 2 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  93. lemma pairwiseDisjoint_iteratedMaximalSubfamily line 553 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Set.PairwiseDisjoint, Set.univ, iteratedMaximalSubfamily

    Proof uses: Membership.mem, Ne, LT.lt, Not, Or, Function.onFun, Disjoint, Classical.em, LE.le, SDiff.sdiff, Set.iUnion, Set.ofPred, Eq.mpr, maximalSubfamily, id, Eq, Eq.rec, Eq.refl, Eq.trans, congrArg and 26 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

    Open to load the checked before-and-after goal states.

  94. lemma eq_biUnion_iteratedMaximalSubfamily Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size line 572 source

    Source documentation

    Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, stackSize, Eq, Set.iUnion and 2 more

    Proof uses: Set.Subset.antisymm, Membership.mem, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, Exists, id, implies_congr, Eq.refl, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, And, π“˜, maximalSubfamily, SDiff.sdiff, Set.ofPred, iteratedMaximalSubfamily.eq_1, And.right and 73 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 51 steps

    Open to load the checked before-and-after goal states.

    lemma eq_biUnion_iteratedMaximalSubfamily (A : Set (𝔓 X)) {N : β„•} (hN : βˆ€ x, stackSize A x ≀ N) :
    A = ⋃ n < N, iteratedMaximalSubfamily A n := by
…

    Mentions: A, 𝔓, stackSize, iteratedMaximalSubfamily