Carleson/Antichain/TileCorrelation.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

32 declarations, 0 contain sorry, 0 declared as axioms

6.2. Proof of the Tile Correlation Lemma

This file contains the proofs of lemmas 6.2.1, 6.2.2, 6.2.3 and 6.1.5 from the blueprint.

Main definitions

Main results

Imports (3)
Imported by 2 files
  1. def Tile.correlation Def 6.2.1 (from Lemma 6.2.1), denoted by φ(y) in the blueprint line 38 source

    Source documentation

    Def 6.2.1 (from Lemma 6.2.1), denoted by φ(y) in the blueprint.

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

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

    Proof uses: HMul.hMul, RingHom, starRingEnd, Ks

    11 instances, coercions and auxiliary constants left out.

    def correlation (s₁ s₂ : ℤ) (x₁ x₂ y : X) : ℂ := conj (Ks s₁ x₁ y) * Ks s₂ x₂ y
…

    Mentions: Ks

  2. lemma Tile.measurable_correlation line 41 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Measurable, Tile.correlation

    Proof uses: Measurable.of_discrete

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma Tile.mem_ball_of_correlation_ne_zero First part of Lemma 6.2.1 (eq line 44 source

    Source documentation

    First part of Lemma 6.2.1 (eq. 6.2.2).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Ne, Tile.correlation, OfNat.ofNat, Membership.mem, Metric.ball, HPow.hPow, defaultD

    Proof uses: Ks, And.left, Not, Eq, Eq.mp, And, Eq.trans, HMul.hMul, RingHom, starRingEnd, Or, congrArg, congrFun', Eq.mpr, LT.lt, Dist.dist, id, propext, Metric.mem_ball, dist_comm and 9 more

    81 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

    lemma mem_ball_of_correlation_ne_zero {s₁ s₂ : ℤ} {x₁ x₂ y : X}
    (hy : correlation s₁ s₂ x₁ x₂ y ≠ 0) : y ∈ ball x₁ (D ^ s₁) := by
…

    Mentions: Tile.correlation

  4. def Tile.C6_2_1 The constant from lemma 6.2.1 line 54 source

    Source documentation

    The constant from lemma 6.2.1. Has value 2 ^ (231 * a ^ 3) in the blueprint.

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

    Statement uses: Nat, NNReal

    Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔, HDiv.hDiv

    19 instances, coercions and auxiliary constants left out.

    def C6_2_1 (a : ℕ) : ℝ≥0 := 2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3)
  5. lemma Tile.aux_6_2_3 line 56 source
  6. lemma Tile.e625 Ineq line 64 source

    Source documentation

    Ineq. (6.2.5) ≤ (6.2.9) from the proof of Lemma 6.2.1.

    private lemma e625 {s₁ s₂ : ℤ} {x₁ x₂ y y' : X} (hy' : y ≠ y') (hs : s₁ ≤ s₂) :
    (2 * D ^ s₁) ^ τ *
    (‖correlation s₁ s₂ x₁ x₂ y - correlation s₁ s₂ x₁ x₂ y'‖ₑ / edist y y' ^ τ) ≤
    2 ^ ((2 * 𝕔 + 5 + 𝕔 / 4) * a ^ 3) /
    (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))) := by
…

    Mentions: Tile.correlation

  7. lemma Tile.correlation_kernel_bound Second part of Lemma 6.2.1 (eq line 131 source

    Source documentation

    Second part of Lemma 6.2.1 (eq. 6.2.3).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, ENNReal, iHolENorm, Tile.correlation, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, defaultτ, HDiv.hDiv, Tile.C6_2_1, MeasureTheory.Measure, NNReal and 3 more

    Proof uses: ENorm.enorm, C2_1_3, Eq.mpr, Ks, id, Eq, congr, congrArg, Eq.trans, RingHom, starRingEnd, enorm_mul, congrFun', RCLike.enorm_conj, pow_two, MeasurableSpace, PseudoMetricSpace, ProperSpace, MeasureTheory.IsFiniteMeasureOnCompacts, ENNReal.mul_div_mul_comm and 122 more

    247 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

    lemma correlation_kernel_bound {s₁ s₂ : ℤ} {x₁ x₂ : X} (hs : s₁ ≤ s₂) :
    iHolENorm (correlation s₁ s₂ x₁ x₂) x₁ (2 * D ^ s₁) τ ≤
    C6_2_1 a / (volume (ball x₁ (D ^ s₁)) * volume (ball x₂ (D ^ s₂))) := by
…

    Mentions: iHolENorm, Tile.correlation, Tile.C6_2_1

  8. lemma Tile.range_support Lemma 6.2.2 line 168 source

    Source documentation

    Lemma 6.2.2.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Ne, adjointCarleson, OfNat.ofNat, Membership.mem and 5 more

    Proof uses: And, E, RingHom, starRingEnd, Ks, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, Exists, MeasureTheory.exists_ne_zero_of_setIntegral_ne_zero, MeasureTheory.MeasureSpace.volume, LT.lt, Dist.dist, GridStructure.Grid_subset_ball, 𝓘, Set.mem_of_subset_of_mem, And.left, Grid and 79 more

    158 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

    lemma range_support {p : 𝔓 X} {g : X → ℂ} {y : X} (hpy : adjointCarleson p g y ≠ 0) :
    y ∈ ball (𝔠 p) (5 * D ^ 𝔰 p) := by
…

    Mentions: 𝔓, g, adjointCarleson, 𝔠, 𝔰

  9. def Tile.C6_2_3 The constant from lemma 6.2.3 line 189 source

    Source documentation

    The constant from lemma 6.2.3.

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

    Statement uses: Nat, NNReal

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

    14 instances, coercions and auxiliary constants left out.

    def C6_2_3 (a : ℕ) : ℝ≥0 := 2 ^ (8 * a)
  10. lemma Tile.ineq_6_2_16 line 191 source
  11. lemma Tile.uncertainty' Lemma 6.2.3 (dist version) line 196 source

    Source documentation

    Lemma 6.2.3 (dist version).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, OfNat.ofNat, 𝔓, 𝔰, Set.Nonempty and 15 more

    Proof uses: LT.lt, Eq.mpr, id, Eq, congrArg, dist_comm, 𝓘, one_le_realD, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 162 more

    243 instances, coercions and auxiliary constants left out.

    Tactic trace: 81 steps

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

    lemma uncertainty' (ha : 1 ≤ a) {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰 p₂)
    (hinter : (ball (𝔠 p₁) (5 * D ^ 𝔰 p₁) ∩ ball (𝔠 p₂) (5 * D ^ 𝔰 p₂)).Nonempty) {x₁ x₂ : X}
    (hx₁ : x₁ ∈ E p₁) (hx₂ : x₂ ∈ E p₂) :
    1 + dist_(p₁) (𝒬 p₁) (𝒬 p₂) ≤ C6_2_3 a * (1 + dist_{x₁, D ^ 𝔰 p₁} (Q x₁) (Q x₂)) := by
…

    Mentions: 𝔓, 𝔰, 𝔠, E, Tile.C6_2_3

  12. lemma Tile.uncertainty Lemma 6.2.3 (edist version) line 295 source

    Source documentation

    Lemma 6.2.3 (edist version).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, OfNat.ofNat, 𝔓, 𝔰, Set.Nonempty and 16 more

    Proof uses: Eq, ENNReal.ofReal, Eq.mpr, id, congrArg, ENNReal.ofReal_coe_nnreal, Eq.refl, Dist.dist, congr, Eq.trans, edist_dist, PseudoMetricSpace, Eq.symm, ENNReal.ofReal_add, zero_le_one, dist_nonneg, ENNReal.ofReal_mul, NNReal.zero_le_coe, ENNReal.ofReal_le_ofReal, Tile.uncertainty'

    114 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma uncertainty (ha : 1 ≤ a) {p₁ p₂ : 𝔓 X} (hle : 𝔰 p₁ ≤ 𝔰 p₂)
    (hinter : (ball (𝔠 p₁) (5 * D ^ 𝔰 p₁) ∩ ball (𝔠 p₂) (5 * D ^ 𝔰 p₂)).Nonempty) {x₁ x₂ : X}
    (hx₁ : x₁ ∈ E p₁) (hx₂ : x₂ ∈ E p₂) :
    1 + edist_(p₁) (𝒬 p₁) (𝒬 p₂) ≤ C6_2_3 a * (1 + edist_{x₁, D ^ 𝔰 p₁} (Q x₁) (Q x₂)) := by
…

    Mentions: 𝔓, 𝔰, 𝔠, E, Tile.C6_2_3

  13. def Tile.C6_1_5 The constant from lemma 6.1.5 line 308 source

    Source documentation

    The constant from lemma 6.1.5. Has value 2 ^ (232 * a ^ 3) in the blueprint.

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

    Statement uses: Nat, NNReal

    Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔, HDiv.hDiv

    19 instances, coercions and auxiliary constants left out.

    def C6_1_5 (a : ℕ) : ℝ≥0 := 2 ^ ((2 * 𝕔 + 7 + 𝕔 / 4) * a ^ 3)
  14. lemma Tile.C6_1_5_bound line 310 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HMul.hMul, HPow.hPow, HAdd.hAdd, 𝕔, HDiv.hDiv, Tile.C6_1_5

    Proof uses: Eq, rfl, Eq.mpr, id, congrArg, Tile.C6_1_5.eq_1, Eq.symm, pow_add, pow_le_pow, le_rfl, one_le_two, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 73 more

    142 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  15. lemma Tile.complex_exp_lintegral line 318 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Eq, RingHom, starRingEnd, MeasureTheory.integral and 13 more

    Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, funext, map_mul, RingHomCompTriple.comp_apply, RingHom.id, NormedAddCommGroup, NormedSpace, MeasurableSpace, MeasureTheory.Measure, Eq.rec, Eq.refl, Eq.symm, Complex.exp_conj, HMul, congr, Complex.conj_I and 41 more

    138 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  16. def Tile.I12 Definition (6.2.27) line 327 source

    Source documentation

    Definition (6.2.27).

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

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

    Proof uses: ENorm.enorm, HMul.hMul, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, Complex.exp, Complex.I, HAdd.hAdd, Neg.neg, FunctionDistances.Θ, MeasureTheory.SimpleFunc, Tile.correlation, 𝔰

    55 instances, coercions and auxiliary constants left out.

    def I12 (p p' : 𝔓 X) (g : X → ℂ) (x1 x2 : X) : ℝ≥0∞ :=
…

    Mentions: 𝔓, g

  17. lemma Tile.I12_le' Inequality (6.2.28) line 332 source

    Source documentation

    Inequality (6.2.28).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, 𝔰, E, ENNReal and 18 more

    Proof uses: LT.lt, defaultD_pow_pos, Function.support, Tile.correlation, Tile.mem_ball_of_correlation_ne_zero, Eq, Eq.mpr, id, congrArg, ENNReal.mul_comm_div, mul_comm, mul_div_assoc, Eq.refl, MeasureTheory.integral, Complex.exp, Complex.I, congrFun', Eq.trans, enorm_mul, mul_le_mul' and 36 more

    253 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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

    lemma I12_le' {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ} (x1 : E p') (x2 : E p) :
    I12 p p' g x1 x2 ≤
    2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 8 * a) *
      ((1 + edist_{x1.1, D ^ 𝔰 p'} (Q x1) (Q x2)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹)) /
    volume (ball x2.1 (D ^ 𝔰 p)) * ‖g x1‖ₑ * ‖g x2‖ₑ := by
…

    Mentions: 𝔓, 𝔰, g, E, Tile.I12

  18. lemma Tile.exp_ineq line 378 source
  19. lemma Tile.I12_le Inequality (6.2.29) line 386 source

    Source documentation

    Inequality (6.2.29).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, OfNat.ofNat, 𝔓, 𝔰, Set.Nonempty and 20 more

    Proof uses: LE.le.trans, MeasureTheory.SimpleFunc, FunctionDistances.Θ, Tile.I12_le', id, mul_le_mul', Eq.mpr, Eq, congrArg, pow_add, pow_one, mul_comm, mul_assoc, ENNReal.div_le_div, le_refl, Tile.C6_2_3, Tile.uncertainty, Subtype.property, LT.lt, Iff.mpr and 122 more

    329 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

    lemma I12_le (ha : 4 ≤ a) {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ}
    (hinter : (ball (𝔠 p') (5 * D ^ 𝔰 p') ∩ ball (𝔠 p) (5 * D ^ 𝔰 p)).Nonempty)
    (x1 : E p') (x2 : E p) :
    I12 p p' g x1 x2 ≤
    (2 ^ ((2 * 𝕔 + 6 + 𝕔 / 4) * a ^ 3 + 8 * a + 1) *
      ((1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹))) /
    volume (ball x2.1 (D ^ 𝔰 p)) * ‖g x1‖ₑ * ‖g x2‖ₑ := by
…

    Mentions: 𝔓, 𝔰, g, 𝔠, E, Tile.I12

  20. lemma Tile.volume_coeGrid_le Inequality (6.2.32) line 416 source

    Source documentation

    Inequality (6.2.32).

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

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

    Proof uses: LT.lt, Dist.dist, 𝔠, Eq.rec, Eq, GridStructure.Grid_subset_ball, Set.mem_of_subset_of_mem, And.left, Grid, And, FunctionDistances.Θ, TileStructure.Ω, MeasureTheory.SimpleFunc, Set.Icc, Subtype.prop, Eq.symm, dist_comm, LE.le.trans, GridStructure.c, GridStructure.s and 50 more

    156 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

    lemma volume_coeGrid_le {p : 𝔓 X} (x2 : E p) :
    volume (𝓘 p : Set X) ≤ 2 ^ (3 * a) * volume (ball x2.1 (D ^ 𝔰 p)) := by
…

    Mentions: 𝔓, E, 𝓘, 𝔰

  21. lemma Tile.bound_6_2_29 line 433 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, OfNat.ofNat, 𝔓, E, ENNReal and 18 more

    Proof uses: Eq.mpr, id, Eq, congrArg, mul_comm, mul_div_assoc, mul_le_mul_right, Trans.trans, congr, congrFun', Eq.trans, Eq.symm, ENNReal.zpow_add, two_ne_zero, ENNReal.ofNat_ne_top, HDiv, Eq.rec, Eq.refl, HPow, Nat.cast_add and 82 more

    220 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  22. lemma Tile.enorm_eq_zero_of_notMem_closedBall line 455 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, Norm.norm, Set.indicator, OfNat.ofNat, Not, Membership.mem, Metric.closedBall, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, defaultS and 3 more

    Proof uses: Eq.mpr, id, congrArg, propext, enorm_eq_zero, Eq.symm, norm_eq_zero, le_antisymm, LE.le.trans, Set.indicator_of_notMem, Set.notMem_subset, Metric.ball, G_subset, Metric.ball_subset_closedBall, le_refl, norm_nonneg

    95 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  23. lemma Tile.eq_zero_of_notMem_closedBall line 462 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, Norm.norm, Set.indicator, OfNat.ofNat, Not, Membership.mem, Metric.closedBall, cancelPt, defaultA, HDiv.hDiv, HPow.hPow, defaultD, defaultS and 1 more

    Proof uses: Eq.mp, ENNReal, ENorm.enorm, Tile.enorm_eq_zero_of_notMem_closedBall

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  24. lemma Tile.boundedCompactSupport_star_Ks_mul_g line 466 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Measurable, LE.le, Norm.norm, Set.indicator and 11 more

    Proof uses: BoundedCompactSupport.mul_bdd_left', bcs_of_measurable_of_le_indicator_g, continuous_fst, MeasureTheory.Measure.quasiMeasurePreserving_fst, Continuous.comp_aestronglyMeasurable, Complex.continuous_conj, aestronglyMeasurable_Ks, IsCompact, Membership.mem, Dist.dist, Exists, Inter.inter, Set.preimage, tsupport, Iff.mp, Bornology.IsBounded, Metric.isBounded_iff, IsCompact.isBounded, Metric.isCompact_of_isClosed_isBounded, IsClosed.inter and 87 more

    191 instances, coercions and auxiliary constants left out.

    Tactic trace: 48 steps

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

  25. lemma Tile.boundedCompactSupport_Ks_mul_star_g line 513 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Measurable, LE.le, Norm.norm, Set.indicator and 12 more

    Proof uses: Eq.mpr, id, Eq, Eq.rec, MeasureTheory.Measure, Eq.refl, funext, Eq.trans, congrArg, Eq.symm, Complex.conj_conj, map_mul, Function.comp_apply, MeasureTheory.BoundedCompactSupport.conj, Tile.boundedCompactSupport_star_Ks_mul_g

    99 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  26. lemma Tile.boundedCompactSupport_aux_6_2_26 line 519 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Measurable, LE.le, Norm.norm, Set.indicator and 17 more

    Proof uses: MeasureTheory.BoundedCompactSupport.mk, And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, ENNReal, MeasureTheory.eLpNorm, Top.top, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, Measurable.stronglyMeasurable, Measurable.fun_mul, Prod.fst, Prod.snd, Measurable.fun_comp, Complex.measurable_starRingEnd, Prod.mk, measurable_Ks, Measurable.prodMk, Measurable.fst, Measurable.snd, measurable_id' and 178 more

    315 instances, coercions and auxiliary constants left out.

    Tactic trace: 66 steps

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

  27. lemma Tile.bound_6_2_26_aux line 592 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Prod, Tile.bound_6_2_26_aux.match_1, HMul.hMul, RingHom and 23 more

    Proof uses: MeasurableSpace, MeasureTheory.Measure, Eq.rec, Eq.refl, funext, NormedAddCommGroup, NormedSpace, Eq.mpr, id, congrFun', congrArg, mul_add, mul_sub, sub_eq_add_neg, congr, Complex.exp_add, of_eq_true, Eq.trans, True, HPow.hPow and 51 more

    181 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  28. lemma Tile.bound_6_2_26 line 618 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Measurable, LE.le, Norm.norm, Set.indicator and 17 more

    Proof uses: Eq, Ks, 𝔰, Complex.exp, Complex.I, HSub.hSub, FunctionDistances.Θ, MeasureTheory.SimpleFunc, HAdd.hAdd, Neg.neg, Tile.complex_exp_lintegral, id, Eq.mpr, congrFun', congrArg, funext, MeasureTheory.Measure.prod, Set.univ, Eq.symm, MeasureTheory.setIntegral_univ and 14 more

    139 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  29. lemma Tile.correlation_le_of_nonempty_inter We assume 6.2.23 line 638 source

    Source comment

    We assume 6.2.23.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, LE.le, OfNat.ofNat, 𝔓, 𝔰, Measurable and 28 more

    Proof uses: Trans.trans, Eq, Prod, SProd.sprod, Prod.fst, Prod.snd, Tile.I12, Tile.bound_6_2_26, MeasureTheory.setLIntegral_mono', MeasurableSet.prod, measurableSet_E, Membership.mem, LE.le.trans, Subtype.mk, And.left, And.right, 𝕔, Tile.I12_le, id, mul_le_mul' and 24 more

    214 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

    lemma correlation_le_of_nonempty_inter (ha : 4 ≤ a) {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ}
    (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x)
    (hinter : (ball (𝔠 p') (5 * D ^ 𝔰 p') ∩ ball (𝔠 p) (5 * D ^ 𝔰 p)).Nonempty) :
    ‖∫ y, adjointCarleson p' g y * conj (adjointCarleson p g y)‖ₑ ≤
    C6_1_5 a * (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) /
    volume (𝓘 p : Set X) * (∫⁻ y in E p', ‖g y‖ₑ) * ∫⁻ y in E p, ‖g y‖ₑ := by
…

    Mentions: 𝔓, 𝔰, g, 𝔠, adjointCarleson, Tile.C6_1_5, 𝓘, E

  30. lemma Tile.correlation_le_of_empty_inter If (6.2.23) does not hold, the LHS is zero and the result follows trivially line 658 source

    Source documentation

    If (6.2.23) does not hold, the LHS is zero and the result follows trivially.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Not, Set.Nonempty, Inter.inter, Metric.ball and 26 more

    Proof uses: Eq, Eq.mpr, id, congrArg, propext, enorm_eq_zero, MeasureTheory.integral_eq_zero_of_ae, Eq.eventuallyEq, MeasureTheory.ae, funext, Membership.mem, Or, Eq.mp, Eq.trans, And, Exists, forall_congr, Decidable.byContradiction, Tile.range_support, of_eq_true and 7 more

    189 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

    lemma correlation_le_of_empty_inter {p p' : 𝔓 X} {g : X → ℂ}
    (hinter : ¬(ball (𝔠 p') (5 * D ^ 𝔰 p') ∩ ball (𝔠 p) (5 * D ^ 𝔰 p)).Nonempty) :
    ‖∫ y, adjointCarleson p' g y * conj (adjointCarleson p g y)‖ₑ ≤
    C6_1_5 a * (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) /
    volume (𝓘 p : Set X) * (∫⁻ y in E p', ‖g y‖ₑ) * ∫⁻ y in E p, ‖g y‖ₑ := by
…

    Mentions: 𝔓, g, 𝔠, 𝔰, adjointCarleson, Tile.C6_1_5, 𝓘, E

  31. lemma Tile.correlation_le Part 1 of Lemma 6.1.5 (eq line 680 source

    Source documentation

    Part 1 of Lemma 6.1.5 (eq. 6.1.43).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, 𝔰, Measurable, Norm.norm and 25 more

    Proof uses: dite, Set.Nonempty, Inter.inter, Metric.ball, Classical.propDecidable, Tile.correlation_le_of_nonempty_inter, KernelProofData.four_le_a, Not, Tile.correlation_le_of_empty_inter

    165 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

    lemma correlation_le {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ}
    (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :
    ‖∫ y, adjointCarleson p' g y * conj (adjointCarleson p g y)‖ₑ ≤
    C6_1_5 a * (1 + edist_(p') (𝒬 p') (𝒬 p)) ^ (-(2 * a ^ 2 + a ^ 3 : ℝ)⁻¹) /
    volume (𝓘 p : Set X) * (∫⁻ y in E p', ‖g y‖ₑ) * ∫⁻ y in E p, ‖g y‖ₑ := by
…

    Mentions: 𝔓, 𝔰, g, adjointCarleson, Tile.C6_1_5, 𝓘, E

  32. lemma Tile.correlation_zero_of_ne_subset Part 2 of Lemma 6.1.5 (claim 6.1.44) line 690 source

    Source documentation

    Part 2 of Lemma 6.1.5 (claim 6.1.44).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, LE.le, 𝔰, Not, 𝓘 and 13 more

    Proof uses: Mathlib.Tactic.Contrapose.contrapose₂, id, Ne, Exists, MeasureTheory.exists_ne_zero_of_integral_ne_zero, Eq.mp, congrArg, propext, enorm_ne_zero, LE.le.trans, GridStructure.c, GridStructure.s, GridStructure.Grid_subset_ball, Membership.mem, Eq.mpr, LT.lt, Dist.dist, Metric.mem_ball, Trans.trans, HAdd.hAdd and 47 more

    209 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    lemma correlation_zero_of_ne_subset {p p' : 𝔓 X} (hle : 𝔰 p' ≤ 𝔰 p) {g : X → ℂ}
    (hp : ¬(𝓘 p' : Set X) ⊆ ball (𝔠 p) (14 * D ^ 𝔰 p)) :
    ‖∫ y, adjointCarleson p' g y * conj (adjointCarleson p g y)‖ₑ = 0 := by
…

    Mentions: 𝔓, 𝔰, g, 𝓘, 𝔠, adjointCarleson