Code

WIP: progress on Chapter 8#195

Code

Open

grunweg wants to merge 54 commits intomasterfpvandoorn/carleson:masterfrom MR-statements-8.0.1fpvandoorn/carleson:MR-statements-8.0.1Copy head branch name to clipboard

+270-19

Commits

Commits on Nov 12, 2024

• wip: formalise the first three statements

  grunweg

  committed
  2094483

  Copy full SHA for 2094483

• First lemma proven.

  grunweg

  committed
  f36512a

  Copy full SHA for f36512a

• checkpoint

  grunweg

  committed
  3d7c3c8

  Copy full SHA for 3d7c3c8

• Checkpoint, with what I just learned.

  grunweg

  committed
  baed19a

  Copy full SHA for baed19a

• Checkpoint: *mostly* solved 8.0.6; exposed a missing lemma in mathlib

  grunweg

  committed
  5131eb6

  Copy full SHA for 5131eb6

• Mathlib has the main lemma I want.

  grunweg

  committed
  5bed1dd

  Copy full SHA for 5bed1dd

• Mostly proved Lipschitz-ness, except for one error I don't understand yet.

  grunweg

  committed
  54ad877

  Copy full SHA for 54ad877

• Blueprint errors.

  grunweg

  committed
  65bc6f1

  Copy full SHA for 65bc6f1

• Last items for today.

  grunweg

  committed
  be82214

  Copy full SHA for be82214

• Progress towards 8_0_8; one superfluous hypothesis.

  grunweg

  committed
  990202c

  Copy full SHA for 990202c

• Is this better? Elaborator bug is obscuring things.

  grunweg

  committed
  541f756

  Copy full SHA for 541f756

• Progress

  grunweg

  committed
  0dd4c13

  Copy full SHA for 0dd4c13

• Small progress.

  grunweg

  committed
  b3a41ff

  Copy full SHA for b3a41ff

• chore: cleaner variable management

  grunweg

  committed
  abf7df2

  Copy full SHA for abf7df2

• Powering through; inelegant.

  grunweg

  committed
  f85f674

  Copy full SHA for f85f674

• Clean up a little.

  grunweg

  committed
  a227814

  Copy full SHA for a227814

• Progress; enough for today

  grunweg

  committed
  8451a0b

  Copy full SHA for 8451a0b

• Fix one type mismatch.

  grunweg

  committed
  b512f0c

  Copy full SHA for b512f0c

• Small clean-ups.

  grunweg

  committed
  16f3bf6

  Copy full SHA for 16f3bf6

• WIP Lipschitz lemma

  grunweg

  committed
  78357ce

  Copy full SHA for 78357ce

• Fix the bump.

  grunweg

  committed
  24ac916

  Copy full SHA for 24ac916

• Slow progress. Conversions are hard.

  grunweg

  committed
  51eee40

  Copy full SHA for 51eee40

• Slightly further.

  grunweg

  committed
  bd43907

  Copy full SHA for bd43907

• Try flipping the order of the calc blocks.

  grunweg

  committed
  fedca2e

  Copy full SHA for fedca2e

Commits on Nov 13, 2024

• Small progress.

  grunweg

  committed
  1625f4c

  Copy full SHA for 1625f4c

Commits on Nov 17, 2024

• Merge branch 'master' into MR-statements-8.0.1

  grunweg

  committed
  bce5f2a

  Copy full SHA for bce5f2a

• chore: fix merge

  grunweg

  committed
  dff8cab

  Copy full SHA for dff8cab

• Tweaks on upstreaming PR.

  grunweg

  committed
  81be853

  Copy full SHA for 81be853

Commits on Nov 18, 2024

• chore: mostly state the missing pieces towards Lemma 8.0.1

  grunweg

  committed
  1144067

  Copy full SHA for 1144067

• Merge branch 'master' into MR-statements-8.0.1

  grunweg

  committed
  5707dd3

  Copy full SHA for 5707dd3

• Fix merge.

  grunweg

  committed
  18d446f

  Copy full SHA for 18d446f

• refactor: extract a long have

  grunweg

  committed
  67c591a

  Copy full SHA for 67c591a

• Small tweaks.

  grunweg

  committed
  18c30da

  Copy full SHA for 18c30da

• Progress, more sorries.

  grunweg

  committed
  85bbcd9

  Copy full SHA for 85bbcd9

Commits on Nov 19, 2024

• Tweaks during the meeting.

  grunweg

  committed
  bbf01c9

  Copy full SHA for bbf01c9

• Progress/simplify

  grunweg

  committed
  ca1aea4

  Copy full SHA for ca1aea4

• Fix another sorry.

  grunweg

  committed
  1cd27f1

  Copy full SHA for 1cd27f1

• WIP: try using better types. enough for the moment

  grunweg

  committed
  5e5c7e3

  Copy full SHA for 5e5c7e3

Commits on Dec 16, 2024

• Merge branch 'master' into MR-statements-8.0.1

  grunweg

  committed
  23272c9

  Copy full SHA for 23272c9

• Some simplifications.

  grunweg

  committed
  df997c3

  Copy full SHA for df997c3

• Still difficult!

  grunweg

  committed
  2165e6a

  Copy full SHA for 2165e6a

• 8.0.8 is still proving difficult

  grunweg

  committed
  9587930

  Copy full SHA for 9587930

• Getting closer

  grunweg

  committed
  3c77c1d

  Copy full SHA for 3c77c1d

• Small progress

  grunweg

  committed
  73beac4

  Copy full SHA for 73beac4

• Small golfs

  grunweg

  committed
  eb48fee

  Copy full SHA for eb48fee

• WIP: fixing 8.0.8 for good - need to use N as an integer (perhaps even a natural number)

  grunweg

  committed
  cf7d5da

  Copy full SHA for cf7d5da

• Trying a bit more: a few more annoying conversions!

  grunweg

  committed
  935af44

  Copy full SHA for 935af44

• Enough for today

  grunweg

  committed
  a95e6ec

  Copy full SHA for a95e6ec

Commits on Dec 17, 2024

• fix: lift N to \N, this part works now

  grunweg

  committed
  c55b933

  Copy full SHA for c55b933

• Progress

  grunweg

  committed
  0615604

  Copy full SHA for 0615604

• Update

  grunweg

  committed
  84faaf3

  Copy full SHA for 84faaf3

• Big progress on aux8_0_8

  grunweg

  committed
  dc150f8

  Copy full SHA for dc150f8

• One sorry in the main proof of 8.0.8

  grunweg

  committed
  a6fe34a

  Copy full SHA for a6fe34a

• Auxiliary lemma done; clean-up: one total sorry remains for (8.0.8)

  grunweg

  committed
  aa8db25

  Copy full SHA for aa8db25