Commits

Branch selector

 main

User selector

All users

Datepicker

All time

Commit History

Commits on Dec 25, 2025

• Merge pull request #424 from brandondong/comment_fix

  Show description for 1a501c7
  teorth

  authored
  1a501c7

  Copy full SHA for 1a501c7

• Merge pull request #423 from aodecipher/main

  Show description for 7f6235c
  teorth

  authored
  7f6235c

  Copy full SHA for 7f6235c

Commits on Dec 23, 2025

• Complete proofs for Lemma 1.3.9 TFAE helper lemmas

  Show description for 4c8ae71
  aodecipher

  committed
  4c8ae71

  Copy full SHA for 4c8ae71

• Add structure for Lemma 1.3.9 TFAE proof (UnsignedMeasurable equivalences)

  Show description for dcd6d75
  aodecipher

  committed
  dcd6d75

  Copy full SHA for dcd6d75

Commits on Dec 22, 2025

• Minor section 2/3 comment fixes

  brandondong

  committed
  7d96982

  Copy full SHA for 7d96982

• Merge sketch branch into main

  aodecipher

  committed
  e5e9bce

  Copy full SHA for e5e9bce

• Complete proofs for AlmostEverywhereEqual equivalence relation

  Show description for 1973913
  aodecipher

  committed
  1973913

  Copy full SHA for 1973913

• Add AlmostEverywhereEqual equivalence relation structure

  Show description for 03efe0b
  aodecipher

  committed
  03efe0b

  Copy full SHA for 03efe0b

• Merge sketch branch into main

  aodecipher

  committed
  40050a5

  Copy full SHA for 40050a5

• Complete proof for RealSimpleFunction.toComplex

  Show description for 7a4ec5f
  aodecipher

  committed
  7a4ec5f

  Copy full SHA for 7a4ec5f

• Refactor: move singleAtom machinery to IntegralWellDef namespace

  Show description for bcfed3d
  aodecipher

  committed
  bcfed3d

  Copy full SHA for bcfed3d

• Add disjoint representation and complete RealSimpleFunction.pos/neg proofs

  Show description for 909b88e
  aodecipher

  committed
  909b88e

  Copy full SHA for 909b88e

• Complete proofs for ComplexSimpleFunction real and imaginary parts

  Show description for 57a5f5f
  aodecipher

  committed
  57a5f5f

  Copy full SHA for 57a5f5f

Commits on Dec 21, 2025

• Merge pull request #422 from ggrandi/exercise-4-4-2-b

  Show description for e175819
  teorth

  authored
  e175819

  Copy full SHA for e175819

• added the second part of exercise 4.4.2 (b)

  ggrandi

  committed
  7f2896c

  Copy full SHA for 7f2896c

Commits on Dec 20, 2025

• Merge branch 'main' into sketch

  aodecipher

  committed
  0cc610a

  Copy full SHA for 0cc610a

• Complete proofs for AlmostAlways lemmas and support measurability

  Show description for cedd36d
  aodecipher

  committed
  cedd36d

  Copy full SHA for cedd36d

• Update .gitignore: exclude env files, aider config, and docker directories

  Show description for ef62888
  aodecipher

  committed
  ef62888

  Copy full SHA for ef62888

• Merge pull request #421 from teorth:1.4.1

  Show description for 27eeea1
  teorth

  authored
  27eeea1

  Copy full SHA for 27eeea1

• Finish 1.4.1

  teorth

  committed
  6557f7a

  Copy full SHA for 6557f7a

• start on 1.4.1

  teorth

  committed
  f95b59c

  Copy full SHA for f95b59c

Commits on Dec 19, 2025

• Merge pull request #420 from aodecipher/main

  Show description for 9bda02d
  teorth

  authored
  9bda02d

  Copy full SHA for 9bda02d

Commits on Dec 18, 2025

• Complete proving that Lower Unsigned Lebesgue Integral only requires a.e. boundedness

  Show description for b61ab70
  aodecipher

  committed
  b61ab70

  Copy full SHA for b61ab70

Commits on Dec 17, 2025

• Refactor: extract bitwise lemmas to NatBitwise utility file

  Show description for 4e93566
  aodecipher

  committed
  4e93566

  Copy full SHA for 4e93566

• Complete proof of Lemma 1.3.4 (Well-definedness of simple integral) and all its helpers

  Show description for 0c74676
  aodecipher

  committed
  0c74676

  Copy full SHA for 0c74676

• Construct main proof of UnsignedSimpleFunction.integral_eq (Lemma 1.3.4)

  Show description for 029785e
  aodecipher

  committed
  029785e

  Copy full SHA for 029785e

• Construct the main proof of LowerUnsignedLebesgueIntegral.add (Corollary 1.3.14)

  Show description for 2e12cec
  aodecipher

  committed
  2e12cec

  Copy full SHA for 2e12cec

Commits on Dec 16, 2025

• Complete proofs for RealSimpleFunction and ComplexSimpleFunction operations

  Show description for 32f22bf
  aodecipher

  committed
  32f22bf

  Copy full SHA for 32f22bf

• Refactor: move ereal_mul_sum_nonneg to public utilities

  Show description for 07e83a8
  aodecipher

  committed
  07e83a8

  Copy full SHA for 07e83a8

• Complete proofs for UnsignedSimpleFunction.add and smul

  Show description for 5035a9e
  aodecipher

  committed
  5035a9e

  Copy full SHA for 5035a9e

Commits on Dec 15, 2025

• Merge pull request #419 from lcastelli/set-fixes

  Show description for 36544c6
  teorth

  authored
  36544c6

  Copy full SHA for 36544c6

• Adds missing brackets.

  lcastelli

  committed
  94e09c4

  Copy full SHA for 94e09c4

• Rename a theorem to better match its statement.

  lcastelli

  committed
  8dd2ad1

  Copy full SHA for 8dd2ad1

• Fixes duplicate exercise number.

  lcastelli

  committed
  5b85a93

  Copy full SHA for 5b85a93

• Fixes the definition of the bottom element of extended reals.

  lcastelli

  committed
  c327935

  Copy full SHA for c327935

Pagination

Previous

Next