Carleson/Discrete/ExceptionalSet.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

41 declarations, 0 contain sorry, 0 declared as axioms

Section 5.2 and Lemma 5.1.1

Imports (2)
Imported by 2 files
  1. def C5_2_9 The constant in Lemma 5.2.9, with value D ^ (1 - κ * Z * (n + 1)) line 19 source

    Source documentation

    The constant in Lemma 5.2.9, with value D ^ (1 - κ * Z * (n + 1))

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, NNReal

    Proof uses: HPow.hPow, defaultD, HSub.hSub, OfNat.ofNat, HMul.hMul, defaultκ, defaultZ, HAdd.hAdd

    19 instances, coercions and auxiliary constants left out.

    def C5_2_9 [ProofData a q K σ₁ σ₂ F G] (n : ℕ) : ℝ≥0 := D ^ (1 - κ * Z * (n + 1))
…

    Mentions: ProofData, K

  2. lemma third_exception_rearrangement A rearrangement for Lemma 5.2.9 that does not require the tile structure line 24 source

    Source documentation

    A rearrangement for Lemma 5.2.9 that does not require the tile structure.

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, Eq, ENNReal, tsum, ite, LE.le, HMul.hMul, C5_2_9, HPow.hPow, OfNat.ofNat, HSub.hSub, HAdd.hAdd, MeasureTheory.Measure, NNReal and 7 more

    Proof uses: Trans.trans, eq_of_heq, AddCommMonoid, TopologicalSpace, optParam, SummationFilter, HEq, Eq.refl, HEq.refl, Eq.symm, funext, ite_congr, Eq.mpr, id, congrArg, ENNReal.tsum_mul_left, mul_rotate, mul_assoc, HMul, Eq.rec and 106 more

    245 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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

    lemma third_exception_rearrangement :
    (∑' n, ∑' k, if k ≤ n then ∑' (j : ℕ),
      C5_2_9 X n * 2 ^ (9 * a - j : ℤ) * 2 ^ (n + k + 3) * volume G else 0) =
    ∑' k, 2 ^ (9 * a + 4 + 2 * k) * D ^ (1 - κ * Z * (k + 1)) * volume G *
      ∑' n, if k ≤ n then (2 * D ^ (-κ * Z) : ℝ≥0∞) ^ (n - k : ℝ) else 0 := by
…

    Mentions: k, C5_2_9

  3. lemma first_exception' Lemma 5.2.1 line 66 source

    Source documentation

    Lemma 5.2.1

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, G₁ and 4 more

    Proof uses: dite, Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, G₁_empty, MeasureTheory.measure_empty, Not, Eq.rec, zero_le, Eq.symm, MeasureTheory.OuterMeasureClass.measure_empty, G₁_empty', HDiv.hDiv, HAdd.hAdd, GT.gt, ENNReal.div_pos and 148 more

    224 instances, coercions and auxiliary constants left out.

    Tactic trace: 60 steps

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

    lemma first_exception' : volume (G₁ : Set X) ≤ 2 ^ (- 5 : ℤ) * volume G := by
…

    Mentions: G₁

  4. lemma first_exception line 130 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, G₁ and 4 more

    Proof uses: Trans.trans, first_exception', mul_le_mul', ENNReal.zpow_le_of_le, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, neg_le_neg, le_refl

    92 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. lemma dense_cover Lemma 5.2.2 line 137 source

    Source documentation

    Lemma 5.2.2

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Set.iUnion and 7 more

    Proof uses: Finset, Finset.filter, LT.lt, Neg.neg, Inter.inter, Finset.univ, id, SDiff.sdiff, aux𝓒, Eq.mpr, Exists, Eq, congrArg, propext, Set.mem_iUnion₂, Eq.mp, And, And.left, Not, Set.ofPred and 72 more

    204 instances, coercions and auxiliary constants left out.

    Tactic trace: 31 steps

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

    lemma dense_cover (k : ℕ) : volume (⋃ i ∈ 𝓒 (X := X) k, (i : Set X)) ≤ 2 ^ (k + 1) * volume G := by
…

    Mentions: k, 𝓒

  6. lemma pairwiseDisjoint_E1 Lemma 5.2.3 line 167 source

    Source documentation

    Lemma 5.2.3

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Set.PairwiseDisjoint, 𝔓, 𝔐, E₁

    Proof uses: Membership.mem, Ne, id, Function.onFun, Disjoint, Mathlib.Tactic.Contrapose.contrapose₂, Eq, Not, 𝓘, Function.mt, Disjoint.mono, E₁_subset, LE.le, s, Or, Classical.em, And, Exists, Iff.mp, Set.not_disjoint_iff and 38 more

    81 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

    lemma pairwiseDisjoint_E1 : (𝔐 (X := X) k n).PairwiseDisjoint E₁ := fun p mp p' mp' h ↦ by
…

    Mentions: 𝔐, k, E₁

  7. lemma dyadic_union Lemma 5.2.4 line 182 source

    Source documentation

    Lemma 5.2.4

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Membership.mem, setA, Exists, Grid, And and 1 more

    Proof uses: Finset, 𝔓, Finset.filter, 𝔐, 𝓘, Classical.propDecidable, Finset.univ, id, Set.ofPred, LT.lt, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, stackSize, Eq.mpr, Finset.sum, Set.indicator, ite, Eq and 36 more

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

    lemma dyadic_union (hx : x ∈ setA l k n) : ∃ i : Grid X, x ∈ i ∧ (i : Set X) ⊆ setA l k n := by
…

    Mentions: setA, k, Grid

  8. lemma iUnion_MsetA_eq_setA line 193 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Eq, Set.iUnion, Grid, Membership.mem, Finset and 2 more

    Proof uses: Set.ext, Eq.mpr, Iff, Exists, id, congrFun', congrArg, Finset.filter, LE.le, Classical.propDecidable, Finset.univ, funext, propext, exists_prop_congr, Iff.of_eq, Eq.refl, Iff.intro, Set.mem_of_mem_of_subset, And, dyadic_union and 1 more

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  9. lemma john_nirenberg_aux1 Equation (5.2.7) in the proof of Lemma 5.2.5 line 202 source

    Source documentation

    Equation (5.2.7) in the proof of Lemma 5.2.5.

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, Membership.mem, Finset, Grid.maxCubes, MsetA and 11 more

    Proof uses: Eq, Not, Disjoint, id, Eq.mpr, Finset.sum, Finset.filter, Classical.propDecidable, Finset.univ, Set.indicator, AddUnits, forall_congr, implies_congr, Eq.refl, False, eq_false, of_eq_true, Eq.trans, True, congrArg and 77 more

    141 instances, coercions and auxiliary constants left out.

    Tactic trace: 49 steps

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

    lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n))
    (mx : x ∈ setA (l + 1) k n) (mx₂ : x ∈ L) : 2 ^ (n + 1) ≤
    stackSize { q ∈ 𝔐 (X := X) k n | 𝓘 q ≤ L} x := by
…

    Mentions: Grid, Grid.maxCubes, MsetA, k, setA, stackSize, 𝔐, 𝓘

  10. lemma john_nirenberg_aux2 Equation (5.2.11) in the proof of Lemma 5.2.5 line 262 source

    Source documentation

    Equation (5.2.11) in the proof of Lemma 5.2.5.

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Grid, Membership.mem, Finset, Grid.maxCubes, MsetA and 9 more

    Proof uses: 𝔓, Finset.filter, And, 𝔐, 𝓘, Classical.propDecidable, Finset.univ, Measurable, Set.indicator, Measurable.indicator, measurable_one, GridStructure.coeGrid_measurable, Finset.sum, E₁, Trans.trans, Set.iUnion, Eq, Eq.symm, MeasureTheory.measure_biUnion_finset, Ne and 101 more

    233 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

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

    lemma john_nirenberg_aux2 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n)) :
    2 * volume (setA (X := X) (l + 1) k n ∩ L) ≤ volume (L : Set X) := by
…

    Mentions: Grid, Grid.maxCubes, MsetA, k, setA

  11. lemma john_nirenberg Lemma 5.2.5 line 314 source

    Source documentation

    Lemma 5.2.5

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, setA and 5 more

    Proof uses: Nat.recAux, Trans.trans, Set.iUnion, Grid, Membership.mem, 𝓒, MeasureTheory.measure_mono, setA_subset_iUnion_𝓒, Eq.mpr, id, Eq, congrArg, Eq.symm, ENNReal.rpow_intCast, of_eq_true, Eq.trans, True, congrFun', CharP.cast_eq_zero, sub_zero and 73 more

    162 instances, coercions and auxiliary constants left out.

    Tactic trace: 59 steps

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

    lemma john_nirenberg : volume (setA (X := X) l k n) ≤ 2 ^ (k + 1 - l : ℤ) * volume G := by
…

    Mentions: setA, k

  12. lemma second_exception Lemma 5.2.6 line 360 source

    Source documentation

    Lemma 5.2.6

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, G₂ and 4 more

    Proof uses: Trans.trans, Eq, Set.iUnion, setA, HAdd.hAdd, tsum, HSub.hSub, SummationFilter.unconditional, ite, EmptyCollection.emptyCollection, MeasureTheory.measure_iUnion_le, eq_of_heq, AddCommMonoid, TopologicalSpace, optParam, SummationFilter, HEq, Eq.refl, HEq.refl, Eq.symm and 70 more

    161 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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

    lemma second_exception : volume (G₂ (X := X)) ≤ 2 ^ (-2 : ℤ) * volume G :=
…

    Mentions: G₂

  13. def layervol The volume of a "layer" in the key function of Lemma 5.2.7 line 397 source

    Source documentation

    The volume of a "layer" in the key function of Lemma 5.2.7.

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, ENNReal

    Proof uses: MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Set.ofPred, LE.le, Finset.sum, 𝔓, Finset.filter, Membership.mem, 𝔐, Classical.propDecidable, Finset.univ, Set.indicator, 𝓘, OfNat.ofNat

    39 instances, coercions and auxiliary constants left out.

    def layervol (k n : ℕ) (t : ℝ) : ℝ≥0∞ :=
…

    Mentions: k

  14. lemma indicator_sum_eq_natCast line 402 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Finset, 𝔓, Eq, Finset.sum, Set.indicator and 2 more

    Proof uses: Eq.mpr, id, congrArg, Nat.cast_sum, Finset.sum_congr, Eq.refl, Membership.mem, of_eq_true, ite, HPow.hPow, HMul.hMul, 𝕔, Classical.decPred, Eq.trans, True, Nat.cast_ite, congr, Nat.cast_one, CharP.cast_eq_zero, eq_self

    78 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  15. lemma layervol_eq_zero_of_lt line 408 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LT.lt, Finset.card, 𝔓, Set.toFinset, 𝔐 and 6 more

    Proof uses: Eq.mpr, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Set.ofPred, LE.le, Finset.sum, Finset.filter, Finset.univ, Set.indicator, 𝓘, id, congrArg, layervol.eq_1, Filter.Eventually, Not, MeasureTheory.ae, propext, MeasureTheory.measure_eq_zero_iff_ae_notMem, MeasureTheory.ae_of_all, Set.mem_ofPred and 15 more

    80 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  16. lemma lintegral_Ioc_layervol_one line 419 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Eq, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume and 4 more

    Proof uses: Trans.trans, HMul.hMul, MeasureTheory.Measure, MeasureTheory.setLIntegral_congr_fun, measurableSet_Ioc, Membership.mem, id, eq_of_heq, Set.ofPred, LE.le, Finset.sum, 𝔓, Finset.filter, 𝔐, Classical.propDecidable, Finset.univ, Set.indicator, 𝓘, HEq, DFunLike and 31 more

    133 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

  17. lemma antitone_layervol line 432 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Antitone, ENNReal, layervol

    Proof uses: LE.le, id, MeasureTheory.measure_mono, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Set.ofPred, Finset.sum, 𝔓, Finset.filter, Membership.mem, 𝔐, Classical.propDecidable, Finset.univ, Set.indicator, 𝓘, OfNat.ofNat, LE.le.trans

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  18. lemma lintegral_Ioc_layervol_le line 435 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume and 6 more

    Proof uses: Trans.trans, Eq, Finset.sum, Finset.Ico, Eq.mpr, id, congrArg, Eq.symm, mul_one, eq_of_heq, HEq, Eq.refl, HEq.refl, Finset.sum_congr, Finset, Membership.mem, MeasurableSpace, MeasureTheory.Measure, of_eq_true, Eq.trans and 20 more

    122 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  19. lemma top_tiles_aux line 448 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, Eq, ENNReal, Finset.sum, 𝔓, Finset.filter and 17 more

    Proof uses: Eq.mpr, id, congrArg, rfl, Trans.trans, Set.Ioi, ENNReal.ofReal, Set.indicator, Finset.sum_congr, Eq.refl, Finset, Eq.symm, MeasureTheory.lintegral_indicator_one, GridStructure.coeGrid_measurable, MeasureTheory.lintegral_finsetSum, Measurable.indicator, measurable_one, eq_of_heq, MeasurableSpace, HEq and 46 more

    171 instances, coercions and auxiliary constants left out.

    Tactic trace: 31 steps

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

  20. lemma top_tiles Lemma 5.2.7 line 480 source

    Source documentation

    Lemma 5.2.7

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, Finset.sum, 𝔓, Finset.filter and 11 more

    Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Finset.card, Set.toFinset, Trans.trans, tsum, HSub.hSub, SummationFilter.unconditional, Finset.range, setA, layervol, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.Ioc, top_tiles_aux, Finset.Ico, Finset and 70 more

    199 instances, coercions and auxiliary constants left out.

    Tactic trace: 34 steps

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

    lemma top_tiles : ∑ m with m ∈ 𝔐 (X := X) k n, volume (𝓘 m : Set X) ≤
…

    Mentions: 𝔐, k, 𝓘

  21. def 𝔘 The function 𝔘(m) used in the proof of Lemma 5.2.8 line 529 source

    Source documentation

    The function 𝔘(m) used in the proof of Lemma 5.2.8

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Finset

    Proof uses: Finset.filter, And, Membership.mem, Grid, 𝓘, LE.le, TileLike, smul, OfNat.ofNat, Classical.propDecidable, Set.toFinset, 𝔘₁

    40 instances, coercions and auxiliary constants left out.

    def 𝔘 (m : 𝔓 X) := (𝔘₁ k n j).toFinset.filter (fun u ↦ x ∈ 𝓘 u ∧ smul 100 u ≤ smul 1 m)

    Mentions: 𝔓, 𝔘₁, k, 𝓘, smul

  22. def big_ball Ball that covers the image of 𝒬 line 532 source

    Source comment

    Ball that covers the image of `𝒬`. Radius chosen for convenience with `BallsCoverBalls.pow_mul`
    private def big_ball (m : 𝔓 X) (u : 𝔓 X) := ball_(u) (𝒬 m) (2 ^ 9 * 0.2)
…

    Mentions: 𝔓

  23. lemma x_mem_𝓘u line 539 source
  24. lemma 𝒬m_mem_ball line 545 source
  25. lemma 𝓘_not_lt_𝓘 line 551 source
  26. lemma 𝓘_eq_𝓘 line 561 source
  27. lemma ball_eq_ball line 567 source
  28. lemma disjoint_balls line 572 source
  29. lemma mem_big_ball line 579 source
  30. lemma subset_big_ball line 588 source
  31. lemma balls_cover_big_ball line 594 source
  32. lemma 𝒬_injOn_𝔘m line 597 source
  33. lemma card_𝔘m_le line 601 source
  34. def 𝔐' line 631 source
  35. lemma interchange line 635 source
  36. lemma indicator_le line 647 source
  37. lemma tree_count Lemma 5.2.8 line 668 source

    Source documentation

    Lemma 5.2.8

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, stackSize, 𝔘₁, HMul.hMul, HPow.hPow and 3 more

    Proof uses: Eq, Finset.sum, 𝔓, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Set.indicator, 𝓘, Grid, Set.toFinset, Eq.mpr, id, congrArg, Finset, Set.filter_mem_univ_eq_toFinset, ite, Finset.sum_filter, Finset.sum_congr, rfl and 43 more

    175 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

    lemma tree_count :
    stackSize (𝔘₁ k n j) x ≤ (2 : ℝ) ^ (9 * a - j : ℤ) * stackSize (𝔐 k n) x := by
…

    Mentions: stackSize, 𝔘₁, k, 𝔐

  38. lemma boundary_exception Lemma 5.2.9 line 691 source

    Source documentation

    Lemma 5.2.9

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume and 7 more

    Proof uses: dite, Set.Nonempty, Classical.propDecidable, Set.ofPred, And, Metric.infEDist, Compl.compl, OfNat.ofNat, HPow.hPow, HSub.hSub, 𝔰, defaultZ, HAdd.hAdd, Eq, rfl, Trans.trans, Neg.neg, Prod.fst, GridStructure.Grid, Prod.mk and 231 more

    362 instances, coercions and auxiliary constants left out.

    Tactic trace: 155 steps

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

    lemma boundary_exception {u : 𝔓 X} :
    volume (⋃ i ∈ 𝓛 (X := X) n u, (i : Set X)) ≤ C5_2_9 X n * volume (𝓘 u : Set X) := by
…

    Mentions: 𝔓, 𝓛, C5_2_9, 𝓘

  39. lemma third_exception_aux line 841 source

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Set.iUnion and 10 more

    Proof uses: Trans.trans, Finset.sum, Finset.filter, 𝔐, Classical.propDecidable, Finset.univ, 𝔘₁, Eq, tsum, SummationFilter.unconditional, Grid, 𝓛, MeasureTheory.measure_mono, Set.iUnion₂_subset, And, Exists, And.right, ℭ₄, Set.subset_iUnion₂_of_subset, MeasureTheory.measure_biUnion_le and 77 more

    181 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

  40. lemma third_exception Lemma 5.2.10 line 878 source

    Source documentation

    Lemma 5.2.10

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, G₃ and 4 more

    Proof uses: Trans.trans, Set.iUnion, HAdd.hAdd, 𝔓, Membership.mem, 𝔏₄, 𝓘, HSub.hSub, 𝕔, Eq, defaultZ, tsum, Inv.inv, SummationFilter.unconditional, ite, C5_2_9, EmptyCollection.emptyCollection, MeasureTheory.measure_iUnion_le, Summable.tsum_le_tsum, ENNReal.summable and 179 more

    303 instances, coercions and auxiliary constants left out.

    Tactic trace: 105 steps

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

    lemma third_exception : volume (G₃ (X := X)) ≤ 2 ^ (-4 : ℤ) * volume G := by
…

    Mentions: G₃

  41. lemma exceptional_set Lemma 5.1.1 line 979 source

    Source documentation

    Lemma 5.1.1

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

    Statement uses: MetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, G' and 4 more

    Proof uses: Trans.trans, HAdd.hAdd, Eq, G₁, G₂, G₃, rfl, le_add_of_le_add_right, Union.union, MeasureTheory.measure_union_le, add_le_add_three, first_exception, second_exception, third_exception, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.mpr and 60 more

    147 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

    lemma exceptional_set : volume (G' : Set X) ≤ 2 ^ (-1 : ℤ) * volume G :=
…

    Mentions: G'